internlm/Lean-Github huggingface dataset:
Theorem: gleason_diagram_commutes
Proof 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
Proof 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
Theorem: gleason_diagram_commutes
Proof 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
Proof 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
Theorem: gleason_diagram_commutes
Proof 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]
Proof 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)
Theorem: gleason_diagram_commutes
Proof 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, π₁]
Proof 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
Theorem: gleason_diagram_commutes
Proof 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
Proof 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
Theorem: gleason_diagram_commutes
Proof 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
Proof 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
Theorem: gleason_diagram_commutes
Proof 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
Proof state after:
no goals
Theorem: gleason_diagram_commutes
Proof 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]
Proof 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 = φ
Theorem: gleason_diagram_commutes
Proof 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]
Proof 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 = φ
Theorem: gleason_diagram_commutes
Proof 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]
Proof state after:
no goals
Theorem: ExtrDisc.openEmbedding_of_sigma_desc_iso
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
⊢ ∀ (a : α), OpenEmbedding ↑(i a)
Tactic:
intro a
Proof state after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
⊢ OpenEmbedding ↑(i a)
Theorem: ExtrDisc.openEmbedding_of_sigma_desc_iso
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
⊢ OpenEmbedding ↑(i a)
Tactic:
have h₁ : OpenEmbedding (Sigma.desc i) :=
  (ExtrDisc.homeoOfIso (asIso (Sigma.desc i))).openEmbedding
Proof state after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
⊢ OpenEmbedding ↑(i a)
Theorem: ExtrDisc.openEmbedding_of_sigma_desc_iso
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
⊢ OpenEmbedding ↑(i a)
Tactic:
have h₂ : OpenEmbedding (Sigma.ι Z a) := openEmbedding_ι _ _
Proof state after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
⊢ OpenEmbedding ↑(i a)
Theorem: ExtrDisc.openEmbedding_of_sigma_desc_iso
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
⊢ OpenEmbedding ↑(i a)
Tactic:
have := OpenEmbedding.comp h₁ h₂
Proof state after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding (↑(Sigma.desc i) ∘ ↑(Sigma.ι Z a))
⊢ OpenEmbedding ↑(i a)
Theorem: ExtrDisc.openEmbedding_of_sigma_desc_iso
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding (↑(Sigma.desc i) ∘ ↑(Sigma.ι Z a))
⊢ OpenEmbedding ↑(i a)
Tactic:
erw [← CategoryTheory.coe_comp (Sigma.ι Z a) (Sigma.desc i)] at this
Proof state after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding ↑(Sigma.ι Z a ≫ Sigma.desc i)
⊢ OpenEmbedding ↑(i a)
Theorem: ExtrDisc.openEmbedding_of_sigma_desc_iso
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding ↑(Sigma.ι Z a ≫ Sigma.desc i)
⊢ OpenEmbedding ↑(i a)
Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app] at this
Proof state after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding ↑(i a)
⊢ OpenEmbedding ↑(i a)
Theorem: ExtrDisc.openEmbedding_of_sigma_desc_iso
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding ↑(i a)
⊢ OpenEmbedding ↑(i a)
Tactic:
assumption
Proof state after:
no goals
Theorem: ExtrDisc.isIso_of_bijective
Proof state before:
X Y : ExtrDisc
f : X ⟶ Y
hf : Function.Bijective ↑f
⊢ IsIso (toCompHaus.map f)
Tactic:
exact CompHaus.isIso_of_bijective _ hf
Proof state after:
no goals
Theorem: ExtrDisc.isIso_of_bijective
Proof state before:
X Y : ExtrDisc
f : X ⟶ Y
hf : Function.Bijective ↑f
this : IsIso (toCompHaus.map f)
⊢ IsIso f
Tactic:
apply isIso_of_fully_faithful toCompHaus
Proof state after:
no goals
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
π : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α), OpenEmbedding ↑(π a)
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
let ζ := finiteCoproduct.desc _ (fun a => pullback.snd f (hOpen a) ≫ finiteCoproduct.ι Z a )
Proof state after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
π : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
π : (a : α) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
let α := finiteCoproduct.desc _ ((fun a => pullback.fst f (hOpen a)))
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Theorem: ExtrDisc.extensivity_injective
Proof state before:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))
Tactic:
let β := finiteCoproduct.desc _ π
Proof state after:
α✝ : Type
inst✝ : Fintype α✝
X : ExtrDisc
Z : α✝ → ExtrDisc
π : (a : α✝) → Z a ⟶ X
Y : ExtrDisc
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
hOpen : ∀ (a : α✝), OpenEmbedding ↑(π a)
ζ : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.snd f (_ : OpenEmbedding ↑(π a)) ≫ finiteCoproduct.ι Z a
α : (finiteCoproduct fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) ⟶ Y :=
  finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
    ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a))
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Injective
    ↑(finiteCoproduct.desc (fun a => (OpenEmbeddingCone f (_ : OpenEmbedding ↑(π a))).pt) fun a =>
        ExtrDisc.pullback.fst f (_ : OpenEmbedding ↑(π a)))