awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
add_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r + s)) = liftFun R X f (HAdd.hAdd (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
mul_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r * s)) = liftFun R X f (HMul.hMul (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (b + c))
add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (b * c))
one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
⊢ liftFun R X f a = liftFun R X f b
have left_distrib : ∀ {a b c : Pre R X}, liftFun R X f (a * (b + c)) = liftFun R X f (a * b + a * c)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
add_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r + s)) = liftFun R X f (HAdd.hAdd (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
mul_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r * s)) = liftFun R X f (HMul.hMul (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (b + c))
add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (b * c))
one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
left_distrib : ∀ {a b c : Pre R X}, liftFun R X f (a * (b + c)) = liftFun R X f (a * b + a * c)
⊢ liftFun R X f a = liftFun R X f b
have right_distrib : ∀ {a b c : Pre R X}, liftFun R X f ((a + b) * c) = liftFun R X f (a * c + b * c)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
add_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r + s)) = liftFun R X f (HAdd.hAdd (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
mul_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r * s)) = liftFun R X f (HMul.hMul (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (b + c))
add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (b * c))
one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
left_distrib : ∀ {a b c : Pre R X}, liftFun R X f (a * (b + c)) = liftFun R X f (a * b + a * c)
right_distrib : ∀ {a b c : Pre R X}, liftFun R X f ((a + b) * c) = liftFun R X f (a * c + b * c)
⊢ liftFun R X f a = liftFun R X f b
have zero_mul : ∀ {a : Pre R X}, liftFun R X f (0 * a) = liftFun R X f 0
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
add_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r + s)) = liftFun R X f (HAdd.hAdd (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
mul_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r * s)) = liftFun R X f (HMul.hMul (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (b + c))
add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (b * c))
one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
left_distrib : ∀ {a b c : Pre R X}, liftFun R X f (a * (b + c)) = liftFun R X f (a * b + a * c)
right_distrib : ∀ {a b c : Pre R X}, liftFun R X f ((a + b) * c) = liftFun R X f (a * c + b * c)
zero_mul : ∀ {a : Pre R X}, liftFun R X f (0 * a) = liftFun R X f 0
⊢ liftFun R X f a = liftFun R X f b
have mul_zero : ∀ {a : Pre R X}, liftFun R X f (a * 0) = liftFun R X f 0
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
add_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r + s)) = liftFun R X f (HAdd.hAdd (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
mul_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r * s)) = liftFun R X f (HMul.hMul (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (b + c))
add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (b * c))
one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
left_distrib : ∀ {a b c : Pre R X}, liftFun R X f (a * (b + c)) = liftFun R X f (a * b + a * c)
right_distrib : ∀ {a b c : Pre R X}, liftFun R X f ((a + b) * c) = liftFun R X f (a * c + b * c)
zero_mul : ∀ {a : Pre R X}, liftFun R X f (0 * a) = liftFun R X f 0
mul_zero : ∀ {a : Pre R X}, liftFun R X f (a * 0) = liftFun R X f 0
⊢ liftFun R X f a = liftFun R X f b
have add_compat_left : ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (a + c) = liftFun R X f (b + c)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
add_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r + s)) = liftFun R X f (HAdd.hAdd (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
mul_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r * s)) = liftFun R X f (HMul.hMul (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (b + c))
add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (b * c))
one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
left_distrib : ∀ {a b c : Pre R X}, liftFun R X f (a * (b + c)) = liftFun R X f (a * b + a * c)
right_distrib : ∀ {a b c : Pre R X}, liftFun R X f ((a + b) * c) = liftFun R X f (a * c + b * c)
zero_mul : ∀ {a : Pre R X}, liftFun R X f (0 * a) = liftFun R X f 0
mul_zero : ∀ {a : Pre R X}, liftFun R X f (a * 0) = liftFun R X f 0
add_compat_left :
  ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (a + c) = liftFun R X f (b + c)
⊢ liftFun R X f a = liftFun R X f b
have add_compat_right : ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (c + a) = liftFun R X f (c + b)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
add_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r + s)) = liftFun R X f (HAdd.hAdd (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
mul_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r * s)) = liftFun R X f (HMul.hMul (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (b + c))
add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (b * c))
one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
left_distrib : ∀ {a b c : Pre R X}, liftFun R X f (a * (b + c)) = liftFun R X f (a * b + a * c)
right_distrib : ∀ {a b c : Pre R X}, liftFun R X f ((a + b) * c) = liftFun R X f (a * c + b * c)
zero_mul : ∀ {a : Pre R X}, liftFun R X f (0 * a) = liftFun R X f 0
mul_zero : ∀ {a : Pre R X}, liftFun R X f (a * 0) = liftFun R X f 0
add_compat_left :
  ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (a + c) = liftFun R X f (b + c)
add_compat_right :
  ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (c + a) = liftFun R X f (c + b)
⊢ liftFun R X f a = liftFun R X f b
have mul_compat_left : ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (a * c) = liftFun R X f (b * c)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
add_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r + s)) = liftFun R X f (HAdd.hAdd (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
mul_scalar :
  ∀ {r s : R},
    liftFun R X f (Pre.ofScalar (r * s)) = liftFun R X f (HMul.hMul (α := Pre R X) (Pre.ofScalar r) (Pre.ofScalar s))
central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (b + c))
add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (b * c))
one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
left_distrib : ∀ {a b c : Pre R X}, liftFun R X f (a * (b + c)) = liftFun R X f (a * b + a * c)
right_distrib : ∀ {a b c : Pre R X}, liftFun R X f ((a + b) * c) = liftFun R X f (a * c + b * c)
zero_mul : ∀ {a : Pre R X}, liftFun R X f (0 * a) = liftFun R X f 0
mul_zero : ∀ {a : Pre R X}, liftFun R X f (a * 0) = liftFun R X f 0
add_compat_left :
  ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (a + c) = liftFun R X f (b + c)
add_compat_right :
  ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (c + a) = liftFun R X f (c + b)
mul_compat_left :
  ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (a * c) = liftFun R X f (b * c)
⊢ liftFun R X f a = liftFun R X f b
have mul_compat_right : ∀ {a b c : Pre R X}, Rel R X a b → liftFun R X f a = liftFun R X f b → liftFun R X f (c * a) = liftFun R X f (c * b)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
⊢ liftFun R X f (a_2 + b_1 + c) = liftFun R X f (a_2 + (b_1 + c))
have add_assoc : liftFun R X f a_2 + liftFun R X f b_1 + liftFun R X f c = liftFun R X f a_2 + (liftFun R X f b_1 + liftFun R X f c)
Tactic: change _ + _ + _ = _ + (_ + _)
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
⊢ liftFun R X f a_2 + liftFun R X f b_1 + liftFun R X f c = liftFun R X f a_2 + (liftFun R X f b_1 + liftFun R X f c)
have add_assoc : liftFun R X f a_2 + (liftFun R X f b_1 + liftFun R X f c) = liftFun R X f a_2 + (liftFun R X f b_1 + liftFun R X f c)
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 : Pre R X
⊢ liftFun R X f (a_2 + b_1) = liftFun R X f (b_1 + a_2)
have add_comm : liftFun R X f a_2 + liftFun R X f b_1 = liftFun R X f b_1 + liftFun R X f a_2
Tactic: change _ + _ = _ + _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 : Pre R X
⊢ liftFun R X f a_2 + liftFun R X f b_1 = liftFun R X f b_1 + liftFun R X f a_2
have add_comm : liftFun R X f b_1 + liftFun R X f a_2 = liftFun R X f b_1 + liftFun R X f a_2
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 : Pre R X
⊢ liftFun R X f (0 + a_2) = liftFun R X f a_2
have zero_add : HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) 0 : A) (liftFun R X f a_2) = liftFun R X f a_2
Tactic: change algebraMap _ _ _ + liftFun R X f _ = liftFun R X f _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
⊢ liftFun R X f (a_2 * b_1 * c) = liftFun R X f (a_2 * (b_1 * c))
have mul_assoc : liftFun R X f a_2 * liftFun R X f b_1 * liftFun R X f c = liftFun R X f a_2 * (liftFun R X f b_1 * liftFun R X f c)
Tactic: change _ * _ * _ = _ * (_ * _)
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
⊢ liftFun R X f a_2 * liftFun R X f b_1 * liftFun R X f c = liftFun R X f a_2 * (liftFun R X f b_1 * liftFun R X f c)
have mul_assoc : liftFun R X f a_2 * (liftFun R X f b_1 * liftFun R X f c) = liftFun R X f a_2 * (liftFun R X f b_1 * liftFun R X f c)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 : Pre R X
⊢ liftFun R X f (1 * a_2) = liftFun R X f a_2
have one_mul : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) 1 : A) (liftFun R X f a_2) = liftFun R X f a_2
Tactic: change algebraMap _ _ _ * liftFun R X f _ = liftFun R X f _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 : Pre R X
⊢ liftFun R X f (a_2 * 1) = liftFun R X f a_2
have mul_one : HMul.hMul (β := A) (liftFun R X f a_2) ((algebraMap R A : (a : R) → A) 1 : A) = liftFun R X f a_2
Tactic: change liftFun R X f _ * algebraMap _ _ _ = liftFun R X f _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
⊢ liftFun R X f (a_2 * (b_1 + c)) = liftFun R X f (a_2 * b_1 + a_2 * c)
have left_distrib : liftFun R X f a_2 * (liftFun R X f b_1 + liftFun R X f c) =
  liftFun R X f a_2 * liftFun R X f b_1 + liftFun R X f a_2 * liftFun R X f c
Tactic: change _ * (_ + _) = _ * _ + _ * _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
⊢ liftFun R X f a_2 * (liftFun R X f b_1 + liftFun R X f c) =
    liftFun R X f a_2 * liftFun R X f b_1 + liftFun R X f a_2 * liftFun R X f c
have left_distrib : liftFun R X f a_2 * liftFun R X f b_1 + liftFun R X f a_2 * liftFun R X f c =
  liftFun R X f a_2 * liftFun R X f b_1 + liftFun R X f a_2 * liftFun R X f c
Tactic: rw [left_distrib]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
⊢ liftFun R X f ((a_2 + b_1) * c) = liftFun R X f (a_2 * c + b_1 * c)
have right_distrib : (liftFun R X f a_2 + liftFun R X f b_1) * liftFun R X f c =
  liftFun R X f a_2 * liftFun R X f c + liftFun R X f b_1 * liftFun R X f c
Tactic: change (_ + _) * _ = _ * _ + _ * _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
⊢ (liftFun R X f a_2 + liftFun R X f b_1) * liftFun R X f c =
    liftFun R X f a_2 * liftFun R X f c + liftFun R X f b_1 * liftFun R X f c
have right_distrib : liftFun R X f a_2 * liftFun R X f c + liftFun R X f b_1 * liftFun R X f c =
  liftFun R X f a_2 * liftFun R X f c + liftFun R X f b_1 * liftFun R X f c
Tactic: rw [right_distrib]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 : Pre R X
⊢ liftFun R X f (0 * a_2) = liftFun R X f 0
have zero_mul : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) 0 : A) (liftFun R X f a_2) = (algebraMap R A : (a : R) → A) 0
Tactic: change algebraMap _ _ _ * _ = algebraMap _ _ _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 : Pre R X
⊢ liftFun R X f (a_2 * 0) = liftFun R X f 0
have mul_zero : HMul.hMul (β := A) (liftFun R X f a_2) ((algebraMap R A : (a : R) → A) 0 : A) = (algebraMap R A : (a : R) → A) 0
Tactic: change _ * algebraMap _ _ _ = algebraMap _ _ _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f (a_2 + c) = liftFun R X f (b_1 + c)
have add_compat_left : liftFun R X f a_2 + liftFun R X f c = liftFun R X f (b_1 + c)
Tactic: change liftFun R X f _ + liftFun R X f _ = _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f a_2 + liftFun R X f c = liftFun R X f (b_1 + c)
have add_compat_left : liftFun R X f b_1 + liftFun R X f c = liftFun R X f (b_1 + c)
Tactic: simp only [*]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f (c + a_2) = liftFun R X f (c + b_1)
have add_compat_right : liftFun R X f c + liftFun R X f a_2 = liftFun R X f (c + b_1)
Tactic: change liftFun R X f _ + liftFun R X f _ = _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f c + liftFun R X f a_2 = liftFun R X f (c + b_1)
have add_compat_right : liftFun R X f c + liftFun R X f b_1 = liftFun R X f (c + b_1)
Tactic: simp only [*]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f (a_2 * c) = liftFun R X f (b_1 * c)
have mul_compat_left : liftFun R X f a_2 * liftFun R X f c = liftFun R X f (b_1 * c)
Tactic: change liftFun R X f _ * liftFun R X f _ = _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f a_2 * liftFun R X f c = liftFun R X f (b_1 * c)
have mul_compat_left : liftFun R X f b_1 * liftFun R X f c = liftFun R X f (b_1 * c)
Tactic: simp only [*]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f (c * a_2) = liftFun R X f (c * b_1)
have mul_compat_right : liftFun R X f c * liftFun R X f a_2 = liftFun R X f (c * b_1)
Tactic: change liftFun R X f _ * liftFun R X f _ = _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f c * liftFun R X f a_2 = liftFun R X f (c * b_1)
have mul_compat_right : liftFun R X f c * liftFun R X f b_1 = liftFun R X f (c * b_1)
Tactic: simp only [*]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
⊢ liftFun R X f (a_2 * c) = liftFun R X f (b_1 * c)
have mul_compat_left : liftFun R X f a_2 * liftFun R X f c = liftFun R X f (b_1 * c)
Tactic: repeat
        change liftFun R X f _ * liftFun R X f _ = _
        simp only [*]
        rfl