Theorem: gleason_diagram_commutes (ExtrDisc/Gleason.lean)

State before:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun) ∧
    f ∘ restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ
Tactic:
constructor
State after:
case left
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun)

case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ f ∘ restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ

State before:
case left
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun)
Tactic:
refine' Continuous.comp _ _
State after:
case left.refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f))

case left.refine'_2
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (ρ' hφ hf hf').toEquiv.invFun

State before:
case left.refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f))
Tactic:
refine' ContinuousOn.restrict _
State after:
case left.refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ ContinuousOn (π₂ φ f) (E' hφ hf hf')

State before:
case left.refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ ContinuousOn (π₂ φ f) (E' hφ hf hf')
Tactic:
apply Continuous.continuousOn
State after:
case left.refine'_1.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (π₂ φ f)

State before:
case left.refine'_1.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (π₂ φ f)
Tactic:
exact Continuous.comp continuous_snd continuous_subtype_val
State after:
no goals

State before:
case left.refine'_2
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ Continuous (ρ' hφ hf hf').toEquiv.invFun
Tactic:
exact (Homeomorph.continuous (Homeomorph.symm (ρ' hφ hf hf')))
State after:
no goals

State before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ f ∘ restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ
Tactic:
suffices : f ∘ (E' hφ hf hf').restrict (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toFun
State after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
this : f ∘ restrict (E' hφ hf hf') (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toEquiv.toFun
⊢ f ∘ restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ

case this
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ f ∘ restrict (E' hφ hf hf') (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toEquiv.toFun

State before:
case this
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
⊢ f ∘ restrict (E' hφ hf hf') (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toEquiv.toFun
Tactic:
ext x
State after:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
⊢ (f ∘ restrict (E' hφ hf hf') (π₂ φ f)) x = (φ ∘ (ρ' hφ hf hf').toEquiv.toFun) x

State before:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
⊢ (f ∘ restrict (E' hφ hf hf') (π₂ φ f)) x = (φ ∘ (ρ' hφ hf hf').toEquiv.toFun) x
Tactic:
simp only [Function.comp_apply, restrict_apply, Equiv.toFun_as_coe, Homeomorph.coe_toEquiv]
State after:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
⊢ f (π₂ φ f ↑x) = φ (↑(ρ' hφ hf hf') x)

State before:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
⊢ f (π₂ φ f ↑x) = φ (↑(ρ' hφ hf hf') x)
Tactic:
dsimp [π₂, ρ', compact_to_T2_homeomorph, Continuous.homeoOfEquivCompactToT2_toEquiv,
  Continuous.homeoOfEquivCompactToT2, π₁]
State after:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
⊢ f (↑↑x).snd = φ (↑↑x).fst

State before:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
⊢ f (↑↑x).snd = φ (↑↑x).fst
Tactic:
have := x.val.prop
State after:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
this : ↑↑x ∈ D' φ f
⊢ f (↑↑x).snd = φ (↑↑x).fst

State before:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
this : ↑↑x ∈ D' φ f
⊢ f (↑↑x).snd = φ (↑↑x).fst
Tactic:
dsimp [D'] at this
State after:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
this : φ (↑↑x).fst = f (↑↑x).snd
⊢ f (↑↑x).snd = φ (↑↑x).fst

State before:
case this.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
x : ↑(E' hφ hf hf')
this : φ (↑↑x).fst = f (↑↑x).snd
⊢ f (↑↑x).snd = φ (↑↑x).fst
Tactic:
exact this.symm
State after:
no goals

State before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
this : f ∘ restrict (E' hφ hf hf') (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toEquiv.toFun
⊢ f ∘ restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ
Tactic:
simp only [← Function.comp.assoc]
State after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
this : f ∘ restrict (E' hφ hf hf') (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toEquiv.toFun
⊢ (f ∘ restrict (E' hφ hf hf') (π₂ φ f)) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ

State before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
this : f ∘ restrict (E' hφ hf hf') (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toEquiv.toFun
⊢ (f ∘ restrict (E' hφ hf hf') (π₂ φ f)) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ
Tactic:
rw [this]
State after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
this : f ∘ restrict (E' hφ hf hf') (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toEquiv.toFun
⊢ (φ ∘ (ρ' hφ hf hf').toEquiv.toFun) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ

State before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
E : Set D
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSpace B
inst✝⁷ : TopologicalSpace C
inst✝⁶ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁵ : T2Space A
inst✝⁴ : CompactSpace A
inst✝³ : T2Space B
inst✝² : CompactSpace B
inst✝¹ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
inst✝ : ExtremallyDisconnected A
this : f ∘ restrict (E' hφ hf hf') (π₂ φ f) = φ ∘ (ρ' hφ hf hf').toEquiv.toFun
⊢ (φ ∘ (ρ' hφ hf hf').toEquiv.toFun) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ
Tactic:
simp only [Function.comp.assoc, Equiv.toFun_as_coe, Homeomorph.coe_toEquiv,
  Equiv.invFun_as_coe, Homeomorph.coe_symm_toEquiv,
  Homeomorph.self_comp_symm, Function.comp.right_id]
State after:
no goals