Theorem: Hom.ext (WTA.lean)

State before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom₁ hom₂ : Hom alg₁ alg₂
⊢ hom₁.hom = hom₂.hom → hom₁ = hom₂
Tactic:
intro h
State after:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom₁ hom₂ : Hom alg₁ alg₂
h : hom₁.hom = hom₂.hom
⊢ hom₁ = hom₂

State before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom₁ hom₂ : Hom alg₁ alg₂
h : hom₁.hom = hom₂.hom
⊢ hom₁ = hom₂
Tactic:
cases hom₁ <;> cases hom₂
State after:
case mk.mk
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom✝¹ : alg₁.carrier → alg₂.carrier
property✝¹ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝¹ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝¹ ∘ cs)
hom✝ : alg₁.carrier → alg₂.carrier
property✝ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝ ∘ cs)
h : { hom := hom✝¹, property := property✝¹ }.hom = { hom := hom✝, property := property✝ }.hom
⊢ { hom := hom✝¹, property := property✝¹ } = { hom := hom✝, property := property✝ }

State before:
case mk.mk
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom✝¹ : alg₁.carrier → alg₂.carrier
property✝¹ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝¹ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝¹ ∘ cs)
hom✝ : alg₁.carrier → alg₂.carrier
property✝ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝ ∘ cs)
h : { hom := hom✝¹, property := property✝¹ }.hom = { hom := hom✝, property := property✝ }.hom
⊢ { hom := hom✝¹, property := property✝¹ } = { hom := hom✝, property := property✝ }
Tactic:
simp at h
State after:
case mk.mk
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom✝¹ : alg₁.carrier → alg₂.carrier
property✝¹ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝¹ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝¹ ∘ cs)
hom✝ : alg₁.carrier → alg₂.carrier
property✝ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝ ∘ cs)
h : hom✝¹ = hom✝
⊢ { hom := hom✝¹, property := property✝¹ } = { hom := hom✝, property := property✝ }

State before:
case mk.mk
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom✝¹ : alg₁.carrier → alg₂.carrier
property✝¹ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝¹ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝¹ ∘ cs)
hom✝ : alg₁.carrier → alg₂.carrier
property✝ :
  ∀ (σ : Δ✝.alphabet) (cs : alg₁.carrier⋆RankedAlphabet.rank Δ✝ σ),
    hom✝ (Algebra.θ alg₁ σ cs) = Algebra.θ alg₂ σ (hom✝ ∘ cs)
h : hom✝¹ = hom✝
⊢ { hom := hom✝¹, property := property✝¹ } = { hom := hom✝, property := property✝ }
Tactic:
simp [h]
State after:
no goals