Theorem: ExtrDisc.finiteCoproduct.hom_ext (ExtrDisc/Basic.lean)

State before:
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
⊢ f = g
Tactic:
ext ⟨a,x⟩
State after:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : CoeSort.coe (X a)
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }

State before:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
h : ∀ (a : α), ι X a ≫ f = ι X a ≫ g
a : α
x : CoeSort.coe (X a)
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
specialize h a
State after:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }

State before:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ι X a ≫ f = ι X a ≫ g
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
apply_fun (fun q => q x) at h
State after:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }

State before:
case w.mk
α : Type
inst✝ : Fintype α
B✝ : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B✝
surj : ∀ (b : CoeSort.coe B✝), ∃ a x, ↑(π a) x = b
B : ExtrDisc
f g : finiteCoproduct X ⟶ B
a : α
x : CoeSort.coe (X a)
h : ↑(ι X a ≫ f) x = ↑(ι X a ≫ g) x
⊢ ↑f { fst := a, snd := x } = ↑g { fst := a, snd := x }
Tactic:
exact h
State after:
no goals