Theorem: ExtrDisc.EffectiveEpiFamily.helper (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
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
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₂

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

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₁))
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₂

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

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π)
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₂

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

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

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

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