awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
h : Subsingleton R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
(cardinalMk_eq_one R X).trans_le (le_max_of_le_right one_le_aleph0)

Premises used: Eq.trans_le, le_max_of_le_right, FreeAlgebra.cardinalMk_eq_one, Cardinal.one_le_aleph0
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
h : Subsingleton R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
exact (cardinalMk_eq_one R X).trans_le (le_max_of_le_right one_le_aleph0)

Premises used: Eq.trans_le, le_max_of_le_right, FreeAlgebra.cardinalMk_eq_one, Cardinal.one_le_aleph0
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
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)) ℵ₀
inr₁ : Nonempty 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)) ℵ₀

Tactic:
cases isEmpty_or_nonempty X

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
h : Nontrivial R
h_1 : IsEmpty X
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
(cardinalMk_eq_lift R X).trans_le (le_max_of_le_left <| le_max_left _ _)

Premises used: FreeAlgebra.cardinalMk_eq_lift, Eq.trans_le, le_max_of_le_left, le_max_left
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
h : Nontrivial R
h_1 : IsEmpty X
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
exact (cardinalMk_eq_lift R X).trans_le (le_max_of_le_left <| le_max_left _ _)

Premises used: FreeAlgebra.cardinalMk_eq_lift, Eq.trans_le, le_max_of_le_left, le_max_left
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
h : Nontrivial R
h_1 : Nonempty X
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
(cardinalMk_eq_max_lift R X).le

Premises used: Eq.le, FreeAlgebra.cardinalMk_eq_max_lift
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type v
h : Nontrivial R
h_1 : Nonempty X
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
exact (cardinalMk_eq_max_lift R X).le

Premises used: Eq.le, FreeAlgebra.cardinalMk_eq_max_lift
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type u
inst_1 : Nonempty X
inst_2 : Nontrivial R
⊢ #(FreeAlgebra R X) = max (max #R #X) ℵ₀

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type u
inst_1 : IsEmpty X
⊢ #(FreeAlgebra R X) = #R

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
X : Type u
⊢ #(FreeAlgebra R X) ≤ max (max #R #X) ℵ₀

Tactic:
simpa using cardinalMk_le_max_lift R X

Premises used: FreeAlgebra.cardinalMk_le_max_lift
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ 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))
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
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}
      #(↑(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

Premises used: Cardinal.lift_umax
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
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 })
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))) ℵ₀
⊢ lift.{u, v} #↥(adjoin R s) ≤ max (max (lift.{v, u} #R) (lift.{u, v} #(↑s : Type v))) ℵ₀

Tactic:
rw [Algebra.adjoin_eq_range_freeAlgebra_lift]

Premises used: Algebra.adjoin_eq_range_freeAlgebra_lift
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
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}
      #↥(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:
H.trans (FreeAlgebra.cardinalMk_le_max_lift R s)

Premises used: Set.Mem, setOf, Set.Elem, FreeAlgebra.cardinalMk_le_max_lift, Set.range, LE.le.trans
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
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}
      #↥(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:
exact H.trans (FreeAlgebra.cardinalMk_le_max_lift R s)

Premises used: Set.Elem, FreeAlgebra.cardinalMk_le_max_lift, LE.le.trans
-- Module: Mathlib.Algebra.FreeAlgebra.Cardinality
Goal:
R : Type u
inst : CommSemiring R
A : Type u
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ #↥(adjoin R s) ≤ max (max #R #(↑s : Type u)) ℵ₀

Tactic:
simpa using lift_cardinalMk_adjoin_le R s

Premises used: Algebra.lift_cardinalMk_adjoin_le
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
x y : Pre R X
⊢ Quot.mk (Rel R X) (x * y) = Quot.mk (Rel R X) x * Quot.mk (Rel R X) y

Tactic:
rfl

Premises used: Quot.map₂, Quot.lift₂, rfl
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
c : FreeAlgebra R X
a_3 : Pre R X
⊢ Quot.mk (Rel R X) a_1 * Quot.mk (Rel R X) a_2 * Quot.mk (Rel R X) a_3 =
    Quot.mk (Rel R X) a_1 * (Quot.mk (Rel R X) a_2 * Quot.mk (Rel R X) a_3)

Tactic:
Quot.sound Rel.mul_assoc

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra.Rel.mul_assoc, FreeAlgebra
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
c : FreeAlgebra R X
a_3 : Pre R X
⊢ Quot.mk (Rel R X) a_1 * Quot.mk (Rel R X) a_2 * Quot.mk (Rel R X) a_3 =
    Quot.mk (Rel R X) a_1 * (Quot.mk (Rel R X) a_2 * Quot.mk (Rel R X) a_3)

Tactic:
exact Quot.sound Rel.mul_assoc

Premises used: Quot.sound, FreeAlgebra.Rel.mul_assoc
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
⊢ 1 * Quot.mk (Rel R X) a_1 = Quot.mk (Rel R X) a_1

Tactic:
Quot.sound Rel.one_mul

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra, FreeAlgebra.Rel.one_mul
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
⊢ 1 * Quot.mk (Rel R X) a_1 = Quot.mk (Rel R X) a_1

Tactic:
exact Quot.sound Rel.one_mul

Premises used: Quot.sound, FreeAlgebra.Rel.one_mul
-- Module: Mathlib.Algebra.FreeAlgebra
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 * 1 = Quot.mk (Rel R X) a_1

Tactic:
Quot.sound Rel.mul_one

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra, FreeAlgebra.Rel.mul_one
-- Module: Mathlib.Algebra.FreeAlgebra
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 * 1 = Quot.mk (Rel R X) a_1

Tactic:
exact Quot.sound Rel.mul_one

Premises used: Quot.sound, FreeAlgebra.Rel.mul_one
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
⊢ 0 * Quot.mk (Rel R X) a_1 = 0

Tactic:
Quot.sound Rel.zero_mul

Premises used: FreeAlgebra.Rel.zero_mul, Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
⊢ 0 * Quot.mk (Rel R X) a_1 = 0

Tactic:
exact Quot.sound Rel.zero_mul

Premises used: FreeAlgebra.Rel.zero_mul, Quot.sound
-- Module: Mathlib.Algebra.FreeAlgebra
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 = 0

Tactic:
Quot.sound Rel.mul_zero

Premises used: FreeAlgebra.Rel.mul_zero, Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra
-- Module: Mathlib.Algebra.FreeAlgebra
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 = 0

Tactic:
exact Quot.sound Rel.mul_zero

Premises used: FreeAlgebra.Rel.mul_zero, Quot.sound
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
c : FreeAlgebra R X
a_3 : Pre R X
⊢ Quot.mk (Rel R X) a_1 * (Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_3) =
    Quot.mk (Rel R X) a_1 * Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_1 * Quot.mk (Rel R X) a_3

Tactic:
Quot.sound Rel.left_distrib

Premises used: Quot.sound, FreeAlgebra.Rel.left_distrib, Quot.map₂, Quot.lift₂, FreeAlgebra
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
c : FreeAlgebra R X
a_3 : Pre R X
⊢ Quot.mk (Rel R X) a_1 * (Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_3) =
    Quot.mk (Rel R X) a_1 * Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_1 * Quot.mk (Rel R X) a_3

Tactic:
exact Quot.sound Rel.left_distrib

Premises used: Quot.sound, FreeAlgebra.Rel.left_distrib
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
c : FreeAlgebra R X
a_3 : Pre R X
⊢ (Quot.mk (Rel R X) a_1 + Quot.mk (Rel R X) a_2) * Quot.mk (Rel R X) a_3 =
    Quot.mk (Rel R X) a_1 * Quot.mk (Rel R X) a_3 + Quot.mk (Rel R X) a_2 * Quot.mk (Rel R X) a_3

Tactic:
Quot.sound Rel.right_distrib

Premises used: Quot.sound, Quot.map₂, FreeAlgebra.Rel.right_distrib, Quot.lift₂, FreeAlgebra
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
c : FreeAlgebra R X
a_3 : Pre R X
⊢ (Quot.mk (Rel R X) a_1 + Quot.mk (Rel R X) a_2) * Quot.mk (Rel R X) a_3 =
    Quot.mk (Rel R X) a_1 * Quot.mk (Rel R X) a_3 + Quot.mk (Rel R X) a_2 * Quot.mk (Rel R X) a_3

Tactic:
exact Quot.sound Rel.right_distrib

Premises used: Quot.sound, FreeAlgebra.Rel.right_distrib
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
c : FreeAlgebra R X
a_3 : Pre R X
⊢ Quot.mk (Rel R X) a_1 + Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_3 =
    Quot.mk (Rel R X) a_1 + (Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_3)

Tactic:
Quot.sound Rel.add_assoc

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra.Rel.add_assoc, FreeAlgebra
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
c : FreeAlgebra R X
a_3 : Pre R X
⊢ Quot.mk (Rel R X) a_1 + Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_3 =
    Quot.mk (Rel R X) a_1 + (Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_3)

Tactic:
exact Quot.sound Rel.add_assoc

Premises used: Quot.sound, FreeAlgebra.Rel.add_assoc
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
⊢ 0 + Quot.mk (Rel R X) a_1 = Quot.mk (Rel R X) a_1

Tactic:
Quot.sound Rel.zero_add

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra, FreeAlgebra.Rel.zero_add
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
⊢ 0 + Quot.mk (Rel R X) a_1 = Quot.mk (Rel R X) a_1

Tactic:
exact Quot.sound Rel.zero_add

Premises used: Quot.sound, FreeAlgebra.Rel.zero_add
-- Module: Mathlib.Algebra.FreeAlgebra
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
mk₁ mk₂ : Quot.mk (Rel R X) a_1 = Quot.mk (Rel R X) a_1
⊢ Quot.mk (Rel R X) (a_1 + 0) = Quot.mk (Rel R X) a_1

Tactic:
rw [Quot.sound Rel.add_comm, Quot.sound Rel.zero_add]

Premises used: Quot.sound, FreeAlgebra.Rel.add_comm, FreeAlgebra.Rel.zero_add
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
x : FreeAlgebra R X
a : Pre R X
mk : Quot.mk (Rel R X) (Pre.ofScalar 0 * a) = 0
⊢ Quot.mk (Rel R X) (HMul.hMul (α := Pre R X) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) 0) : Pre R X) a) = 0

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.FreeAlgebra
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) (Pre.ofScalar 0 * a) = 0

Tactic:
Quot.sound Rel.zero_mul

Premises used: FreeAlgebra.Rel.zero_mul, Quot.sound
-- Module: Mathlib.Algebra.FreeAlgebra
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) (Pre.ofScalar 0 * a) = 0

Tactic:
exact Quot.sound Rel.zero_mul

Premises used: FreeAlgebra.Rel.zero_mul, Quot.sound
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
n : ℕ
x : FreeAlgebra R X
a : Pre R X
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
⊢ 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

Tactic:
rw [map_add, map_one, mk_mul, mk_mul, ← add_one_mul (_ : FreeAlgebra R X)]

Premises used: map_add, _private.0.FreeAlgebra.mk_mul, add_one_mul, map_one
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
n : ℕ
x : FreeAlgebra R X
a : Pre R X
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
⊢ 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:
congr 1
-- Module: Mathlib.Algebra.FreeAlgebra
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) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) n)) + 1

Tactic:
Quot.sound Rel.add_scalar

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra.Rel.add_scalar, FreeAlgebra
-- Module: Mathlib.Algebra.FreeAlgebra
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) (Pre.ofScalar ((algebraMap ℕ R : (a : ℕ) → R) n)) + 1

Tactic:
exact Quot.sound Rel.add_scalar

Premises used: Quot.sound, FreeAlgebra.Rel.add_scalar
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
⊢ Quot.mk (Rel R X) a_1 + Quot.mk (Rel R X) a_2 = Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_1

Tactic:
Quot.sound Rel.add_comm

Premises used: Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra, FreeAlgebra.Rel.add_comm
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
a : FreeAlgebra R X
a_1 : Pre R X
b : FreeAlgebra R X
a_2 : Pre R X
⊢ Quot.mk (Rel R X) a_1 + Quot.mk (Rel R X) a_2 = Quot.mk (Rel R X) a_2 + Quot.mk (Rel R X) a_1

Tactic:
exact Quot.sound Rel.add_comm

Premises used: Quot.sound, FreeAlgebra.Rel.add_comm
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
simp : Quot.mk (Rel R X) (Pre.ofScalar 0) = 0
⊢ Quot.mk (Rel R X) (Pre.ofScalar (↑0 : R)) = 0

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
⊢ Quot.mk (Rel R X) (Pre.ofScalar 0) = 0

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
n : ℕ
⊢ Quot.mk (Rel R X) (Pre.ofScalar (↑(n + 1) : R)) = Quot.mk (Rel R X) (Pre.ofScalar (↑n : R)) + 1

Tactic:
simpa using Quot.sound Rel.add_scalar

Premises used: Quot.sound, FreeAlgebra.Rel.add_scalar
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : R
x_1 : FreeAlgebra A X
a : Pre A X
⊢ HMul.hMul (α := FreeAlgebra A X)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              { toFun := fun (r : A) ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ : A →+* FreeAlgebra A X }
              (algebraMap R A) :
            (a : R) → FreeAlgebra A X)
          x :
        FreeAlgebra A X)
      (Quot.mk (Rel A X) a) =
    HMul.hMul (β := FreeAlgebra A X) (Quot.mk (Rel A X) a)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              { toFun := fun (r : A) ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ }
              (algebraMap R A) :
            (a : R) → FreeAlgebra A X)
          x :
        FreeAlgebra A X)

Tactic:
Quot.sound Rel.central_scalar

Premises used: FreeAlgebra.Rel.central_scalar, Quot.sound, Quot.map₂, Quot.lift₂, FreeAlgebra
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : R
x_1 : FreeAlgebra A X
a : Pre A X
⊢ HMul.hMul (α := FreeAlgebra A X)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              { toFun := fun (r : A) ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ : A →+* FreeAlgebra A X }
              (algebraMap R A) :
            (a : R) → FreeAlgebra A X)
          x :
        FreeAlgebra A X)
      (Quot.mk (Rel A X) a) =
    HMul.hMul (β := FreeAlgebra A X) (Quot.mk (Rel A X) a)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              { toFun := fun (r : A) ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ }
              (algebraMap R A) :
            (a : R) → FreeAlgebra A X)
          x :
        FreeAlgebra A X)

Tactic:
exact Quot.sound Rel.central_scalar

Premises used: FreeAlgebra.Rel.central_scalar, Quot.sound
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Type
inst_1 : CommSemiring S
⊢ Eq (α := Algebra ℕ (FreeAlgebra S X)) Semiring.toNatAlgebra (instAlgebra ℕ X)

Tactic:
rfl

Premises used: FreeAlgebra, rfl
-- 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
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)
⊢ (r • s) • x = r • s • x

Tactic:
change algebraMap S A (r • s) • x = algebraMap R A _ • (algebraMap S A _ • x)

Premises used: Algebra.algebraMap, HSMul.hSMul, DFunLike.coe
-- 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
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
⊢ 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:
rw [← smul_assoc]

Premises used: smul_assoc