awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R_1 : Type u_1
X : Type u_2
inst : CommSemiring R_1
R : Type u_3
S : Type u_4
A : Type u_5
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : CommSemiring A
inst_4 : SMul R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
e_a :
  (algebraMap S A : (a : S) → A) (r • s) =
    HSMul.hSMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap S A : (a : S) → A) s : A)
⊢ HSMul.hSMul (α := A) ((algebraMap S A : (a : S) → A) (r • s) : A) x =
    HSMul.hSMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap S A : (a : S) → A) s : A) • x

Tactic:
congr
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R_1 : Type u_1
X : Type u_2
inst : CommSemiring R_1
R : Type u_3
S : Type u_4
A : Type u_5
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : CommSemiring A
inst_4 : SMul R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
e_a : HSMul.hSMul (β := A) (r • s) 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1
⊢ (algebraMap S A : (a : S) → A) (r • s) =
    HSMul.hSMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap S A : (a : S) → A) s : A)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_eq_mul]

Premises used: Algebra.algebraMap_eq_smul_one, smul_eq_mul
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R_1 : Type u_1
X : Type u_2
inst : CommSemiring R_1
R : Type u_3
S : Type u_4
A : Type u_5
inst_1 : CommSemiring R
inst_2 : CommSemiring S
inst_3 : CommSemiring A
inst_4 : SMul R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
e_a : r • HSMul.hSMul (β := A) s 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1
e_a₁ e_a₂ : HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1
⊢ HSMul.hSMul (β := A) (r • s) 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1

Tactic:
rw [smul_assoc, ← smul_one_mul]

Premises used: smul_assoc, smul_one_mul
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Type
inst_1 : CommRing S
⊢ Eq.{u_2 + 1} (α := Algebra ℤ (FreeAlgebra S X)) (Ring.toIntAlgebra (FreeAlgebra S X)) (instAlgebra ℤ X)

Tactic:
rfl

Premises used: FreeAlgebra, Quot.map, rfl
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
m : X
rw rw₁ : Quot.mk (Rel R X) (Pre.of m) = Quot.mk (Rel R X) (Pre.of m)
⊢ Quot.mk (Rel R X) (Pre.of m) = ι R m

Tactic:
rw [ι_def]

Premises used: FreeAlgebra.ι_def
-- Module: Mathlib.Algebra.FreeAlgebra
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)
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)
⊢ liftFun R X f a = liftFun R X f b

Tactic:
induction h
-- Module: Mathlib.Algebra.FreeAlgebra
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
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))

Tactic:
(algebraMap R A).map_add _ _

Premises used: Algebra.algebraMap, FreeAlgebra.liftFun, RingHom.map_add
-- Module: Mathlib.Algebra.FreeAlgebra
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
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))

Tactic:
exact (algebraMap R A).map_add _ _

Premises used: Algebra.algebraMap, RingHom.map_add
-- Module: Mathlib.Algebra.FreeAlgebra
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
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))

Tactic:
(algebraMap R A).map_mul _ _

Premises used: Algebra.algebraMap, FreeAlgebra.liftFun, RingHom.map_mul
-- Module: Mathlib.Algebra.FreeAlgebra
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
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))

Tactic:
exact (algebraMap R A).map_mul _ _

Premises used: Algebra.algebraMap, RingHom.map_mul
-- Module: Mathlib.Algebra.FreeAlgebra
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
r : R
a_2 : Pre R X
⊢ liftFun R X f (Pre.ofScalar r * a_2) = liftFun R X f (a_2 * Pre.ofScalar r)

Tactic:
apply Algebra.commutes

Premises used: Algebra.commutes
-- Module: Mathlib.Algebra.FreeAlgebra
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
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)
⊢ liftFun R X f (a_2 + b_1 + c) = liftFun R X f (a_2 + (b_1 + c))

Tactic:
change _ + _ + _ = _ + (_ + _)

Premises used: HAdd.hAdd
-- Module: Mathlib.Algebra.FreeAlgebra
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
add_assoc 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)
⊢ 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]

Premises used: add_assoc
-- Module: Mathlib.Algebra.FreeAlgebra
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
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
⊢ liftFun R X f (a_2 + b_1) = liftFun R X f (b_1 + a_2)

Tactic:
change _ + _ = _ + _
-- Module: Mathlib.Algebra.FreeAlgebra
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
add_comm 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
⊢ 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:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.FreeAlgebra
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
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
⊢ liftFun R X f (0 + a_2) = liftFun R X f a_2

Tactic:
change algebraMap _ _ _ + liftFun R X f _ = liftFun R X f _

Premises used: Algebra.algebraMap, FreeAlgebra.liftFun, DFunLike.coe
-- Module: Mathlib.Algebra.FreeAlgebra
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
⊢ HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) 0 : A) (liftFun R X f a_2) = liftFun R X f a_2

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
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
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)
⊢ liftFun R X f (a_2 * b_1 * c) = liftFun R X f (a_2 * (b_1 * c))

Tactic:
change _ * _ * _ = _ * (_ * _)

Premises used: HMul.hMul
-- Module: Mathlib.Algebra.FreeAlgebra
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
mul_assoc 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)
⊢ 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]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.FreeAlgebra
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
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
⊢ liftFun R X f (1 * a_2) = liftFun R X f a_2

Tactic:
change algebraMap _ _ _ * liftFun R X f _ = liftFun R X f _

Premises used: Algebra.algebraMap, FreeAlgebra.liftFun, DFunLike.coe
-- Module: Mathlib.Algebra.FreeAlgebra
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
⊢ HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) 1 : A) (liftFun R X f a_2) = liftFun R X f a_2

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
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
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
⊢ liftFun R X f (a_2 * 1) = liftFun R X f a_2

Tactic:
change liftFun R X f _ * algebraMap _ _ _ = liftFun R X f _

Premises used: Algebra.algebraMap, FreeAlgebra.liftFun, DFunLike.coe
-- Module: Mathlib.Algebra.FreeAlgebra
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
⊢ HMul.hMul (β := A) (liftFun R X f a_2) ((algebraMap R A : (a : R) → A) 1 : A) = liftFun R X f a_2

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
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
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
⊢ liftFun R X f (a_2 * (b_1 + c)) = liftFun R X f (a_2 * b_1 + a_2 * c)

Tactic:
change _ * (_ + _) = _ * _ + _ * _

Premises used: HAdd.hAdd
-- Module: Mathlib.Algebra.FreeAlgebra
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
left_distrib 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
⊢ 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:
rw [left_distrib]

Premises used: left_distrib
-- Module: Mathlib.Algebra.FreeAlgebra
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
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
⊢ liftFun R X f ((a_2 + b_1) * c) = liftFun R X f (a_2 * c + b_1 * c)

Tactic:
change (_ + _) * _ = _ * _ + _ * _

Premises used: HAdd.hAdd
-- Module: Mathlib.Algebra.FreeAlgebra
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
right_distrib 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
⊢ (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:
rw [right_distrib]

Premises used: right_distrib
-- Module: Mathlib.Algebra.FreeAlgebra
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
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
⊢ liftFun R X f (0 * a_2) = liftFun R X f 0

Tactic:
change algebraMap _ _ _ * _ = algebraMap _ _ _

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.FreeAlgebra
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
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
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
⊢ liftFun R X f (a_2 * 0) = liftFun R X f 0

Tactic:
change _ * algebraMap _ _ _ = algebraMap _ _ _

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.FreeAlgebra
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
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
add_compat_left : liftFun R X f a_2 + liftFun R X f c = liftFun R X f (b_1 + c)
⊢ liftFun R X f (a_2 + c) = liftFun R X f (b_1 + c)

Tactic:
change liftFun R X f _ + liftFun R X f _ = _

Premises used: FreeAlgebra.liftFun
-- Module: Mathlib.Algebra.FreeAlgebra
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
add_compat_left : liftFun R X f b_1 + liftFun R X f c = liftFun R X f (b_1 + c)
⊢ liftFun R X f a_2 + liftFun R X f c = liftFun R X f (b_1 + c)

Tactic:
simp only [*]
-- Module: Mathlib.Algebra.FreeAlgebra
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 b_1 + liftFun R X f c = liftFun R X f (b_1 + c)

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeAlgebra
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
add_compat_right : liftFun R X f c + liftFun R X f a_2 = liftFun R X f (c + b_1)
⊢ liftFun R X f (c + a_2) = liftFun R X f (c + b_1)

Tactic:
change liftFun R X f _ + liftFun R X f _ = _

Premises used: FreeAlgebra.liftFun
-- Module: Mathlib.Algebra.FreeAlgebra
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
add_compat_right : liftFun R X f c + liftFun R X f b_1 = liftFun R X f (c + b_1)
⊢ liftFun R X f c + liftFun R X f a_2 = liftFun R X f (c + b_1)

Tactic:
simp only [*]
-- Module: Mathlib.Algebra.FreeAlgebra
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 b_1 = liftFun R X f (c + b_1)

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeAlgebra
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
mul_compat_left : liftFun R X f a_2 * liftFun R X f c = liftFun R X f (b_1 * c)
⊢ liftFun R X f (a_2 * c) = liftFun R X f (b_1 * c)

Tactic:
change liftFun R X f _ * liftFun R X f _ = _

Premises used: FreeAlgebra.liftFun
-- Module: Mathlib.Algebra.FreeAlgebra
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
mul_compat_left : liftFun R X f b_1 * liftFun R X f c = liftFun R X f (b_1 * c)
⊢ liftFun R X f a_2 * liftFun R X f c = liftFun R X f (b_1 * c)

Tactic:
simp only [*]
-- Module: Mathlib.Algebra.FreeAlgebra
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 b_1 * liftFun R X f c = liftFun R X f (b_1 * c)

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeAlgebra
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
mul_compat_right : liftFun R X f c * liftFun R X f a_2 = liftFun R X f (c * b_1)
⊢ liftFun R X f (c * a_2) = liftFun R X f (c * b_1)

Tactic:
change liftFun R X f _ * liftFun R X f _ = _

Premises used: FreeAlgebra.liftFun
-- Module: Mathlib.Algebra.FreeAlgebra
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
mul_compat_right : liftFun R X f c * liftFun R X f b_1 = liftFun R X f (c * b_1)
⊢ liftFun R X f c * liftFun R X f a_2 = liftFun R X f (c * b_1)

Tactic:
simp only [*]
-- Module: Mathlib.Algebra.FreeAlgebra
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 b_1 = liftFun R X f (c * b_1)

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeAlgebra
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
mul_compat_left : liftFun R X f a_2 * liftFun R X f c = liftFun R X f (b_1 * c)
mul_compat_left₁ : liftFun R X f b_1 * liftFun R X f c = liftFun R X f (b_1 * c)
⊢ liftFun R X f (a_2 * c) = liftFun R X f (b_1 * c)

Tactic:
repeat
        change liftFun R X f _ * liftFun R X f _ = _
        simp only [*]
        rfl

Premises used: FreeAlgebra.liftFun
-- Module: Mathlib.Algebra.FreeAlgebra
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
change : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) 1 : A) (1 : A)
⊢ Quot.liftOn (r := Rel R X) 1 (liftFun R X f) ⋯ = 1

Tactic:
change algebraMap _ _ _ = _

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.FreeAlgebra
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
⊢ Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) 1 : A) (1 : A)

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
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
x : FreeAlgebra R X
a : Pre R X
y : FreeAlgebra R X
a_1 : Pre R X
⊢ Quot.liftOn (r := Rel R X) (Quot.mk (Rel R X) a * Quot.mk (Rel R X) a_1) (liftFun R X f) ⋯ =
    (Quot.mk (Rel R X) a).liftOn (r := Rel R X) (liftFun R X f) ⋯ *
      (Quot.mk (Rel R X) a_1).liftOn (r := Rel R X) (liftFun R X f) ⋯

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeAlgebra
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
change : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) 0 : A) (0 : A)
⊢ Quot.liftOn (r := Rel R X) 0 (liftFun R X f) ⋯ = 0

Tactic:
change algebraMap _ _ _ = _

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.Algebra.FreeAlgebra
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
⊢ Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) 0 : A) (0 : A)

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
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
x : FreeAlgebra R X
a : Pre R X
y : FreeAlgebra R X
a_1 : Pre R X
⊢ Quot.liftOn (r := Rel R X) (Quot.mk (Rel R X) a + Quot.mk (Rel R X) a_1) (liftFun R X f) ⋯ =
    (Quot.mk (Rel R X) a).liftOn (r := Rel R X) (liftFun R X f) ⋯ +
      (Quot.mk (Rel R X) a_1).liftOn (r := Rel R X) (liftFun R X f) ⋯

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeAlgebra
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
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ :
  ∀ (r : R),
    Quot.liftOn (r := Rel R X) ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r) (liftFun R X f) ⋯ =
      (algebraMap R A : (a : R) → A) r
⊢ ∀ (r : R),
    Quot.liftOn (r := Rel R X) ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r) (liftFun R X f) ⋯ =
      (algebraMap R A : (a : R) → A) r

Tactic:
tauto