internlm/Lean-Github huggingface dataset:
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inr.inl
a b : Nat
h : b = a
⊢ Nat.max a b = Nat.max b a
Tactic:
rw [max_of_eq h, max_of_eq' h.symm]
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_comm
Proof state before:
case inr.inr
a b : Nat
h : b < a
⊢ Nat.max a b = Nat.max b a
Tactic:
rw [max_of_lt h, max_of_gt h]
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
⊢ ∀ (a b c : Nat), Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
intros a b c
Proof state after:
a b c : Nat
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
a b c : Nat
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
cases Nat.lt_or_ge a b
<;> cases Nat.lt_or_ge b c
<;> rename_i ab bc
Proof state after:
case inl.inl
a b c : Nat
ab : a < b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inl.inl
a b c : Nat
ab : a < b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
. rw [max_of_lt ab, max_of_lt bc, max_of_lt (trans ab bc)]
Proof state after:
case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
. rw [max_of_lt ab, max_of_ge bc, max_of_lt ab]
Proof state after:
case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)

case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
. rw [max_of_ge ab, max_of_lt bc]
Proof state after:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
. rw [max_of_ge ab, max_of_ge bc, max_of_ge ab]
  exact max_of_ge (trans bc ab : c ≤ a)
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inl.inl
a b c : Nat
ab : a < b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
rw [max_of_lt ab, max_of_lt bc, max_of_lt (trans ab bc)]
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inl.inr
a b c : Nat
ab : a < b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
rw [max_of_lt ab, max_of_ge bc, max_of_lt ab]
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inr.inl
a b c : Nat
ab : a ≥ b
bc : b < c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
rw [max_of_ge ab, max_of_lt bc]
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Tactic:
rw [max_of_ge ab, max_of_ge bc, max_of_ge ab]
Proof state after:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max a c = a
Theorem: Mt.Utils.Nat.max_assoc
Proof state before:
case inr.inr
a b c : Nat
ab : a ≥ b
bc : b ≥ c
⊢ Nat.max a c = a
Tactic:
exact max_of_ge (trans bc ab : c ≤ a)
Proof state after:
no goals
Theorem: Mt.Utils.Nat.zero_max
Proof state before:
⊢ ∀ (a : Nat), Nat.max 0 a = a
Tactic:
intro a
Proof state after:
a : Nat
⊢ Nat.max 0 a = a
Theorem: Mt.Utils.Nat.zero_max
Proof state before:
a : Nat
⊢ Nat.max 0 a = a
Tactic:
simp only [Nat.max, Nat.zero_le, ite_true]
Proof state after:
a : Nat
⊢ max 0 a = a
Theorem: Mt.Utils.Nat.max_le
Proof state before:
a b c : Nat
⊢ Nat.max a b ≤ c ↔ a ≤ c ∧ b ≤ c
Tactic:
constructor <;> intro h
<;> (cases Nat.lt_or_ge a b) <;> rename_i ab
Proof state after:
case mp.inl
a b c : Nat
h : Nat.max a b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c

case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mp.inl
a b c : Nat
h : Nat.max a b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c

case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
. rw [max_of_lt ab] at h
  exact ⟨Nat.le_of_lt (trans ab h), h⟩
Proof state after:
case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c

case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
. rw [max_of_ge ab] at h
  exact ⟨h, trans ab h⟩
Proof state after:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
. rw [max_of_lt ab]
  exact h.right
Proof state after:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
. rw [max_of_ge ab]
  exact h.left
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mpr
a b c : Nat
h : a ≤ c ∧ b ≤ c
⊢ Nat.max a b ≤ c
Tactic:
cases Nat.lt_or_ge a b
Proof state after:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
h✝ : a < b
⊢ Nat.max a b ≤ c

case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
h✝ : a ≥ b
⊢ Nat.max a b ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mp.inl
a b c : Nat
h : Nat.max a b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c
Tactic:
rw [max_of_lt ab] at h
Proof state after:
case mp.inl
a b c : Nat
h : b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mp.inl
a b c : Nat
h : b ≤ c
ab : a < b
⊢ a ≤ c ∧ b ≤ c
Tactic:
exact ⟨Nat.le_of_lt (trans ab h), h⟩
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mp.inr
a b c : Nat
h : Nat.max a b ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c
Tactic:
rw [max_of_ge ab] at h
Proof state after:
case mp.inr
a b c : Nat
h : a ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mp.inr
a b c : Nat
h : a ≤ c
ab : a ≥ b
⊢ a ≤ c ∧ b ≤ c
Tactic:
exact ⟨h, trans ab h⟩
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ Nat.max a b ≤ c
Tactic:
rw [max_of_lt ab]
Proof state after:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ b ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mpr.inl
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a < b
⊢ b ≤ c
Tactic:
exact h.right
Proof state after:
no goals
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ Nat.max a b ≤ c
Tactic:
rw [max_of_ge ab]
Proof state after:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ a ≤ c
Theorem: Mt.Utils.Nat.max_le
Proof state before:
case mpr.inr
a b c : Nat
h : a ≤ c ∧ b ≤ c
ab : a ≥ b
⊢ a ≤ c
Tactic:
exact h.left
Proof state after:
no goals
Theorem: const_func_ext
Proof state before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
⊢ ((fun x => a) = fun x => b) → a = b
Tactic:
intro h
Proof state after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
⊢ a = b
Theorem: const_func_ext
Proof state before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
⊢ a = b
Tactic:
have ha : (fun _ : α => a) (choice inferInstance) = a := rfl
Proof state after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
⊢ a = b
Theorem: const_func_ext
Proof state before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
⊢ a = b
Tactic:
have hb : (fun _ : α => b) (choice inferInstance) = b := rfl
Proof state after:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
hb : (fun x => b) (choice (_ : Nonempty α)) = b
⊢ a = b
Theorem: const_func_ext
Proof state before:
α : Sort u_1
β : Sort u_2
inst✝ : Nonempty α
a b : β
h : (fun x => a) = fun x => b
ha : (fun x => a) (choice (_ : Nonempty α)) = a
hb : (fun x => b) (choice (_ : Nonempty α)) = b
⊢ a = b
Tactic:
rw [←ha, ←hb, h]
Proof state after:
no goals
Theorem: Set.mem_singleton
Proof state before:
α✝ : Type u_1
a : α✝
⊢ a ∈ singleton a
Tactic:
simp [singleton, Membership.mem]
Proof state after:
no goals
Theorem: Word.ε_mem_prefixes
Proof state before:
α : Type
u : α⋆
⊢ ε ∈ prefixes u
Tactic:
induction u
Proof state after:
case nil
α : Type
⊢ ε ∈ prefixes []

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : ε ∈ prefixes tail✝
⊢ ε ∈ prefixes (head✝ :: tail✝)
Theorem: Word.ε_mem_prefixes
Proof state before:
α : Type
⊢ ε ∈ prefixes []
Tactic:
case nil => simp [prefixes, Set.mem_singleton]
Proof state after:
no goals
Theorem: Word.ε_mem_prefixes
Proof state before:
α : Type
i : α
v : List α
hi : ε ∈ prefixes v
⊢ ε ∈ prefixes (i :: v)
Tactic:
case cons i v hi => 
  simp [prefixes] 
  simp [Membership.mem] at *
  exact hi
Proof state after:
no goals
Theorem: Word.ε_mem_prefixes
Proof state before:
α : Type
⊢ ε ∈ prefixes []
Tactic:
simp [prefixes, Set.mem_singleton]
Proof state after:
no goals
Theorem: Word.ε_mem_prefixes
Proof state before:
α : Type
i : α
v : List α
hi : ε ∈ prefixes v
⊢ ε ∈ prefixes (i :: v)
Tactic:
simp [prefixes]
Proof state after:
α : Type
i : α
v : List α
hi : ε ∈ prefixes v
⊢ ε ∈ fun u => u = i⬝v ∨ u ∈ prefixes v
Theorem: Word.ε_mem_prefixes
Proof state before:
α : Type
i : α
v : List α
hi : ε ∈ prefixes v
⊢ ε ∈ fun u => u = i⬝v ∨ u ∈ prefixes v
Tactic:
simp [Membership.mem] at *
Proof state after:
α : Type
i : α
v : List α
hi : prefixes v ε
⊢ prefixes v ε
Theorem: Word.ε_mem_prefixes
Proof state before:
α : Type
i : α
v : List α
hi : prefixes v ε
⊢ prefixes v ε
Tactic:
exact hi
Proof state after:
no goals
Theorem: Algebra.carrier_closed
Proof state before:
Δ : RankedAlphabet
alg : Algebra Δ
⊢ Closed alg Set.univ
Tactic:
simp [Closed, Set.mem_univ]
Proof state after:
no goals
Theorem: Hom.ext
Proof state before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom₁ hom₂ : Hom alg₁ alg₂
⊢ hom₁.hom = hom₂.hom → hom₁ = hom₂
Tactic:
intro h
Proof state after:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom₁ hom₂ : Hom alg₁ alg₂
h : hom₁.hom = hom₂.hom
⊢ hom₁ = hom₂
Theorem: Hom.ext
Proof state before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom₁ hom₂ : Hom alg₁ alg₂
h : hom₁.hom = hom₂.hom
⊢ hom₁ = hom₂
Tactic:
cases hom₁ <;> cases hom₂
Proof 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✝ }
Theorem: Hom.ext
Proof 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
Proof 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✝ }
Theorem: Hom.ext
Proof 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]
Proof state after:
no goals
Theorem: lemma_2_6_2
Proof state before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
⊢ Closed alg₂ (Set.image hom.hom)
Tactic:
intro σ cs₂
Proof state after:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
⊢ Algebra.θ alg₂ σ (Vector.lift cs₂) ∈ Set.image hom.hom
Theorem: lemma_2_6_2
Proof state before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
⊢ Algebra.θ alg₂ σ (Vector.lift cs₂) ∈ Set.image hom.hom
Tactic:
simp [Closed, Set.mem_image_iff]
Proof state after:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
⊢ ∃ a, Hom.hom hom a = Algebra.θ alg₂ σ (Vector.lift cs₂)
Theorem: lemma_2_6_2
Proof state before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
⊢ ∃ a, Hom.hom hom a = Algebra.θ alg₂ σ (Vector.lift cs₂)
Tactic:
have h := hom.property σ cs₁
Proof state after:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ ∃ a, Hom.hom hom a = Algebra.θ alg₂ σ (Vector.lift cs₂)
Theorem: lemma_2_6_2
Proof state before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ ∃ a, Hom.hom hom a = Algebra.θ alg₂ σ (Vector.lift cs₂)
Tactic:
exists alg₁.θ σ cs₁
Proof state after:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (Vector.lift cs₂)
Theorem: lemma_2_6_2
Proof state before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (Vector.lift cs₂)
Tactic:
rw [h]
Proof state after:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ Algebra.θ alg₂ σ (hom.hom ∘ cs₁) = Algebra.θ alg₂ σ (Vector.lift cs₂)
Theorem: lemma_2_6_2
Proof state before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ Algebra.θ alg₂ σ (hom.hom ∘ cs₁) = Algebra.θ alg₂ σ (Vector.lift cs₂)
Tactic:
congr
Proof state after:
case e_a
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ hom.hom ∘ cs₁ = Vector.lift cs₂
Theorem: lemma_2_6_2
Proof state before:
case e_a
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ hom.hom ∘ cs₁ = Vector.lift cs₂
Tactic:
funext i
Proof state after:
case e_a.h
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
i : Fin (RankedAlphabet.rank Δ✝ σ)
⊢ Function.comp hom.hom cs₁ i = Vector.lift cs₂ i
Theorem: lemma_2_6_2
Proof state before:
case e_a.h
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
i : Fin (RankedAlphabet.rank Δ✝ σ)
⊢ Function.comp hom.hom cs₁ i = Vector.lift cs₂ i
Tactic:
apply Set.image_choose
Proof state after:
no goals
Theorem: BinOp.Identity.unique
Proof state before:
α : Type
e e' : α
op : BinOp α
⊢ Identity op e → Identity op e' → e = e'
Tactic:
intro h h'
Proof state after:
α : Type
e e' : α
op : BinOp α
h : Identity op e
h' : Identity op e'
⊢ e = e'
Theorem: BinOp.Identity.unique
Proof state before:
α : Type
e e' : α
op : BinOp α
h : Identity op e
h' : Identity op e'
⊢ e = e'
Tactic:
rw [←h'.left e, h.right e']
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof state before:
Δ : RankedAlphabet
H : Type
⊢ ∀ (c : (Term.algebra Δ H).carrier), c ∈ closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
intro c
Proof state after:
Δ : RankedAlphabet
H : Type
c : (Term.algebra Δ H).carrier
⊢ c ∈ closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Theorem: Term.algebra_freelyGenerated
Proof state before:
Δ : RankedAlphabet
H : Type
c : (Term.algebra Δ H).carrier
⊢ c ∈ closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
simp [closure]
Proof state after:
Δ : RankedAlphabet
H : Type
c : (Term.algebra Δ H).carrier
⊢ c ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Theorem: Term.algebra_freelyGenerated
Proof state before:
Δ : RankedAlphabet
H : Type
c : (Term.algebra Δ H).carrier
⊢ c ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
induction c
Proof 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))
Theorem: Term.algebra_freelyGenerated
Proof 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]
Proof state after:
no goals
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))
⊢ 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
Proof state after:
no goals
Theorem: Term.algebra_freelyGenerated
Proof state before:
Δ : RankedAlphabet
H : Type
h : H
⊢ var h ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
apply Closure.root
Proof state after:
case a
Δ : RankedAlphabet
H : Type
h : H
⊢ var h ∈ Vars Δ H
Theorem: Term.algebra_freelyGenerated
Proof state before:
case a
Δ : RankedAlphabet
H : Type
h : H
⊢ var h ∈ Vars Δ H
Tactic:
simp [Membership.mem, Vars]
Proof state after:
no goals
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))
⊢ app σ v ∈ Closure (Vars Δ H) (Algebra.ops (Term.algebra Δ H))
Tactic:
refine Closure.app ?_ hi
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))
⊢ { fst := RankedAlphabet.rank Δ σ, snd := app σ } ∈ Algebra.ops (Term.algebra Δ H)