Theorem: Term.algebra_freelyGenerated (WTA.lean)

State before:
Δ : RankedAlphabet
H : Type
⊢ ∀ (c : (Term.algebra Δ H).carrier), c ∈ closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
intro c
State after:
Δ : RankedAlphabet
H : Type
c : (Term.algebra Δ H).carrier
⊢ c ∈ closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))

State before:
Δ : RankedAlphabet
H : Type
c : (Term.algebra Δ H).carrier
⊢ c ∈ closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
simp [closure]
State after:
Δ : RankedAlphabet
H : Type
c : (Term.algebra Δ H).carrier
⊢ c ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))

State before:
Δ : RankedAlphabet
H : Type
c : (Term.algebra Δ H).carrier
⊢ c ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
induction c
State after:
case var
Δ : RankedAlphabet
H : Type
h✝ : H
⊢ var h✝ ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))

case app
Δ : RankedAlphabet
H : Type
σ✝ : Δ.alphabet
v✝ : Fin (RankedAlphabet.rank Δ σ✝) → Term Δ H
v_ih✝ : ∀ (a : Fin (RankedAlphabet.rank Δ σ✝)), v✝ a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ app σ✝ v✝ ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))

State before:
Δ : RankedAlphabet
H : Type
h : H
⊢ var h ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
case var h => 
  apply Closure.root 
  simp [Membership.mem, Vars]
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
v : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), v a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ app σ v ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
case app σ v hi =>
  refine Closure.app ?_ hi
  simp [Term.algebra, Algebra.ops, Membership.mem]
  exists σ, rfl
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
h : H
⊢ var h ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
apply Closure.root
State after:
case a
Δ : RankedAlphabet
H : Type
h : H
⊢ var h ∈ Vars Δ H

State before:
case a
Δ : RankedAlphabet
H : Type
h : H
⊢ var h ∈ Vars Δ H
Tactic:
simp [Membership.mem, Vars]
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
v : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), v a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ app σ v ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
refine Closure.app ?_ hi
State after:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
v : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), v a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ { fst := RankedAlphabet.rank Δ σ, snd := app σ } ∈ Algebra.ops (Term.algebra Δ H)

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
v : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), v a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ { fst := RankedAlphabet.rank Δ σ, snd := app σ } ∈ Algebra.ops (Term.algebra Δ H)
Tactic:
simp [Term.algebra, Algebra.ops, Membership.mem]
State after:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
v : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), v a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ ∃ σ_1 h, app σ_1 = (_ : RankedAlphabet.rank Δ σ = RankedAlphabet.rank Δ σ_1) ▸ app σ

State before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
v : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), v a ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
⊢ ∃ σ_1 h, app σ_1 = (_ : RankedAlphabet.rank Δ σ = RankedAlphabet.rank Δ σ_1) ▸ app σ
Tactic:
exists σ, rfl
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
⊢ ∀ (alg' : Algebra Δ) (f : { a // Vars Δ H a } → alg'.carrier),
    alg' ∈ Set.univ → ExistsUnique fun hom => ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
Tactic:
intro target f _
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ExistsUnique fun hom => ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ExistsUnique fun hom => ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
Tactic:
simp [ExistsUnique]
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∃ x,
    (∀ (c : { a // Vars Δ H a }), f c = Hom.hom x c.val) ∧
      ∀ (y : Hom (Term.algebra Δ H) target), (∀ (c : { a // Vars Δ H a }), f c = Hom.hom y c.val) → y = x

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∃ x,
    (∀ (c : { a // Vars Δ H a }), f c = Hom.hom x c.val) ∧
      ∀ (y : Hom (Term.algebra Δ H) target), (∀ (c : { a // Vars Δ H a }), f c = Hom.hom y c.val) → y = x
Tactic:
exists algebraHom target f
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ (∀ (c : { a // Vars Δ H a }), f c = Hom.hom (Term.algebraHom target f) c.val) ∧
    ∀ (y : Hom (Term.algebra Δ H) target),
      (∀ (c : { a // Vars Δ H a }), f c = Hom.hom y c.val) → y = Term.algebraHom target f

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ (∀ (c : { a // Vars Δ H a }), f c = Hom.hom (Term.algebraHom target f) c.val) ∧
    ∀ (y : Hom (Term.algebra Δ H) target),
      (∀ (c : { a // Vars Δ H a }), f c = Hom.hom y c.val) → y = Term.algebraHom target f
Tactic:
constructor
State after:
case left
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∀ (c : { a // Vars Δ H a }), f c = Hom.hom (Term.algebraHom target f) c.val

case right
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∀ (y : Hom (Term.algebra Δ H) target),
    (∀ (c : { a // Vars Δ H a }), f c = Hom.hom y c.val) → y = Term.algebraHom target f

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∀ (c : { a // Vars Δ H a }), f c = Hom.hom (Term.algebraHom target f) c.val
Tactic:
case left =>
  intro ⟨v, hv⟩
  cases v
  case app => contradiction
  case var => simp [algebraHom, algebraHomImpl]
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∀ (y : Hom (Term.algebra Δ H) target),
    (∀ (c : { a // Vars Δ H a }), f c = Hom.hom y c.val) → y = Term.algebraHom target f
Tactic:
case right =>
  intro hom h
  apply Hom.ext
  funext c
  induction c
  case a.h.var => simp [algebraHom, algebraHomImpl, h _]
  case a.h.app σ cs hi =>
    simp [algebraHom, algebraHomImpl]
    have h := hom.property σ cs
    simp [Term.algebra] at h
    simp [h]
    congr
    funext i
    exact hi i
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∀ (c : { a // Vars Δ H a }), f c = Hom.hom (Term.algebraHom target f) c.val
Tactic:
intro ⟨v, hv⟩
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
v : (Term.algebra Δ H).carrier
hv : Vars Δ H v
⊢ f { val := v, property := hv } = Hom.hom (Term.algebraHom target f) { val := v, property := hv }.val

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
v : (Term.algebra Δ H).carrier
hv : Vars Δ H v
⊢ f { val := v, property := hv } = Hom.hom (Term.algebraHom target f) { val := v, property := hv }.val
Tactic:
cases v
State after:
case var
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
h✝ : H
hv : Vars Δ H (var h✝)
⊢ f { val := var h✝, property := hv } = Hom.hom (Term.algebraHom target f) { val := var h✝, property := hv }.val

case app
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
σ✝ : Δ.alphabet
v✝ : Fin (RankedAlphabet.rank Δ σ✝) → Term Δ H
hv : Vars Δ H (app σ✝ v✝)
⊢ f { val := app σ✝ v✝, property := hv } = Hom.hom (Term.algebraHom target f) { val := app σ✝ v✝, property := hv }.val

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
σ✝ : Δ.alphabet
v✝ : Fin (RankedAlphabet.rank Δ σ✝) → Term Δ H
hv : Vars Δ H (app σ✝ v✝)
⊢ f { val := app σ✝ v✝, property := hv } = Hom.hom (Term.algebraHom target f) { val := app σ✝ v✝, property := hv }.val
Tactic:
case app => contradiction
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
h✝ : H
hv : Vars Δ H (var h✝)
⊢ f { val := var h✝, property := hv } = Hom.hom (Term.algebraHom target f) { val := var h✝, property := hv }.val
Tactic:
case var => simp [algebraHom, algebraHomImpl]
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
σ✝ : Δ.alphabet
v✝ : Fin (RankedAlphabet.rank Δ σ✝) → Term Δ H
hv : Vars Δ H (app σ✝ v✝)
⊢ f { val := app σ✝ v✝, property := hv } = Hom.hom (Term.algebraHom target f) { val := app σ✝ v✝, property := hv }.val
Tactic:
contradiction
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
h✝ : H
hv : Vars Δ H (var h✝)
⊢ f { val := var h✝, property := hv } = Hom.hom (Term.algebraHom target f) { val := var h✝, property := hv }.val
Tactic:
simp [algebraHom, algebraHomImpl]
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
⊢ ∀ (y : Hom (Term.algebra Δ H) target),
    (∀ (c : { a // Vars Δ H a }), f c = Hom.hom y c.val) → y = Term.algebraHom target f
Tactic:
intro hom h
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
⊢ hom = Term.algebraHom target f

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
⊢ hom = Term.algebraHom target f
Tactic:
apply Hom.ext
State after:
case a
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
⊢ hom.hom = (Term.algebraHom target f).hom

State before:
case a
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
⊢ hom.hom = (Term.algebraHom target f).hom
Tactic:
funext c
State after:
case a.h
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
c : (Term.algebra Δ H).carrier
⊢ Hom.hom hom c = Hom.hom (Term.algebraHom target f) c

State before:
case a.h
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
c : (Term.algebra Δ H).carrier
⊢ Hom.hom hom c = Hom.hom (Term.algebraHom target f) c
Tactic:
induction c
State after:
case a.h.var
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
h✝ : H
⊢ Hom.hom hom (var h✝) = Hom.hom (Term.algebraHom target f) (var h✝)

case a.h.app
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ✝ : Δ.alphabet
v✝ : Fin (RankedAlphabet.rank Δ σ✝) → Term Δ H
v_ih✝ : ∀ (a : Fin (RankedAlphabet.rank Δ σ✝)), Hom.hom hom (v✝ a) = Hom.hom (Term.algebraHom target f) (v✝ a)
⊢ Hom.hom hom (app σ✝ v✝) = Hom.hom (Term.algebraHom target f) (app σ✝ v✝)

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
h✝ : H
⊢ Hom.hom hom (var h✝) = Hom.hom (Term.algebraHom target f) (var h✝)
Tactic:
case a.h.var => simp [algebraHom, algebraHomImpl, h _]
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
⊢ Hom.hom hom (app σ cs) = Hom.hom (Term.algebraHom target f) (app σ cs)
Tactic:
case a.h.app σ cs hi =>
  simp [algebraHom, algebraHomImpl]
  have h := hom.property σ cs
  simp [Term.algebra] at h
  simp [h]
  congr
  funext i
  exact hi i
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
h✝ : H
⊢ Hom.hom hom (var h✝) = Hom.hom (Term.algebraHom target f) (var h✝)
Tactic:
simp [algebraHom, algebraHomImpl, h _]
State after:
no goals

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
⊢ Hom.hom hom (app σ cs) = Hom.hom (Term.algebraHom target f) (app σ cs)
Tactic:
simp [algebraHom, algebraHomImpl]
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
⊢ Hom.hom hom (app σ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
⊢ Hom.hom hom (app σ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)
Tactic:
have h := hom.property σ cs
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (Algebra.θ (Term.algebra Δ H) σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ Hom.hom hom (app σ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (Algebra.θ (Term.algebra Δ H) σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ Hom.hom hom (app σ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)
Tactic:
simp [Term.algebra] at h
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ Hom.hom hom (app σ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ Hom.hom hom (app σ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)
Tactic:
simp [h]
State after:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ Algebra.θ target σ (hom.hom ∘ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)

State before:
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ Algebra.θ target σ (hom.hom ∘ cs) = Algebra.θ target σ fun x => Term.algebraHomImpl target f (cs x)
Tactic:
congr
State after:
case e_a
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ hom.hom ∘ cs = fun x => Term.algebraHomImpl target f (cs x)

State before:
case e_a
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
⊢ hom.hom ∘ cs = fun x => Term.algebraHomImpl target f (cs x)
Tactic:
funext i
State after:
case e_a.h
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
i : Fin (RankedAlphabet.rank Δ σ)
⊢ Function.comp hom.hom cs i = Term.algebraHomImpl target f (cs i)

State before:
case e_a.h
Δ : RankedAlphabet
H : Type
target : Algebra Δ
f : { a // Vars Δ H a } → target.carrier
a✝ : target ∈ Set.univ
hom : Hom (Term.algebra Δ H) target
h✝ : ∀ (c : { a // Vars Δ H a }), f c = Hom.hom hom c.val
σ : Δ.alphabet
cs : Fin (RankedAlphabet.rank Δ σ) → Term Δ H
hi : ∀ (a : Fin (RankedAlphabet.rank Δ σ)), Hom.hom hom (cs a) = Hom.hom (Term.algebraHom target f) (cs a)
h : Hom.hom hom (app σ cs) = Algebra.θ target σ (hom.hom ∘ cs)
i : Fin (RankedAlphabet.rank Δ σ)
⊢ Function.comp hom.hom cs i = Term.algebraHomImpl target f (cs i)
Tactic:
exact hi i
State after:
no goals