-- Mathlib/Topology/PartialHomeomorph.lean
theorem subtypeRestr_symm_trans_subtypeRestr (f f' : PartialHomeomorph X Y) :
    (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈
      (f.symm.trans f').restr (f.target ∩ f.symm ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm

Tactic:
have set_identity : f.symm.source ∩ (f.target ∩ f.symm ⁻¹' s) = f.symm.source ∩ f.symm ⁻¹' s := by
  mfld_set_tac

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans ((s.partialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)

Tactic:
rw [← ofSet_trans _ openness₁, ← trans_assoc, ← trans_assoc]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ ((f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs)).trans f' ≈
    ((ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm).trans f'

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
⊢ (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)

Tactic:
simp only [subtypeRestr_def, trans_symm_eq_symm_trans_symm]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans ((s.partialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans ((s.partialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)

Tactic:
have openness₁ : IsOpen (f.target ∩ f.symm ⁻¹' s) := f.isOpen_inter_preimage_symm s.2

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans ((s.partialHomeomorphSubtypeCoe hs).trans f') ≈
    (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ ofSet (s.partialHomeomorphSubtypeCoe hs).target ⋯ ≈ ofSet (↑s) openness₂

Tactic:
simp only [mfld_simps, Setoid.refl]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ (s.partialHomeomorphSubtypeCoe hs).symm.trans (s.partialHomeomorphSubtypeCoe hs) ≈ ofSet (↑s) openness₂

Tactic:
refine Setoid.trans (symm_trans_self (s.partialHomeomorphSubtypeCoe hs)) ?_

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ ofSet (s.partialHomeomorphSubtypeCoe hs).target ⋯ ≈ ofSet (↑s) openness₂

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s

Tactic:
mfld_set_tac

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ ((f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs)).trans f' ≈
    ((ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm).trans f'

Tactic:
refine EqOnSource.trans' ?_ (eqOnSource_refl _)

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm

Tactic:
have openness₂ : IsOpen (s : Set X) := s.2

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ (f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈
    (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm

Tactic:
rw [ofSet_trans', set_identity, ← trans_of_set' _ openness₂, trans_assoc]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Opens X
hs : Nonempty ↥s
f f' : PartialHomeomorph X Y
openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)
set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s
openness₂ : IsOpen ↑s
⊢ f.symm.trans ((s.partialHomeomorphSubtypeCoe hs).symm.trans (s.partialHomeomorphSubtypeCoe hs)) ≈
    f.symm.trans (ofSet (↑s) openness₂)