awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
N : Type u_4
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : M →ₗ[R] N
r : S
x : M
obtain :
  ∀ (r : R),
    f.toFun (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x) =
      HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) r : S) : S) (f.toFun x)
⊢ f.toFun (r • x) = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) (f.toFun x)

Tactic:
obtain ⟨r, rfl⟩ := h r

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
N : Type u_4
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : M →ₗ[R] N
x : M
r : R
⊢ f.toFun (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) r : S) : S) (f.toFun x)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
N : Type u_4
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : M ≃ₗ[R] N
r : S
x : M
obtain :
  ∀ (r : R),
    (↑f : M →ₗ[R] N).toFun (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x) =
      HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) r : S) : S)
        ((↑f : M →ₗ[R] N).toFun x)
⊢ (↑f : M →ₗ[R] N).toFun (r • x) = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) ((↑f : M →ₗ[R] N).toFun x)

Tactic:
obtain ⟨r, rfl⟩ := h r

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
N : Type u_4
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : M ≃ₗ[R] N
x : M
r : R
⊢ (↑f : M →ₗ[R] N).toFun (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) x) =
    HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) r : S) : S)
      ((↑f : M →ₗ[R] N).toFun x)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_2
N : Type u_3
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
l : M →ₗ[R] N
x : M
⊢ Eq.{u_3 + 1} (α := N) ((extendScalarsOfSurjective h l : (a : M) → N) x : N) ((l : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_2
N : Type u_3
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : M ≃ₗ[R] N
x : M
⊢ Eq.{u_3 + 1} (α := N) ((extendScalarsOfSurjective h f : (a : M) → N) x : N) ((f : (a : M) → N) x : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
S : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_2
N : Type u_3
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module S M
inst_7 : IsScalarTower R S M
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
h : Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
f : M ≃ₗ[R] N
⊢ Eq (α := N ≃ₗ[S] M) (symm (extendScalarsOfSurjective h f)) (extendScalarsOfSurjective h f.symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.extendScalarsOfSurjective, rfl
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_3
s : Finset ι
a : ι → R
⊢ Eq.{u_2 + 1} (α := A) (↑(∏ i ∈ s, a i) : A) (∏ i ∈ s, (↑(a i) : A))

Tactic:
map_prod (algebraMap R A) a s

Premises used: Algebra.algebraMap, map_prod
-- Module: Mathlib.Algebra.Algebra.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_3
s : Finset ι
a : ι → R
⊢ Eq.{u_2 + 1} (α := A) (↑(∑ i ∈ s, a i) : A) (∑ i ∈ s, (↑(a i) : A))

Tactic:
map_sum (algebraMap R A) a s

Premises used: Algebra.algebraMap, map_sum
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Subsingleton R
⊢ Subsingleton A

Tactic:
(algebraMap R A).codomain_trivial

Premises used: Algebra.algebraMap, RingHom.codomain_trivial
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_2 + 1} (α := A) (↑0 : A) 0

Tactic:
map_zero (algebraMap R A)

Premises used: Algebra.algebraMap, map_zero
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq.{u_2 + 1} (α := A) (↑1 : A) 1

Tactic:
map_one (algebraMap R A)

Premises used: Algebra.algebraMap, map_one
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : ℕ
⊢ Eq.{u_2 + 1} (α := A) (↑(↑a : R) : A) (↑a : A)

Tactic:
map_natCast (algebraMap R A) a

Premises used: Algebra.algebraMap, map_natCast
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a b : R
⊢ (↑(a + b) : A) = HAdd.hAdd (α := A) (↑a : A) (↑b : A)

Tactic:
map_add (algebraMap R A) a b

Premises used: Algebra.algebraMap, map_add
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a b : R
⊢ (↑(a * b) : A) = HMul.hMul (α := A) (↑a : A) (↑b : A)

Tactic:
map_mul (algebraMap R A) a b

Premises used: Algebra.algebraMap, map_mul
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : R
n : ℕ
⊢ (↑(a ^ n) : A) = HPow.hPow (α := A) (↑a : A) n

Tactic:
map_pow (algebraMap R A) _ _

Premises used: Algebra.algebraMap, map_pow
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : R
⊢ Eq.{u_2 + 1} (α := A) (↑(-x) : A) (-(↑x : A))

Tactic:
map_neg (algebraMap R A) x

Premises used: Algebra.algebraMap, map_neg
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
a b : R
⊢ (↑(a - b) : A) = HSub.hSub (α := A) (↑a : A) (↑b : A)

Tactic:
map_sub (algebraMap R A) a b

Premises used: map_sub, Algebra.algebraMap
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
i : R →+* S
h : ∀ (c : R) (x : S), HMul.hMul (α := S) ((i : (a : R) → S) c : S) x = HMul.hMul (β := S) x ((i : (a : R) → S) c : S)
r : R
s : S
⊢ let x := i.toAlgebra' h;
  r • s = HMul.hMul (α := S) ((i : (a : R) → S) r : S) s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
i : R →+* S
h : ∀ (c : R) (x : S), HMul.hMul (α := S) ((i : (a : R) → S) c : S) x = HMul.hMul (β := S) x ((i : (a : R) → S) c : S)
⊢ algebraMap R S = i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
i : R →+* S
r : R
s : S
⊢ let x := i.toAlgebra;
  r • s = HMul.hMul (α := S) ((i : (a : R) → S) r : S) s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
i : R →+* S
⊢ algebraMap R S = i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x : A), HSMul.hSMul (β := A) r 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * HSMul.hSMul (β := A) r 1 = r • x
r₁ r₂ : R
⊢ HSMul.hSMul (β := A) (r₁ * r₂) 1 = HSMul.hSMul (β := A) r₁ 1 * HSMul.hSMul (β := A) r₂ 1

Tactic:
simp only [h₁, mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x : A), HSMul.hSMul (β := A) r 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * HSMul.hSMul (β := A) r 1 = r • x
r : R
x : A
⊢ HMul.hMul (α := A)
      ((({ toFun := fun (r : R) ↦ HSMul.hSMul (β := A) r 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ } :
              R →+* A) :
            (a : R) → A)
          r :
        A)
      x =
    HMul.hMul (β := A) x
      ((({ toFun := fun (r : R) ↦ HSMul.hSMul (β := A) r 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ } :
              R →+* A) :
            (a : R) → A)
          r :
        A)

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x : A), HSMul.hSMul (β := A) r 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * HSMul.hSMul (β := A) r 1 = r • x
r : R
x : A
⊢ r • x =
    HMul.hMul (α := A)
      ((({ toFun := fun (r : R) ↦ HSMul.hSMul (β := A) r 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ } :
              R →+* A) :
            (a : R) → A)
          r :
        A)
      x

Tactic:
simp [h₁]
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
rw : r • (1 * x) = r • x
rw₁ rw₂ : r • x = r • x
⊢ HSMul.hSMul (β := A) r 1 * x = r • x

Tactic:
rw [h₁, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
rw : r • (x * 1) = r • x
rw₁ rw₂ : r • x = r • x
⊢ x * HSMul.hSMul (β := A) r 1 = r • x

Tactic:
rw [h₂, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : ∀ (r : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) r : A)
⊢ Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)

Tactic:
replace h : P.algebraMap = Q.algebraMap := DFunLike.ext _ _ h
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
h₁ : ∀ (r : R) (a : A), r • a = r • a
⊢ Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2

Tactic:
funext r a
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
r : R
a : A
h₁ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a = r • a
h₂ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a
h₃ h₄ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a
⊢ r • a = r • a

Tactic:
rw [P.smul_def', Q.smul_def', h]

Premises used: Algebra.smul_def'
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
⊢ Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2

Tactic:
have h' : (haveI := P; (· • ·) : R → A → A) = (haveI := Q; (· • ·) : R → A → A) := by
    funext r a
    rw [P.smul_def', Q.smul_def', h]
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
P Q : Algebra R A
h : Eq (α := R →+* A) (algebraMap R A) (algebraMap R A)
h' : Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2
rcases :
  ∀ (algebraMap : R →+* A)
    (commutes' :
      ∀ (r : R) (x : A),
        HMul.hMul (α := A) ((algebraMap : (a : R) → A) r : A) x =
          HMul.hMul (β := A) x ((algebraMap : (a : R) → A) r : A))
    (P : R → A → A) (smul_def' : ∀ (r : R) (x : A), r • x = HMul.hMul (α := A) ((algebraMap : (a : R) → A) r : A) x)
    (h : Eq (α := R →+* A) (Algebra.algebraMap R A) (Algebra.algebraMap R A))
    (h' : Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2),
    { smul := P, algebraMap := algebraMap, commutes' := commutes', smul_def' := smul_def' : Algebra R A } = Q
⊢ P = Q

Tactic:
rcases P with @⟨⟨P⟩⟩
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
Q : Algebra R A
algebraMap : R →+* A
commutes' :
  ∀ (r : R) (x : A),
    HMul.hMul (α := A) ((algebraMap : (a : R) → A) r : A) x = HMul.hMul (β := A) x ((algebraMap : (a : R) → A) r : A)
P : R → A → A
smul_def' : ∀ (r : R) (x : A), r • x = HMul.hMul (α := A) ((algebraMap : (a : R) → A) r : A) x
h : Eq (α := R →+* A) (Algebra.algebraMap R A) (Algebra.algebraMap R A)
h' : Eq (α := R → A → A) (fun (x1 : R) (x2 : A) ↦ x1 • x2) fun (x1 : R) (x2 : A) ↦ x1 • x2
⊢ { smul := P, algebraMap := algebraMap, commutes' := commutes', smul_def' := smul_def' : Algebra R A } = Q

Tactic:
congr
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ RingHom.toAlgebra (algebraMap R S) = inst_2

Tactic:
algebra_ext _ _ fun _ ↦ rfl

Premises used: Algebra.algebra_ext, rfl
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R_1 : Type u
S : Type v
A_1 : Type w
B : Type u_1
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : Semiring A_1
inst_3 : Algebra R_1 A_1
inst_4 : Semiring B
inst_5 : Algebra R_1 B
R : Type u_2
A : Type u_3
x : CommSemiring R
x_1 : Semiring A
inst_6 : Algebra R A
⊢ ∀ (x_2 y : R) (b : A), (x_2 * y) • b = x_2 • y • b

Tactic:
simp [smul_def', mul_assoc]

Premises used: mul_assoc, Algebra.smul_def'
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R_1 : Type u
S : Type v
A_1 : Type w
B : Type u_1
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : Semiring A_1
inst_3 : Algebra R_1 A_1
inst_4 : Semiring B
inst_5 : Algebra R_1 B
R : Type u_2
A : Type u_3
x : CommSemiring R
x_1 : Semiring A
inst_6 : Algebra R A
x_2 : A
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) 1 x_2 = x_2

Tactic:
simp [smul_def']

Premises used: Algebra.smul_def'
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R_1 : Type u
S : Type v
A_1 : Type w
B : Type u_1
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : Semiring A_1
inst_3 : Algebra R_1 A_1
inst_4 : Semiring B
inst_5 : Algebra R_1 B
R : Type u_2
A : Type u_3
x : CommSemiring R
x_1 : Semiring A
inst_6 : Algebra R A
⊢ ∀ (a : R), HSMul.hSMul (β := A) a 0 = 0

Tactic:
simp [smul_def']

Premises used: Algebra.smul_def'
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R_1 : Type u
S : Type v
A_1 : Type w
B : Type u_1
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : Semiring A_1
inst_3 : Algebra R_1 A_1
inst_4 : Semiring B
inst_5 : Algebra R_1 B
R : Type u_2
A : Type u_3
x : CommSemiring R
x_1 : Semiring A
inst_6 : Algebra R A
⊢ ∀ (a : R) (x_2 y : A), a • (x_2 + y) = a • x_2 + a • y

Tactic:
simp [smul_def', mul_add]

Premises used: Algebra.smul_def', mul_add
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R_1 : Type u
S : Type v
A_1 : Type w
B : Type u_1
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : Semiring A_1
inst_3 : Algebra R_1 A_1
inst_4 : Semiring B
inst_5 : Algebra R_1 B
R : Type u_2
A : Type u_3
x : CommSemiring R
x_1 : Semiring A
inst_6 : Algebra R A
⊢ ∀ (r s : R) (x_2 : A), (r + s) • x_2 = r • x_2 + s • x_2

Tactic:
simp [smul_def', add_mul]

Premises used: add_mul, Algebra.smul_def'
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R_1 : Type u
S : Type v
A_1 : Type w
B : Type u_1
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : Semiring A_1
inst_3 : Algebra R_1 A_1
inst_4 : Semiring B
inst_5 : Algebra R_1 B
R : Type u_2
A : Type u_3
x : CommSemiring R
x_1 : Semiring A
inst_6 : Algebra R A
⊢ ∀ (x_2 : A), HSMul.hSMul.{u_2, u_3, u_3} (α := R) 0 x_2 = 0

Tactic:
simp [smul_def']

Premises used: Algebra.smul_def'
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
x : A
⊢ r • x = HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x

Tactic:
Algebra.smul_def' r x

Premises used: Algebra.smul_def'
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ (algebraMap R A : (a : R) → A) r = HSMul.hSMul (β := A) r 1

Tactic:
calc
    algebraMap R A r = algebraMap R A r * 1 := (mul_one _).symm
    _ = r • (1 : A) := (Algebra.smul_def r 1).symm

Premises used: Trans.trans, Algebra.smul_def, mul_one, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := (a : R) → A) (⇑(algebraMap R A) : (a : R) → A) fun (r : R) ↦ HSMul.hSMul (β := A) r 1

Tactic:
funext algebraMap_eq_smul_one

Premises used: Algebra.algebraMap_eq_smul_one, funext
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
x : A
⊢ HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x =
    HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A)

Tactic:
Algebra.commutes' r x

Premises used: Algebra.commutes'
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
x : A
⊢ Commute ((algebraMap R A : (a : R) → A) r) x

Tactic:
Algebra.commutes r x

Premises used: SemiconjBy, Commute, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
x : A
⊢ Commute x ((algebraMap R A : (a : R) → A) r)

Tactic:
(Algebra.commutes r x).symm

Premises used: SemiconjBy, Commute, Eq.symm, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
y : A
rw :
  HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) * y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
rw₁ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x * y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
rw₂ rw₃ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)
⊢ x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) (x * y)

Tactic:
rw [← mul_assoc, ← commutes, mul_assoc]

Premises used: mul_assoc, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
y : A
rw :
  x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) y =
    HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)
rw₁ :
  x * HMul.hMul (β := A) y ((algebraMap R A : (a : R) → A) r : A) =
    HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)
rw₂ rw₃ :
  HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A) =
    HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)
⊢ HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) * y =
    HMul.hMul (β := A) (x * y) ((algebraMap R A : (a : R) → A) r : A)

Tactic:
rw [mul_assoc, commutes, ← mul_assoc]

Premises used: mul_assoc, Algebra.commutes
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : Algebra R B
x : R
y z : A
rw : x • y * z = x • y • z
rw₁ : x • y * z = x • (y * z)
rw₂ : HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) y * z = x • (y * z)
rw₃ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) y * z =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) (y * z)
rw₄ rw₅ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) (y * z) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) x : A) (y * z)
⊢ (x • y) • z = x • y • z

Tactic:
rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]

Premises used: mul_assoc, Algebra.smul_def, smul_eq_mul
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := R →+* A) RingHom.smulOneHom (algebraMap R A)

Tactic:
RingHom.ext fun r => (algebraMap_eq_smul_one r).symm

Premises used: Algebra.algebraMap_eq_smul_one, RingHom.ext, Eq.symm
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : R
x y : A
rw : x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) y = s • (x * y)
rw₁ :
  x * HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) y =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) (x * y)
rw₂ rw₃ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) (x * y) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) s : A) (x * y)
⊢ x * s • y = s • (x * y)

Tactic:
rw [smul_def, smul_def, left_comm]

Premises used: Algebra.left_comm, Algebra.smul_def
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
x y : A
⊢ r • x * y = r • (x * y)

Tactic:
smul_mul_assoc r x y

Premises used: smul_mul_assoc
-- Module: Mathlib.Algebra.Algebra.Defs
Goal:
R : Type u
A : Type w
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
α : Type u_2
inst_3 : Monoid α
inst_4 : MulDistribMulAction α A
inst_5 : SMulCommClass α R A
a : α
r : R
rw : a • HSMul.hSMul (β := A) r 1 = HSMul.hSMul (β := A) r 1
rw₁ : r • HSMul.hSMul (β := A) a 1 = HSMul.hSMul (β := A) r 1
rw₂ rw₃ : HSMul.hSMul (β := A) r 1 = HSMul.hSMul (β := A) r 1
⊢ HSMul.hSMul (β := A) a ((algebraMap R A : (a : R) → A) r : A) = (algebraMap R A : (a : R) → A) r

Tactic:
rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, MulDistribMulAction.smul_one, SMulCommClass.smul_comm, OfNat.ofNat