Theorem: ExtrDisc.effectiveEpiFamily_tfae (ExtrDisc/Epi.lean)

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
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]

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
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]

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
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]

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
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]

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_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]
Tactic:
tfae_finish
State after:
no goals

State before:
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 π)
Tactic:
intro
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 π)

State before:
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 π)
Tactic:
infer_instance
State after:
no goals

State before:
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 π)
Tactic:
intro
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 π)

State before:
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 π)
Tactic:
infer_instance
State after:
no goals

State before:
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
Tactic:
intro e
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 π)
e : Epi (Sigma.desc π)
⊢ ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b

State before:
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 π)
e : Epi (Sigma.desc π)
⊢ ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
Tactic:
rw [epi_iff_surjective] at e
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 π)
e : Function.Surjective ↑(Sigma.desc π)
⊢ ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b

State before:
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 π)
e : Function.Surjective ↑(Sigma.desc π)
⊢ ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
Tactic:
let i : ∐ X ≅ finiteCoproduct X :=
  (colimit.isColimit _).coconePointUniqueUpToIso (finiteCoproduct.isColimit _)
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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
⊢ ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b

State before:
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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
⊢ ∀ (b : CoeSort.coe B), ∃ a x, ↑(π a) x = b
Tactic:
intro b
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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
b : CoeSort.coe B
⊢ ∃ a x, ↑(π a) x = b

State before:
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 π)
e : Function.Surjective ↑(Sigma.desc π)
i : ∐ X ≅ finiteCoproduct X :=
  IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Discrete.functor X)) (finiteCoproduct.isColimit X)
b : CoeSort.coe B
⊢ ∃ a x, ↑(π a) x = b
Tactic:
obtain ⟨t,rfl⟩ := e b
State after:
case tfae_2_to_3.intro
α✝ : 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)
⊢ ∃ a x, ↑(π a) x = ↑(Sigma.desc π) t

State before:
case tfae_2_to_3.intro
α✝ : 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)
⊢ ∃ a x, ↑(π a) x = ↑(Sigma.desc π) t
Tactic:
let q := i.hom t
State after:
case tfae_2_to_3.intro
α✝ : 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
⊢ ∃ a x, ↑(π a) x = ↑(Sigma.desc π) t

State before:
case tfae_2_to_3.intro
α✝ : 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
⊢ ∃ a x, ↑(π a) x = ↑(Sigma.desc π) t
Tactic:
refine ⟨q.1,q.2,?_⟩
State after:
case tfae_2_to_3.intro
α✝ : 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
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) t

State before:
case tfae_2_to_3.intro
α✝ : 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
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) t
Tactic:
have : t = i.inv (i.hom t) := show t = (i.hom ≫ i.inv) t by simp only [i.hom_inv_id] ; rfl
State after:
case tfae_2_to_3.intro
α✝ : 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)
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) t

State before:
case tfae_2_to_3.intro
α✝ : 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)
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) t
Tactic:
rw [this]
State after:
case tfae_2_to_3.intro
α✝ : 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)
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) (↑i.inv (↑i.hom t))

State before:
case tfae_2_to_3.intro
α✝ : 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)
⊢ ↑(π q.fst) q.snd = ↑(Sigma.desc π) (↑i.inv (↑i.hom t))
Tactic:
show _ = (i.inv ≫ Sigma.desc π) (i.hom t)
State after:
case tfae_2_to_3.intro
α✝ : 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)
⊢ ↑(π q.fst) q.snd = ↑(i.inv ≫ Sigma.desc π) (↑i.hom t)

State before:
case tfae_2_to_3.intro
α✝ : 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)
⊢ ↑(π q.fst) q.snd = ↑(i.inv ≫ Sigma.desc π) (↑i.hom t)
Tactic:
suffices i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π by
  rw [this] ; rfl
State after:
case tfae_2_to_3.intro
α✝ : 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)
⊢ i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π

State before:
case tfae_2_to_3.intro
α✝ : 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)
⊢ i.inv ≫ Sigma.desc π = finiteCoproduct.desc X π
Tactic:
rw [Iso.inv_comp_eq]
State after:
case tfae_2_to_3.intro
α✝ : 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)
⊢ Sigma.desc π = i.hom ≫ finiteCoproduct.desc X π

State before:
case tfae_2_to_3.intro
α✝ : 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)
⊢ Sigma.desc π = i.hom ≫ finiteCoproduct.desc X π
Tactic:
apply colimit.hom_ext
State after:
case tfae_2_to_3.intro.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)
⊢ ∀ (j : Discrete α),
    colimit.ι (Discrete.functor X) j ≫ Sigma.desc π =
      colimit.ι (Discrete.functor X) j ≫ i.hom ≫ finiteCoproduct.desc X π

State before:
case tfae_2_to_3.intro.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)
⊢ ∀ (j : Discrete α),
    colimit.ι (Discrete.functor X) j ≫ Sigma.desc π =
      colimit.ι (Discrete.functor X) j ≫ i.hom ≫ finiteCoproduct.desc X π
Tactic:
rintro ⟨a⟩
State after:
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 : α
⊢ colimit.ι (Discrete.functor X) { as := a } ≫ Sigma.desc π =
    colimit.ι (Discrete.functor X) { as := a } ≫ i.hom ≫ finiteCoproduct.desc X π

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 : α
⊢ colimit.ι (Discrete.functor X) { as := a } ≫ Sigma.desc π =
    colimit.ι (Discrete.functor X) { as := a } ≫ i.hom ≫ finiteCoproduct.desc X π
Tactic:
simp only [Discrete.functor_obj, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app,
  colimit.comp_coconePointUniqueUpToIso_hom_assoc]
State after:
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 π

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
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✝

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
State after:
no goals

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]
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

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
State after:
no goals

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]
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)

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
State after:
no goals

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
State after:
no goals