exacts

Stream: new members

[Nicolò Cavalleri]

Why does not this work?

import data.equiv.local_equiv

open set

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
variables (e : local_equiv α β) (e' : local_equiv β γ)
variables {e} {s : set α} {t : set β} {x : α} {y : β}

lemma source_inter_preimage_target_inter (s : set β) :
  e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
begin
  refine ext_iff.mpr (λ x, ⟨λ hx, _, λ hx, _⟩),
  simp only [mem_inter_eq, mem_preimage] at *;
  exacts [⟨hx.1, hx.2.2⟩, ⟨hx.1, e.map_source hx.1, hx.2⟩], --exacts?
end

[Adam Topaz]

Is this missing an import?

[Adam Topaz]

The code doesn't work for me

[Nicolò Cavalleri]

Sorry, I pasted the wrong import, now it should work

[Kyle Miller]

It's weird, splitting it into two exact tactics works

[Kyle Miller]

I'm also not sure why the exact tactics work

[Nicolò Cavalleri]

Yes that's my point I mean it probably has something to do with the fact that I use an implicit construtctor?

[Adam Topaz]

You have a semicolon. Change it to a comma

[Kyle Miller]

Oh, I completely missed the ;. Exacts should work when there are multiple goals.

[Kyle Miller]

When it's a ;, it means it applies the tactic to each goal that the previous tactic has created.

[Nicolò Cavalleri]

Oh right!! I meant to put it on the previous line! I wanted to apply the simp to both goals!

[Nicolò Cavalleri]

Thanks to both!

[Nicolò Cavalleri]

And thanks to this I realized the simp is not needed.

[Kyle Miller]

@Nicolò Cavalleri You probably already worked this out after removing the simp, but you can condense it down to a one-liner term-mode proof:

lemma source_inter_preimage_target_inter (s : set β) :
  e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
ext (λ x, ⟨λ hx, ⟨hx.1, hx.2.2⟩, λ hx, ⟨hx.1, e.map_source hx.1, hx.2⟩⟩)

(note that set.ext_iff.mpr is set.ext)

[Nicolò Cavalleri]

Yes I know! I already pushed it to mathlib! Thanks anyways!

[Nicolò Cavalleri]

Kyle Miller said:

(note that set.ext_iff.mpr is set.ext)

I did not know this though! Thanks!