internlm/Lean-Github huggingface dataset:
Theorem: ExtrDisc.effectiveEpiFamily_tfae
Proof state before:
case tfae_2_to_3.intro.w.mk
α✝ : 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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
a : α
⊢ π a = (finiteCoproduct.cocone X).ι.app { as := a } ≫ finiteCoproduct.desc X π
Tactic:
ext
Proof state after:
case tfae_2_to_3.intro.w.mk.w
α✝ : 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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
a : α
x✝ : (forget ExtrDisc).obj (X a)
⊢ ↑(π a) x✝ = ↑((finiteCoproduct.cocone X).ι.app { as := a } ≫ finiteCoproduct.desc X π) x✝
Theorem: ExtrDisc.effectiveEpiFamily_tfae
Proof state before:
case tfae_2_to_3.intro.w.mk.w
α✝ : 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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
this : t = ↑i.inv (↑i.hom t)
a : α
x✝ : (forget ExtrDisc).obj (X a)
⊢ ↑(π a) x✝ = ↑((finiteCoproduct.cocone X).ι.app { as := a } ≫ finiteCoproduct.desc X π) x✝
Tactic:
rfl
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_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
⊢ t = ↑(i.hom ≫ i.inv) t
Tactic:
simp only [i.hom_inv_id]
Proof state after:
α✝ : 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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
⊢ t = ↑(𝟙 (∐ X)) t
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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
⊢ t = ↑(𝟙 (∐ X)) t
Tactic:
rfl
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_1_to_2✝ tfae_1_to_2 : EffectiveEpiFamily X π → Epi (Sigma.desc π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
this✝ : t = ↑i.inv (↑i.hom t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ ↑(π q.fst) q.snd = ↑(i.inv ≫ Sigma.desc π) (↑i.hom t)
Tactic:
rw [this]
Proof state after:
α✝ : 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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
this✝ : t = ↑i.inv (↑i.hom t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ ↑(π q.fst) q.snd = ↑(finiteCoproduct.desc X π) (↑i.hom t)
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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
t : CoeSort.coe (∐ fun b => X b)
q : (fun x => CoeSort.coe (finiteCoproduct X)) t := ↑i.hom t
this✝ : t = ↑i.inv (↑i.hom t)
this : i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
⊢ ↑(π q.fst) q.snd = ↑(finiteCoproduct.desc X π) (↑i.hom t)
Tactic:
rfl
Proof state after:
no goals
Theorem: ExtrDisc.effectiveEpiFamily_tfae
Proof state before:
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 π
Tactic:
apply effectiveEpiFamily_of_jointly_surjective
Proof state after:
no goals
Theorem: CompHaus.toFiniteCoproductCompFromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
ext
Proof state after:
case h.w
α : Type
inst✝ : Fintype α
Z : α → CompHaus
b✝ : α
x✝ : (forget CompHaus).obj (Z b✝)
⊢ ↑(Sigma.ι Z b✝ ≫ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z) x✝ = ↑(Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)) x✝
Theorem: CompHaus.toFiniteCoproductCompFromFiniteCoproduct
Proof state before:
case h.w
α : Type
inst✝ : Fintype α
Z : α → CompHaus
b✝ : α
x✝ : (forget CompHaus).obj (Z b✝)
⊢ ↑(Sigma.ι Z b✝ ≫ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z) x✝ = ↑(Sigma.ι Z b✝ ≫ 𝟙 (∐ Z)) x✝
Tactic:
simp [toFiniteCoproduct, fromFiniteCoproduct]
Proof state after:
no goals
Theorem: CompHaus.FromFiniteCoproductComptToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
Proof state after:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
⊢ finiteCoproduct.ι Z a ≫ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a ≫ 𝟙 (finiteCoproduct Z)
Theorem: CompHaus.FromFiniteCoproductComptToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
⊢ finiteCoproduct.ι Z a ≫ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a ≫ 𝟙 (finiteCoproduct Z)
Tactic:
simp [toFiniteCoproduct, fromFiniteCoproduct]
Proof state after:
no goals
Theorem: CompHaus.IsIsotoFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
simp
Proof state after:
no goals
Theorem: CompHaus.IsIsotoFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
simp
Proof state after:
no goals
Theorem: CompHaus.IsIsofromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
⊢ fromFiniteCoproduct Z ≫ toFiniteCoproduct Z = 𝟙 (finiteCoproduct Z)
Tactic:
simp
Proof state after:
no goals
Theorem: CompHaus.IsIsofromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
⊢ toFiniteCoproduct Z ≫ fromFiniteCoproduct Z = 𝟙 (∐ Z)
Tactic:
simp
Proof state after:
no goals
Theorem: CompHaus.Sigma.ιCompToFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
⊢ Sigma.ι Z a ≫ toFiniteCoproduct Z = finiteCoproduct.ι Z a
Tactic:
simp [toFiniteCoproduct]
Proof state after:
no goals
Theorem: CompHaus.finiteCoproduct.ιCompFromFiniteCoproduct
Proof state before:
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
⊢ ι Z a ≫ fromFiniteCoproduct Z = Sigma.ι Z a
Tactic:
simp [fromFiniteCoproduct]
Proof state after:
no goals
Theorem: CompHaus.finiteCoproduct.ι_injective
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
⊢ Function.Injective ↑(ι Z a)
Tactic:
intro x y hxy
Proof state after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
x y : (forget CompHaus).obj (Z a)
hxy : ↑(ι Z a) x = ↑(ι Z a) y
⊢ x = y
Theorem: CompHaus.finiteCoproduct.ι_injective
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a : α
x y : (forget CompHaus).obj (Z a)
hxy : ↑(ι Z a) x = ↑(ι Z a) y
⊢ x = y
Tactic:
exact eq_of_heq (Sigma.ext_iff.mp hxy).2
Proof state after:
no goals
Theorem: CompHaus.finiteCoproduct.ι_jointly_surjective
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
R : ↑(finiteCoproduct Z).toTop
⊢ ∃ a r, R = ↑(ι Z a) r
Tactic:
exact ⟨R.fst, R.snd, rfl⟩
Proof state after:
no goals
Theorem: CompHaus.finiteCoproduct.ι_desc_apply
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
a : α
⊢ ∀ (x : (forget CompHaus).obj (Z a)), ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x
Tactic:
intro x
Proof state after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
a : α
x : (forget CompHaus).obj (Z a)
⊢ ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x
Theorem: CompHaus.finiteCoproduct.ι_desc_apply
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
a : α
x : (forget CompHaus).obj (Z a)
⊢ ↑(desc Z π) (↑(ι Z a) x) = ↑(π a) x
Tactic:
change (ι Z a ≫ desc Z π) _ = _
Proof state after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
a : α
x : (forget CompHaus).obj (Z a)
⊢ ↑(ι Z a ≫ desc Z π) x = ↑(π a) x
Theorem: CompHaus.finiteCoproduct.ι_desc_apply
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
a : α
x : (forget CompHaus).obj (Z a)
⊢ ↑(ι Z a ≫ desc Z π) x = ↑(π a) x
Tactic:
simp only [ι_desc]
Proof state after:
no goals
Theorem: CompHaus.finiteCoproduct.range_eq
Proof state before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
a b : α
h : a = b
⊢ Set.range ↑(ι Z a) = Set.range ↑(ι Z b)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: CompHaus.toExplicitCompFromExcplict
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ toExplicit f i ≫ fromExplicit f i = 𝟙 (Limits.pullback f i)
Tactic:
refine' Limits.pullback.hom_ext (k := (toExplicit f i ≫ fromExplicit f i)) _ _
Proof state after:
case refine'_1
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.fst = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.fst

case refine'_2
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.snd = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.snd
Theorem: CompHaus.toExplicitCompFromExcplict
Proof state before:
case refine'_1
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.fst = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.fst
Tactic:
simp [toExplicit, fromExplicit]
Proof state after:
no goals
Theorem: CompHaus.toExplicitCompFromExcplict
Proof state before:
case refine'_2
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ (toExplicit f i ≫ fromExplicit f i) ≫ Limits.pullback.snd = 𝟙 (Limits.pullback f i) ≫ Limits.pullback.snd
Tactic:
rw [Category.id_comp, Category.assoc, fromExplicit, Limits.pullback.lift_snd,
  toExplicit, pullback.lift_snd]
Proof state after:
no goals
Theorem: CompHaus.fromExcplictComptoExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ (fromExplicit f i ≫ toExplicit f i) ≫ pullback.fst f i = 𝟙 (pullback f i) ≫ pullback.fst f i
Tactic:
simp [toExplicit, fromExplicit]
Proof state after:
no goals
Theorem: CompHaus.fromExcplictComptoExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ (fromExplicit f i ≫ toExplicit f i) ≫ pullback.snd f i = 𝟙 (pullback f i) ≫ pullback.snd f i
Tactic:
simp [toExplicit, fromExplicit]
Proof state after:
no goals
Theorem: CompHaus.fst_comp_fromExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ pullback.fst f i = fromExplicit f i ≫ Limits.pullback.fst
Tactic:
dsimp [fromExplicit]
Proof state after:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ pullback.fst f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.fst
Theorem: CompHaus.fst_comp_fromExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ pullback.fst f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.fst
Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
Proof state after:
no goals
Theorem: CompHaus.snd_comp_fromExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ pullback.snd f i = fromExplicit f i ≫ Limits.pullback.snd
Tactic:
dsimp [fromExplicit]
Proof state after:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ pullback.snd f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.snd
Theorem: CompHaus.snd_comp_fromExplicit
Proof state before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ pullback.snd f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.snd
Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
Proof state after:
no goals
Theorem: CompHaus.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let ζ := finiteCoproduct.desc _ (fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a )
Proof state after:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Theorem: CompHaus.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let σ := finiteCoproduct.desc _ ((fun a => pullback.fst f (π a)))
Proof state after:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Theorem: CompHaus.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
let β := finiteCoproduct.desc _ π
Proof state after:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Theorem: CompHaus.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
have comm : ζ ≫ β = σ ≫ f := by
   refine' finiteCoproduct.hom_ext _ _ _ (fun a => _)
   simp [← Category.assoc, finiteCoproduct.ι_desc, pullback.condition]
Proof state after:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Theorem: CompHaus.extensivity_injective
Proof state before:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
⊢ Function.Injective ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a))
Tactic:
intro R₁ R₂ hR
Proof state after:
α : Type
inst✝ : Fintype α
X : CompHaus
Z : α → CompHaus
π : (a : α) → Z a ⟶ X
Y : CompHaus
f : Y ⟶ X
HIso : IsIso (finiteCoproduct.desc (fun a => Z a) π)
ζ : (finiteCoproduct fun a => pullback f (π a)) ⟶ finiteCoproduct Z :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.snd f (π a) ≫ finiteCoproduct.ι Z a
σ : (finiteCoproduct fun a => pullback f (π a)) ⟶ Y :=
  finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)
β : (finiteCoproduct fun a => Z a) ⟶ X := finiteCoproduct.desc (fun a => Z a) π
comm : ζ ≫ β = σ ≫ f
R₁ R₂ : (forget CompHaus).obj (finiteCoproduct fun a => pullback f (π a))
hR :
  ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₁ =
    ↑(finiteCoproduct.desc (fun a => pullback f (π a)) fun a => pullback.fst f (π a)) R₂
⊢ R₁ = R₂