internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ¬↑f x ∈ V
Tactic:
refine' mt (fun α => hVU α) _
Proof state after:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ¬↑f x ∈ U
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ¬↑f x ∈ U
Tactic:
simp only [Set.mem_compl_iff, Set.mem_range, not_exists, not_forall, not_not]
Proof state after:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ∃ y, ↑f y = ↑f x
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case h.h.hnc
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
y : CoeSort.coe Y
hy : ∀ (a : CoeSort.coe X), ↑f a ≠ y
h✝ : Epi f
C : Set (CoeSort.coe Y) := Set.range ↑f
hC : IsClosed C
U : Set (CoeSort.coe Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ nhds y
this : TotallyDisconnectedSpace ((forget CompHaus).obj (toCompHaus.obj Y))
V : Set (CoeSort.coe Y)
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ ExtrDisc.two := ContinuousMap.mk ↑(LocallyConstant.map ULift.up (LocallyConstant.ofClopen hV))
h : Y ⟶ ExtrDisc.two := ContinuousMap.mk fun x => { down := 1 }
x : ↑((fun x => x.compHaus) X).toTop
⊢ ∃ y, ↑f y = ↑f x
Tactic:
exact ⟨x, rfl⟩
Proof state after:
no goals
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
⊢ Function.Surjective ↑f → Epi f
Tactic:
intro (h : Function.Surjective (toCompHaus.map f))
Proof state after:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Function.Surjective ↑(toCompHaus.map f)
⊢ Epi f
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Function.Surjective ↑(toCompHaus.map f)
⊢ Epi f
Tactic:
rw [← CompHaus.epi_iff_surjective] at h
Proof state after:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Epi (toCompHaus.map f)
⊢ Epi f
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mpr
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Epi (toCompHaus.map f)
⊢ Epi f
Tactic:
constructor
Proof state after:
case mpr.left_cancellation
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Epi (toCompHaus.map f)
⊢ ∀ {Z : ExtrDisc} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mpr.left_cancellation
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h : Epi (toCompHaus.map f)
⊢ ∀ {Z : ExtrDisc} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
Tactic:
intro W a b h
Proof state after:
case mpr.left_cancellation
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : f ≫ a = f ≫ b
⊢ a = b
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mpr.left_cancellation
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : f ≫ a = f ≫ b
⊢ a = b
Tactic:
apply Functor.map_injective toCompHaus
Proof state after:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : f ≫ a = f ≫ b
⊢ toCompHaus.map a = toCompHaus.map b
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : f ≫ a = f ≫ b
⊢ toCompHaus.map a = toCompHaus.map b
Tactic:
apply_fun toCompHaus.map at h
Proof state after:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : toCompHaus.map (f ≫ a) = toCompHaus.map (f ≫ b)
⊢ toCompHaus.map a = toCompHaus.map b
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : toCompHaus.map (f ≫ a) = toCompHaus.map (f ≫ b)
⊢ toCompHaus.map a = toCompHaus.map b
Tactic:
simp only [Functor.map_comp] at h
Proof state after:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : toCompHaus.map f ≫ toCompHaus.map a = toCompHaus.map f ≫ toCompHaus.map b
⊢ toCompHaus.map a = toCompHaus.map b
Theorem: ExtrDisc.epi_iff_surjective
Proof state before:
case mpr.left_cancellation.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X✝ : α → ExtrDisc
π : (a : α) → X✝ a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
X Y : ExtrDisc
f : X ⟶ Y
h✝ : Epi (toCompHaus.map f)
W : ExtrDisc
a b : Y ⟶ W
h : toCompHaus.map f ≫ toCompHaus.map a = toCompHaus.map f ≫ toCompHaus.map b
⊢ toCompHaus.map a = toCompHaus.map b
Tactic:
rwa [← cancel_epi (toCompHaus.map f)]
Proof state after:
no goals
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
⊢ ∀ {Z : CompHaus} (a₁ a₂ : α) (g₁ : Z ⟶ F.obj (X a₁)) (g₂ : Z ⟶ F.obj (X a₂)),
    g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Tactic:
intro Z a₁ a₂ g₁ g₂ hg
Proof state after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
Tactic:
let βZ := Z.presentation
Proof state after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
Tactic:
let g₁' := F.preimage (Z.presentationπ ≫ g₁ : F.obj βZ ⟶ F.obj (X a₁))
Proof state after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
Tactic:
let g₂' := F.preimage (Z.presentationπ ≫ g₂ : F.obj βZ ⟶ F.obj (X a₂))
Proof state after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂
Tactic:
apply Epi.left_cancellation (f := Z.presentationπ)
Proof state after:
case a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ CompHaus.presentationπ Z ≫ g₁ ≫ e a₁ = CompHaus.presentationπ Z ≫ g₂ ≫ e a₂
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
case a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ CompHaus.presentationπ Z ≫ g₁ ≫ e a₁ = CompHaus.presentationπ Z ≫ g₂ ≫ e a₂
Tactic:
change g₁' ≫ e a₁ = g₂' ≫ e a₂
Proof state after:
case a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ g₁' ≫ e a₁ = g₂' ≫ e a₂
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
case a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ g₁' ≫ e a₁ = g₂' ≫ e a₂
Tactic:
apply h
Proof state after:
case a.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ g₁' ≫ π a₁ = g₂' ≫ π a₂
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
case a.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ g₁' ≫ π a₁ = g₂' ≫ π a₂
Tactic:
change CompHaus.presentationπ Z ≫ g₁ ≫ π a₁ = CompHaus.presentationπ Z ≫ g₂ ≫ π a₂
Proof state after:
case a.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ CompHaus.presentationπ Z ≫ g₁ ≫ π a₁ = CompHaus.presentationπ Z ≫ g₂ ≫ π a₂
Theorem: ExtrDisc.EffectiveEpiFamily.helper
Proof state before:
case a.a
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
surj : ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
W : ExtrDisc
e : (a : α) → X a ⟶ W
h : ∀ {Z : ExtrDisc} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : CompHaus
a₁ a₂ : α
g₁ : Z ⟶ F.obj (X a₁)
g₂ : Z ⟶ F.obj (X a₂)
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
βZ : ExtrDisc := CompHaus.presentation Z
g₁' : βZ ⟶ X a₁ := F.preimage (CompHaus.presentationπ Z ≫ g₁)
g₂' : βZ ⟶ X a₂ := F.preimage (CompHaus.presentationπ Z ≫ g₂)
⊢ CompHaus.presentationπ Z ≫ g₁ ≫ π a₁ = CompHaus.presentationπ Z ≫ g₂ ≫ π a₂
Tactic:
simp [hg]
Proof state after:
no goals
Theorem: ExtrDisc.effectiveEpiFamily_tfae
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b]
Tactic:
tfae_have 1 → 2
Proof state after:
case tfae_1_to_2
α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
⊢ EffectiveEpiFamily X π → Epi (Sigma.desc π)

α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b]
Theorem: ExtrDisc.effectiveEpiFamily_tfae
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b]
Tactic:
tfae_have 1 → 2
Proof state after:
case tfae_1_to_2
α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ EffectiveEpiFamily X π → Epi (Sigma.desc π)

α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b]
Theorem: ExtrDisc.effectiveEpiFamily_tfae
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b]
Tactic:
tfae_have 2 → 3
Proof state after:
case tfae_2_to_3
α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
⊢ Epi (Sigma.desc π) → ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b

α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b]
Theorem: ExtrDisc.effectiveEpiFamily_tfae
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b]
Tactic:
tfae_have 3 → 1
Proof state after:
case tfae_3_to_1
α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
⊢ (∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b) → EffectiveEpiFamily X π

α✝ : Type
inst✝¹ : Fintype α✝
B✝ : ExtrDisc
X✝ : α✝ → ExtrDisc
π✝ : (a : α✝) → X✝ a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π✝ a) x = b
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
tfae_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
tfae_2_to_3 : Epi (Sigma.desc π) → ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
tfae_3_to_1 : (∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b) → EffectiveEpiFamily X π
⊢ TFAE [EffectiveEpiFamily X π, Epi (Sigma.desc π), ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b]