awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (e.trans (PartialEquiv.refl β)).source = e.source

Tactic:
simp [trans_source]

Premises used: PartialEquiv.trans_source
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ ((PartialEquiv.refl α).trans e).source = e.source

Tactic:
simp [trans_source, preimage_id]

Premises used: PartialEquiv.trans_source, Set.preimage_id
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ e.trans (ofSet s) = e.restr ((↑e : α → β) ⁻¹' s)

Tactic:
PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) rfl

Premises used: PartialEquiv.ext, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ (e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr ((↑e : α → β) ⁻¹' s)).source

Tactic:
simp [trans_source]

Premises used: PartialEquiv.trans_source
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
simp : e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ (e.source ∩ (↑e : α → β) ⁻¹' s)
⊢ (e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr (e.source ∩ (↑e : α → β) ⁻¹' s)).source

Tactic:
simp only [trans_source, restr_source, refl_source, univ_inter]

Premises used: PartialEquiv.trans_source, Set.univ_inter, PartialEquiv.refl_source, PartialEquiv.restr_source
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
rw : e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ e.source ∩ (↑e : α → β) ⁻¹' s
rw₁ rw₂ : e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ (↑e : α → β) ⁻¹' s
⊢ e.source ∩ (↑e : α → β) ⁻¹' s = e.source ∩ (e.source ∩ (↑e : α → β) ⁻¹' s)

Tactic:
rw [← inter_assoc, inter_self]

Premises used: Set.inter_self, Set.inter_assoc
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
s : Set α
⊢ ((e.restr s).trans e').source = ((e.trans e').restr s).source

Tactic:
simp [trans_source, inter_comm, inter_assoc]

Premises used: PartialEquiv.trans_source, Set.inter_comm, Set.inter_assoc
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
rwa : (↑e.symm.symm.symm : β → α) ((↑e : α → β) x) ∈ e'.source
rwa₁ : (↑e.symm : β → α) ((↑e : α → β) x) ∈ e'.source
rwa₂ rwa₃ rwa₄ rwa₅ : x ∈ e'.source
⊢ (↑e : α → β) x ∈ (↑e.symm.symm.symm : β → α) ⁻¹' e'.source

Tactic:
rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]

Premises used: PartialEquiv.symm_symm, PartialEquiv.left_inv, Set.mem_preimage
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
refl : ∀ (x : PartialEquiv α β), x.EqOnSource x
symm : ∀ {x y : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource x
trans : ∀ {x y z : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource z → x.EqOnSource z
⊢ Equivalence (α := PartialEquiv α β) EqOnSource

Tactic:
constructor
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ (x : PartialEquiv α β), x.EqOnSource x

Tactic:
grind [EqOnSource, EqOn]

Premises used: Set.EqOn, PartialEquiv.EqOnSource
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ {x y : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource x

Tactic:
grind [EqOnSource, EqOn]

Premises used: Set.EqOn, PartialEquiv.EqOnSource
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ {x y z : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource z → x.EqOnSource z

Tactic:
grind [EqOnSource, EqOn]

Premises used: Set.EqOn, PartialEquiv.EqOnSource
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e ≈ e

Tactic:
Setoid.refl _

Premises used: Setoid.refl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ e.source = e'.source

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ EqOn (↑e : α → β) (↑e' : α → β) e.source

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ e.target = e'.target

Tactic:
simp only [← image_source_eq_target, ← source_eq h, h.2.image_eq]

Premises used: PartialEquiv.image_source_eq_target, PartialEquiv.EqOnSource.source_eq, And.right, Set.EqOn.image_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ e.symm ≈ e'.symm

Tactic:
⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩

Premises used: Set.eqOn_of_leftInvOn_of_rightInvOn, PartialEquiv.EqOnSource, And.intro, PartialEquiv.leftInvOn, PartialEquiv.EqOnSource.target_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
refine_1 : RightInvOn (↑e'.symm : β → α) (↑e : α → β) e.symm.source
refine_2 : MapsTo (↑e'.symm : β → α) e.symm.source e.source
⊢ e.symm ≈ e'.symm

Tactic:
refine ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
refine_1 : RightInvOn (↑e'.symm : β → α) (↑e : α → β) e'.target
⊢ RightInvOn (↑e'.symm : β → α) (↑e : α → β) e.symm.source

Tactic:
simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]

Premises used: PartialEquiv.EqOnSource.source_eq, PartialEquiv.symm_source, PartialEquiv.symm_mapsTo, PartialEquiv.EqOnSource.target_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ MapsTo (↑e'.symm : β → α) e.symm.source e.source

Tactic:
simp only [symm_source, target_eq h, source_eq h, e'.symm_mapsTo]

Premises used: PartialEquiv.EqOnSource.source_eq, PartialEquiv.symm_source, PartialEquiv.symm_mapsTo, PartialEquiv.EqOnSource.target_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑e'.symm : β → α) (↑e : α → β) e'.target

Tactic:
e'.rightInvOn.congr_right e'.symm_mapsTo (source_eq h ▸ h.eqOn.symm)

Premises used: Eq.rec, PartialEquiv.EqOnSource.source_eq, Set.RightInvOn.congr_right, PartialEquiv.symm_mapsTo, Set.EqOn.symm, PartialEquiv.EqOnSource.eqOn, PartialEquiv.rightInvOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑e'.symm : β → α) (↑e : α → β) e'.target

Tactic:
exact e'.rightInvOn.congr_right e'.symm_mapsTo (source_eq h ▸ h.eqOn.symm)

Premises used: Set.RightInvOn.congr_right, PartialEquiv.symm_mapsTo, PartialEquiv.rightInvOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ EqOn (↑e.symm : β → α) (↑e'.symm : β → α) e.target

Tactic:
eqOn h.symm'

Premises used: PartialEquiv.EqOnSource.symm', PartialEquiv.EqOnSource.eqOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
left : (e.trans f).source = (e'.trans f').source
right : EqOn (↑(e.trans f) : α → γ) (↑(e'.trans f') : α → γ) (e.trans f).source
⊢ e.trans f ≈ e'.trans f'

Tactic:
constructor
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
left : (↑e.symm : β → α) '' (e.target ∩ f.source) = (↑e'.symm : β → α) '' (e.target ∩ f.source)
⊢ (e.trans f).source = (e'.trans f').source

Tactic:
rw [trans_source'', trans_source'', ← target_eq he, ← hf.1]

Premises used: PartialEquiv.trans_source'', And.left, PartialEquiv.EqOnSource.target_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (↑e.symm : β → α) '' (e.target ∩ f.source) = (↑e'.symm : β → α) '' (e.target ∩ f.source)

Tactic:
(he.symm'.eqOn.mono inter_subset_left).image_eq

Premises used: Set.inter_subset_left, PartialEquiv.EqOnSource.symm', Set.EqOn.image_eq, PartialEquiv.EqOnSource.eqOn, Set.EqOn.mono
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (↑e.symm : β → α) '' (e.target ∩ f.source) = (↑e'.symm : β → α) '' (e.target ∩ f.source)

Tactic:
exact (he.symm'.eqOn.mono inter_subset_left).image_eq

Premises used: Set.inter_subset_left, PartialEquiv.EqOnSource.symm', Set.EqOn.image_eq, PartialEquiv.EqOnSource.eqOn, Set.EqOn.mono
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ (e.trans f).source
⊢ x ∈ e.source ∩ (↑e : α → β) ⁻¹' f.source

Tactic:
rw [trans_source] at hx

Premises used: PartialEquiv.trans_source
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
x : α
hx : x ∈ e.source ∩ (↑e : α → β) ⁻¹' f.source
⊢ (↑(e.trans f) : α → γ) x = (↑(e'.trans f') : α → γ) x

Tactic:
simp [Function.comp_apply, PartialEquiv.coe_trans, (he.2 hx.1).symm, hf.2 hx.2]

Premises used: And.right, And.left, PartialEquiv.coe_trans, Function.comp_apply, Eq.symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
left : (e.restr s).source = (e'.restr s).source
right : EqOn (↑(e.restr s) : α → β) (↑(e'.restr s) : α → β) (e.restr s).source
⊢ e.restr s ≈ e'.restr s

Tactic:
constructor
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ (e.restr s).source = (e'.restr s).source

Tactic:
simp [he.1]

Premises used: And.left
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ (e.restr s).source
⊢ x ∈ e.source ∧ x ∈ s

Tactic:
simp only [mem_inter_iff, restr_source] at hx

Premises used: Set.mem_inter_iff, PartialEquiv.restr_source
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ e.source ∧ x ∈ s
⊢ (↑(e.restr s) : α → β) x = (↑(e'.restr s) : α → β) x

Tactic:
he.2 hx.1

Premises used: And.right, And.left
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
x : α
hx : x ∈ e.source ∧ x ∈ s
⊢ (↑(e.restr s) : α → β) x = (↑(e'.restr s) : α → β) x

Tactic:
exact he.2 hx.1

Premises used: And.right, And.left
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set β
rw : e.source ∩ (↑e' : α → β) ⁻¹' s = e'.source ∩ (↑e' : α → β) ⁻¹' s
rw₁ rw₂ : e'.source ∩ (↑e' : α → β) ⁻¹' s = e'.source ∩ (↑e' : α → β) ⁻¹' s
⊢ e.source ∩ (↑e : α → β) ⁻¹' s = e'.source ∩ (↑e' : α → β) ⁻¹' s

Tactic:
rw [he.eqOn.inter_preimage_eq, source_eq he]

Premises used: PartialEquiv.EqOnSource.source_eq, PartialEquiv.EqOnSource.eqOn, Set.EqOn.inter_preimage_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
h h₁ h₂ h₃ : ∀ (my_y : α), my_y ∈ (e.trans e.symm).source ↔ my_y ∈ e.source
⊢ (e.trans e.symm).source = e.source

Tactic:
mfld_set_tac
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (e.trans e.symm).source = e.source

Tactic:
have A : (e.trans e.symm).source = e.source := by mfld_set_tac
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
rw : e.source = (ofSet e.source).source
rw₁ rw₂ : e.source = e.source
⊢ (e.trans e.symm).source = (ofSet e.source).source

Tactic:
rw [A, ofSet_source]

Premises used: PartialEquiv.ofSet_source
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
refine : ∀ (x : α) (hx : x ∈ (e.trans e.symm).source), (↑(e.trans e.symm) : α → α) x = (↑(ofSet e.source) : α → α) x
⊢ e.trans e.symm ≈ ofSet e.source

Tactic:
refine ⟨by rw [A, ofSet_source], fun x hx => ?_⟩
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ (e.trans e.symm).source
⊢ x ∈ e.source

Tactic:
rw [A] at hx
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ e.source
⊢ (↑(e.trans e.symm) : α → α) x = (↑(ofSet e.source) : α → α) x

Tactic:
simp only [hx, mfld_simps]
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.symm.trans e ≈ ofSet e.target

Tactic:
self_trans_symm e.symm

Premises used: PartialEquiv.symm, PartialEquiv.self_trans_symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
⊢ e = e'

Tactic:
PartialEquiv.ext (fun x => ?_) (fun x => ?_) h.1

Premises used: PartialEquiv.ext, And.left
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
refine_1 : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
refine_2 : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
⊢ e = e'

Tactic:
refine PartialEquiv.ext (fun x => ?_) (fun x => ?_) h.1

Premises used: PartialEquiv.ext, And.left
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
refine_1 : x ∈ e.source
⊢ (↑e : α → β) x = (↑e' : α → β) x

Tactic:
apply h.2

Premises used: And.right
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
refine_1 : Membership.mem (γ := Set α) univ x
⊢ x ∈ e.source

Tactic:
rw [s]
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ Membership.mem (γ := Set α) univ x

Tactic:
mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ Membership.mem (γ := Set α) univ x

Tactic:
exact mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
refine_2 : x ∈ e.symm.source
⊢ (↑e.symm : β → α) x = (↑e'.symm : β → α) x

Tactic:
apply h.symm'.2

Premises used: PartialEquiv.EqOnSource.symm', And.right
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
refine_2 : Membership.mem (γ := Set β) univ x
⊢ x ∈ e.symm.source

Tactic:
rw [symm_source, t]

Premises used: PartialEquiv.symm_source
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ Membership.mem (γ := Set β) univ x

Tactic:
mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : β
⊢ Membership.mem (γ := Set β) univ x

Tactic:
exact mem_univ _

Premises used: Set.mem_univ
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e'_1 : PartialEquiv β γ
e : PartialEquiv α β
e' : PartialEquiv γ δ
p : α × γ
hp : p ∈ e.source ×ˢ e'.source
⊢ ((↑e : α → β) p.1, (↑e' : γ → δ) p.2) ∈ e.target ×ˢ e'.target

Tactic:
simp_all
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e'_1 : PartialEquiv β γ
e : PartialEquiv α β
e' : PartialEquiv γ δ
p : β × δ
hp : p ∈ e.target ×ˢ e'.target
⊢ ((↑e.symm : β → α) p.1, (↑e'.symm : δ → γ) p.2) ∈ e.source ×ˢ e'.source

Tactic:
simp_all
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e'_1 : PartialEquiv β γ
e : PartialEquiv α β
e' : PartialEquiv γ δ
p : α × γ
hp : p ∈ e.source ×ˢ e'.source
⊢ ((↑e.symm : β → α) ((↑e : α → β) p.1, (↑e' : γ → δ) p.2).1,
      (↑e'.symm : δ → γ) ((↑e : α → β) p.1, (↑e' : γ → δ) p.2).2) =
    p

Tactic:
simp_all
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e'_1 : PartialEquiv β γ
e : PartialEquiv α β
e' : PartialEquiv γ δ
p : β × δ
hp : p ∈ e.target ×ˢ e'.target
⊢ ((↑e : α → β) ((↑e.symm : β → α) p.1, (↑e'.symm : δ → γ) p.2).1,
      (↑e' : γ → δ) ((↑e.symm : β → α) p.1, (↑e'.symm : δ → γ) p.2).2) =
    p

Tactic:
simp_all
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
⊢ (e.prod e').source = e.source ×ˢ e'.source

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
⊢ (e.prod e').target = e.target ×ˢ e'.target

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
⊢ (↑(e.prod e') : α × γ → β × δ) = fun (p : α × γ) ↦ ((↑e : α → β) p.1, (↑e' : γ → δ) p.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
⊢ (↑(e.prod e').symm : β × δ → α × γ) = fun (p : β × δ) ↦ ((↑e.symm : β → α) p.1, (↑e'.symm : δ → γ) p.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
h : ∀ (x : β × δ), ((↑(e.prod e').symm : β × δ → α × γ) x).1 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).1
h₁ : ∀ (x : β × δ), ((↑(e.prod e').symm : β × δ → α × γ) x).2 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).2
hsymm :
  ∀ (x : α × γ), ((↑(e.prod e').symm.symm : α × γ → β × δ) x).1 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).1
hsymm₁ :
  ∀ (x : α × γ), ((↑(e.prod e').symm.symm : α × γ → β × δ) x).2 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).2
hs : ∀ (x : β × δ), x ∈ (e.prod e').symm.source ↔ x ∈ (e.symm.prod e'.symm).source
⊢ (e.prod e').symm = e.symm.prod e'.symm

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ ((↑(e.prod e').symm : β × δ → α × γ) x).1 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).1

Tactic:
simp [prod_coe_symm]

Premises used: PartialEquiv.prod_coe_symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ ((↑(e.prod e').symm : β × δ → α × γ) x).2 = ((↑(e.symm.prod e'.symm) : β × δ → α × γ) x).2

Tactic:
simp [prod_coe_symm]

Premises used: PartialEquiv.prod_coe_symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : α × γ
⊢ ((↑(e.prod e').symm.symm : α × γ → β × δ) x).1 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).1

Tactic:
simp [prod_coe_symm]

Premises used: PartialEquiv.prod_coe_symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : α × γ
⊢ ((↑(e.prod e').symm.symm : α × γ → β × δ) x).2 = ((↑(e.symm.prod e'.symm).symm : α × γ → β × δ) x).2

Tactic:
simp [prod_coe_symm]

Premises used: PartialEquiv.prod_coe_symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv γ δ
x : β × δ
⊢ x ∈ (e.prod e').symm.source ↔ x ∈ (e.symm.prod e'.symm).source

Tactic:
simp [prod_coe_symm]

Premises used: PartialEquiv.prod_coe_symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).1 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).1
h₁ :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).2 =
      ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).2
hsymm :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).1 =
      ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).1
hsymm₁ :
  ∀ (x : α) (y : β),
    ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).2 =
      ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).2
hs :
  ∀ (x : α) (y : β),
    (x, y) ∈ ((PartialEquiv.refl α).prod (PartialEquiv.refl β)).source ↔
      Membership.mem (γ := Set (α × β)) (source (PartialEquiv.refl (α × β))) (x, y)
⊢ (PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
x : α
y : β
⊢ ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).1 =
    ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
x : α
y : β
⊢ ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)) : α × β → α × β) (x, y)).2 =
    ((↑(PartialEquiv.refl (α × β)) : α × β → α × β) (x, y)).2

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
x : α
y : β
⊢ ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).1 =
    ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).1

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
x : α
y : β
⊢ ((↑((PartialEquiv.refl α).prod (PartialEquiv.refl β)).symm : α × β → α × β) (x, y)).2 =
    ((↑(PartialEquiv.symm (PartialEquiv.refl (α × β))) : α × β → α × β) (x, y)).2

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
x : α
y : β
⊢ (x, y) ∈ ((PartialEquiv.refl α).prod (PartialEquiv.refl β)).source ↔
    Membership.mem (γ := Set (α × β)) (source (PartialEquiv.refl (α × β))) (x, y)

Tactic:
simp