awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Nonempty X
inst_2 : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₂ :
  max (Cardinal.lift.{u, v} #(FreeMonoid X)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₃ :
  max (Cardinal.lift.{u, v} (max #X ℵ₀)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₄ :
  max (max (Cardinal.lift.{u, v} #X) (Cardinal.lift.{u, v} ℵ₀)) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₅ :
  max (max (Cardinal.lift.{u, v} #X) ℵ₀) (Cardinal.lift.{v, u} #R) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
rw₆ :
  max (Cardinal.lift.{v, u} #R) (max (Cardinal.lift.{u, v} #X) ℵ₀) =
    max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have rw₇ : max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀ =
  max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra,
    mk_finsupp_lift_of_infinite, hX, lift_max, lift_aleph0, sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : IsEmpty X
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R
have this : Cardinal.lift.{u, max u v} #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{max u v, u} #R
Tactic: have := lift_mk_eq'.2 ⟨show (FreeMonoid X →₀ R) ≃ R from Finsupp.uniqueEquiv 1⟩
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : IsEmpty X
this : Cardinal.lift.{u, max u v} #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{max u v, u} #R
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R
have this₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{v, u} #R
Tactic: rw [lift_id'.{u, v}, lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : IsEmpty X
this : #(Finsupp.{v, u} (FreeMonoid X) R) = Cardinal.lift.{v, u} #R
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R
have rwa : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = Cardinal.lift.{v, u} #R
Tactic: rwa [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Subsingleton R
⊢ #(FreeAlgebra R X) = 1
have rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = 1
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra, mk_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Subsingleton R
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = 1
⊢ #(FreeAlgebra R X) = 1
have rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = 1
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra, mk_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inst_1 : Subsingleton R
rw : #(MonoidAlgebra.{u, v} R (FreeMonoid X)) = 1
rw₁ : #(Finsupp.{v, u} (FreeMonoid X) R) = 1
⊢ #(FreeAlgebra R X) = 1
have rw₂ : Eq (α := Cardinal.{max v u}) 1 1
Tactic: rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra, mk_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have inl : Subsingleton R → #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
inl : Subsingleton R → #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have inr : Nontrivial R → #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
h : Nontrivial R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have inr : IsEmpty X → #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: cases isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
X : Type v
h : Nontrivial R
inr : IsEmpty X → #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
have inr₁ : Nonempty X → #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Tactic: cases isEmpty_or_nonempty X
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #(↑s : Type v))) ℵ₀
have H : lift.{max u v, v}
    #(↑(Set.range (ι := FreeAlgebra.{u, v} R { x : A // x ∈ s })
            (⇑((FreeAlgebra.lift R : (a : { x : A // x ∈ s } → A) → FreeAlgebra R { x : A // x ∈ s } →ₐ[R] A)
                    (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
                  FreeAlgebra.{u, v} R { x : A // x ∈ s } →ₐ[R] A) :
              (a : FreeAlgebra R { x : A // x ∈ s }) → A)) :
        Type v) ≤
  lift.{v, max u v} #(FreeAlgebra.{u, v} R { x : A // x ∈ s })
Tactic: have H := mk_range_le_lift (f := FreeAlgebra.lift R ((↑) : s → A))
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
H :
  lift.{max u v, v}
      #(↑(Set.range (ι := FreeAlgebra.{u, v} R { x : A // x ∈ s })
              (⇑((FreeAlgebra.lift R : (a : { x : A // x ∈ s } → A) → FreeAlgebra R { x : A // x ∈ s } →ₐ[R] A)
                      (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
                    FreeAlgebra.{u, v} R { x : A // x ∈ s } →ₐ[R] A) :
                (a : FreeAlgebra R { x : A // x ∈ s }) → A)) :
          Type v) ≤
    lift.{v, max u v} #(FreeAlgebra.{u, v} R { x : A // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #(↑s : Type v))) ℵ₀
have H₁ : lift.{u, v}
    #(↑(Set.range (ι := FreeAlgebra.{u, v} R { x : A // x ∈ s })
            (⇑((FreeAlgebra.lift R : (a : { x : A // x ∈ s } → A) → FreeAlgebra R { x : A // x ∈ s } →ₐ[R] A)
                    (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
                  FreeAlgebra.{u, v} R { x : A // x ∈ s } →ₐ[R] A) :
              (a : FreeAlgebra R { x : A // x ∈ s }) → A)) :
        Type v) ≤
  #(FreeAlgebra.{u, v} R { x : A // x ∈ s })
Tactic: rw [lift_umax, lift_id'.{v, u}] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra.Cardinality (goal)
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
H :
  lift.{u, v}
      #(↑(Set.range (ι := FreeAlgebra.{u, v} R { x : A // x ∈ s })
              (⇑((FreeAlgebra.lift R : (a : { x : A // x ∈ s } → A) → FreeAlgebra R { x : A // x ∈ s } →ₐ[R] A)
                      (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
                    FreeAlgebra.{u, v} R { x : A // x ∈ s } →ₐ[R] A) :
                (a : FreeAlgebra R { x : A // x ∈ s }) → A)) :
          Type v) ≤
    #(FreeAlgebra.{u, v} R { x : A // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #(↑s : Type v))) ℵ₀
have rw : lift.{u, v}
    #↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : A // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : A // x ∈ s } → A) → FreeAlgebra R { x : A // x ∈ s } →ₐ[R] A)
            (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) ≤
  max (max (lift.{v, u} #R) (lift.{u, v} #(↑s : Type v))) ℵ₀
Tactic: rw [Algebra.adjoin_eq_range_freeAlgebra_lift]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
⊢ Quot.mk (Rel R X) (a_1 + 0) = Quot.mk (Rel R X) a_1
have mk : Quot.mk (Rel R X) (0 + a_1) = Quot.mk (Rel R X) a_1
Tactic: rw [Quot.sound Rel.add_comm, Quot.sound Rel.zero_add]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
mk : Quot.mk (Rel R X) (0 + a_1) = Quot.mk (Rel R X) a_1
⊢ Quot.mk (Rel R X) (a_1 + 0) = Quot.mk (Rel R X) a_1
have mk₁ : Quot.mk (Rel R X) a_1 = Quot.mk (Rel R X) a_1
Tactic: rw [Quot.sound Rel.add_comm, Quot.sound Rel.zero_add]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
x : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (HMul.hMul (α := Pre R X) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) 0) : Pre R X) a) = 0
have mk : Quot.mk (Rel R X) (Pre.ofScalar 0 * a) = 0
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
n : ℕ
x : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (HMul.hMul (α := Pre R X) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) (n + 1)) : Pre R X) a) =
    Quot.mk (Rel R X) (HMul.hMul (α := Pre R X) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) n) : Pre R X) a) +
      Quot.mk (Rel R X) a
have mk : Quot.mk (Rel R X) (Pre.ofScalar (HAdd.hAdd (α := R) (β := R) ((algebraMap ℕ R : (a : ℕ) → R) n : R) (1 : R))) *
    Quot.mk (Rel R X) a =
  (Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) n)) + 1) * Quot.mk (Rel R X) a
Tactic: rw [map_add, map_one, mk_mul, mk_mul, ← add_one_mul (_ : FreeAlgebra R X)]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
n : ℕ
x : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar (HAdd.hAdd (α := R) (β := R) ((algebraMap ℕ R : (a : ℕ) → R) n : R) (1 : R))) *
      Quot.mk (Rel R X) a =
    (Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) n)) + 1) * Quot.mk (Rel R X) a
have mk : Quot.mk (Rel R X) (Pre.ofScalar (HAdd.hAdd (α := R) (β := R) ((algebraMap ℕ R : (a : ℕ) → R) n : R) (1 : R))) =
  Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) n)) + 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
⊢ Quot.mk (Rel R X) (Pre.ofScalar (↑0 : R)) = 0
have simp : Quot.mk (Rel R X) (Pre.ofScalar 0) = 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ (r • s) • x = r • s • x
have change : HSMul.hSMul (α := A) ((algebraMap S A : (a : S) → A) (r • s) : A) x =
  HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A)
    (HSMul.hSMul (α := A) ((algebraMap S A : (a : S) → A) s : A) x)
Tactic: change algebraMap S A (r • s) • x = algebraMap R A _ • (algebraMap S A _ • x)
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ HSMul.hSMul (α := A) ((algebraMap S A : (a : S) → A) (r • s) : A) x =
    HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) r : A)
      (HSMul.hSMul (α := A) ((algebraMap S A : (a : S) → A) s : A) x)
have rw : 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: rw [← smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ (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)
have e_a : HSMul.hSMul (β := A) (r • s) 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1
Tactic: simp only [Algebra.algebraMap_eq_smul_one, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ HSMul.hSMul (β := A) (r • s) 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1
have e_a : r • HSMul.hSMul (β := A) s 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1
Tactic: rw [smul_assoc, ← smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ HSMul.hSMul (β := A) (r • s) 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1
have e_a₁ : HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1 = HSMul.hSMul (β := A) r 1 * HSMul.hSMul (β := A) s 1
Tactic: rw [smul_assoc, ← smul_one_mul]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
m : X
⊢ Quot.mk (Rel R X) (Pre.of m) = ι R m
have rw : Quot.mk (Rel R X) (Pre.of m) = Quot.mk (Rel R X) (Pre.of m)
Tactic: rw [ι_def]
-- 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
⊢ liftFun R X f a = liftFun R X f b
have 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))
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))
⊢ liftFun R X f a = liftFun R X f b
have 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))
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))
⊢ liftFun R X f a = liftFun R X f b
have central_scalar : ∀ {r : R} {a : Pre R X}, liftFun R X f (Pre.ofScalar r * a) = liftFun R X f (a * Pre.ofScalar r)
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)
⊢ liftFun R X f a = liftFun R X f b
have add_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a + b + c) = liftFun R X f (a + (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))
⊢ liftFun R X f a = liftFun R X f b
have add_comm : ∀ {a b : Pre R X}, liftFun R X f (a + b) = liftFun R X f (b + a)
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)
⊢ liftFun R X f a = liftFun R X f b
have zero_add : ∀ {a : Pre R X}, liftFun R X f (0 + a) = liftFun R X f a
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
⊢ liftFun R X f a = liftFun R X f b
have mul_assoc : ∀ {a b c : Pre R X}, liftFun R X f (a * b * c) = liftFun R X f (a * (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))
⊢ liftFun R X f a = liftFun R X f b
have one_mul : ∀ {a : Pre R X}, liftFun R X f (1 * a) = liftFun R X f a
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
⊢ liftFun R X f a = liftFun R X f b
have mul_one : ∀ {a : Pre R X}, liftFun R X f (a * 1) = liftFun R X f a
Tactic: induction h
Cleared hypotheses: h