internlm/Lean-Github huggingface dataset:
Theorem: Term.algebra_freelyGenerated
Proof 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]
Proof 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 σ
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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 _
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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]
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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⟩
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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]
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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✝)
Theorem: Term.algebra_freelyGenerated
Proof 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 _]
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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 _]
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof 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]
Proof 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)
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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)
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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)
Theorem: Term.algebra_freelyGenerated
Proof 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]
Proof 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)
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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)
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof 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)
Theorem: Term.algebra_freelyGenerated
Proof 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
Proof state after:
no goals
Theorem: Term.pos_var
Proof state before:
Δ : RankedAlphabet
H : Type
v : H
⊢ Vars Δ H (var v)
Tactic:
simp [Vars]
Proof state after:
no goals
Theorem: Term.pos_zero
Proof state before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ Hom.hom pos (app σ (Vector.ε' h)) = Set.singleton Word.ε
Tactic:
simp [pos_app (H := H) σ (Vector.ε' h)]
Proof state after:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ (fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) =
    Set.singleton Word.ε
Theorem: Term.pos_zero
Proof state before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ (fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) =
    Set.singleton Word.ε
Tactic:
refine Set.mem_ext ?_
Proof state after:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ ∀ (a : Nat⋆),
    (a ∈ fun x =>
        match x with
        | [] => True
        | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
      a ∈ Set.singleton Word.ε
Theorem: Term.pos_zero
Proof state before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
⊢ ∀ (a : Nat⋆),
    (a ∈ fun x =>
        match x with
        | [] => True
        | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
      a ∈ Set.singleton Word.ε
Tactic:
intro w
Proof state after:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
    w ∈ Set.singleton Word.ε
Theorem: Term.pos_zero
Proof state before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) ↔
    w ∈ Set.singleton Word.ε
Tactic:
constructor
Proof state after:
case mp
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) →
    w ∈ Set.singleton Word.ε

case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ w ∈ Set.singleton Word.ε →
    w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })
Theorem: Term.pos_zero
Proof state before:
case mp
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ (w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })) →
    w ∈ Set.singleton Word.ε

case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
⊢ w ∈ Set.singleton Word.ε →
    w ∈ fun x =>
      match x with
      | [] => True
      | i :: tl => ∃ h_1, tl ∈ Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 })
Tactic:
all_goals
  intro h'
  simp [Set.singleton, Membership.mem] at *
Proof state after:
case mp
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' :
  match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl
⊢ w = Word.ε

case mpr
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w = Word.ε
⊢ match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl
Theorem: Term.pos_zero
Proof state before:
Δ : RankedAlphabet
H : Type
σ : Δ.alphabet
h : RankedAlphabet.rank Δ σ = 0
w : Nat⋆
h' : w = Word.ε
⊢ match w with
  | [] => True
  | i :: tl => ∃ h_1, Hom.hom pos (Vector.ε' h { val := i, isLt := h_1 }) tl
Tactic:
case mpr => simp [h']
Proof state after:
no goals