[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r₁ r₂ : R
⊢ OneHom.toFun { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) } (r₁ * r₂) =
    OneHom.toFun { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) } r₁ *
      OneHom.toFun { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) } r₂
[PROOFSTEP]
simp only [h₁, mul_smul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r : R
x : (fun x => A) r
⊢ ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) },
                map_mul' := (_ : ∀ (r₁ r₂ : R), (r₁ * r₂) • 1 = r₁ • 1 * r₂ • 1) },
            map_zero' := (_ : 0 • 1 = 0), map_add' := (_ : ∀ (r₁ r₂ : R), (r₁ + r₂) • 1 = r₁ • 1 + r₂ • 1) }
        r *
      x =
    x *
      ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) },
                map_mul' := (_ : ∀ (r₁ r₂ : R), (r₁ * r₂) • 1 = r₁ • 1 * r₂ • 1) },
            map_zero' := (_ : 0 • 1 = 0), map_add' := (_ : ∀ (r₁ r₂ : R), (r₁ + r₂) • 1 = r₁ • 1 + r₂ • 1) }
        r
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r : R
x : (fun x => A) r
⊢ r • x =
    ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) },
                map_mul' := (_ : ∀ (r₁ r₂ : R), (r₁ * r₂) • 1 = r₁ • 1 * r₂ • 1) },
            map_zero' := (_ : 0 • 1 = 0), map_add' := (_ : ∀ (r₁ r₂ : R), (r₁ + r₂) • 1 = r₁ • 1 + r₂ • 1) }
        r *
      x
[PROOFSTEP]
simp [h₁]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : 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
⊢ r • 1 * x = r • x
[PROOFSTEP]
rw [h₁, one_mul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : 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
⊢ x * r • 1 = r • x
[PROOFSTEP]
rw [h₂, mul_one]
[GOAL]
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : ∀ (r : R), ↑(algebraMap R A) r = ↑(algebraMap R A) r
⊢ P = Q
[PROOFSTEP]
replace h : P.toRingHom = Q.toRingHom := FunLike.ext _ _ h
[GOAL]
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
⊢ P = Q
[PROOFSTEP]
have h' :
  (haveI := P;
      (· • ·) :
      R → A → A) =
    (haveI := Q;
      (· • ·) :
      R → A → A) :=
  by
  funext r a
  rw [P.smul_def', Q.smul_def', h]
[GOAL]
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
⊢ (fun x x_1 => x • x_1) = fun x x_1 => x • x_1
[PROOFSTEP]
funext r a
[GOAL]
case h.h
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
r : R
a : A
⊢ r • a = r • a
[PROOFSTEP]
rw [P.smul_def', Q.smul_def', h]
[GOAL]
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
h' : (fun x x_1 => x • x_1) = fun x x_1 => x • x_1
⊢ P = Q
[PROOFSTEP]
rcases P with @⟨⟨P⟩⟩
[GOAL]
case mk.mk
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
Q : Algebra R A
toRingHom✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : (fun x => A) r), ↑toRingHom✝ r * x = x * ↑toRingHom✝ r
P : R → A → A
smul_def'✝ : ∀ (r : R) (x : (fun x => A) r), r • x = ↑toRingHom✝ r * x
h : toRingHom = toRingHom
h' : (fun x x_1 => x • x_1) = fun x x_1 => x • x_1
⊢ mk toRingHom✝ commutes'✝ smul_def'✝ = Q
[PROOFSTEP]
rcases Q with @⟨⟨Q⟩⟩
[GOAL]
case mk.mk.mk.mk
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
toRingHom✝¹ : R →+* A
commutes'✝¹ : ∀ (r : R) (x : (fun x => A) r), ↑toRingHom✝¹ r * x = x * ↑toRingHom✝¹ r
P : R → A → A
smul_def'✝¹ : ∀ (r : R) (x : (fun x => A) r), r • x = ↑toRingHom✝¹ r * x
toRingHom✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : (fun x => A) r), ↑toRingHom✝ r * x = x * ↑toRingHom✝ r
Q : R → A → A
smul_def'✝ : ∀ (r : R) (x : (fun x => A) r), r • x = ↑toRingHom✝ r * x
h : toRingHom = toRingHom
h' : (fun x x_1 => x • x_1) = fun x x_1 => x • x_1
⊢ mk toRingHom✝¹ commutes'✝¹ smul_def'✝¹ = mk toRingHom✝ commutes'✝ smul_def'✝
[PROOFSTEP]
congr
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A
⊢ 1 • x✝ = x✝
[PROOFSTEP]
simp [smul_def']
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (x y : R) (b : A), (x * y) • b = x • y • b
[PROOFSTEP]
simp [smul_def', mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
simp [smul_def']
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (a : R) (x y : A), a • (x + y) = a • x + a • y
[PROOFSTEP]
simp [smul_def', mul_add]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (r s : R) (x : A), (r + s) • x = r • x + s • x
[PROOFSTEP]
simp [smul_def', add_mul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (x : A), 0 • x = 0
[PROOFSTEP]
simp [smul_def']
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
r : R
y : A
⊢ x * (↑(algebraMap R A) r * y) = ↑(algebraMap R A) r * (x * y)
[PROOFSTEP]
rw [← mul_assoc, ← commutes, mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
r : R
y : A
⊢ x * ↑(algebraMap R A) r * y = x * y * ↑(algebraMap R A) r
[PROOFSTEP]
rw [mul_assoc, commutes, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : R
y z : A
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
s : R
x y : A
⊢ x * s • y = s • (x * y)
[PROOFSTEP]
rw [smul_def, smul_def, left_comm]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ a • ↑(algebraMap R A) r = ↑(algebraMap R A) r
[PROOFSTEP]
rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
src✝ : R →+* A := algebraMap R A
x y : R
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
      (x • y) =
    ↑(RingHom.id R) x •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        y
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - ↑(algebraMap R A) r) = (x - ↑(algebraMap R A) r) * x
[PROOFSTEP]
rw [mul_sub, ← commutes, sub_mul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
⊢ x * (x - ↑(algebraMap R A) r) ^ n = (x - ↑(algebraMap R A) r) ^ n * x
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - ↑(algebraMap R A) r) ^ Nat.zero = (x - ↑(algebraMap R A) r) ^ Nat.zero * x
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - ↑(algebraMap R A) r) ^ n = (x - ↑(algebraMap R A) r) ^ n * x
⊢ x * (x - ↑(algebraMap R A) r) ^ Nat.succ n = (x - ↑(algebraMap R A) r) ^ Nat.succ n * x
[PROOFSTEP]
rw [pow_succ, ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝¹ : AddCommGroup A := Module.addCommMonoidToAddCommGroup R
src✝ : Semiring A := inferInstance
z : ℕ
⊢ IntCast.intCast ↑z = ↑z
[PROOFSTEP]
simp only [Int.cast_ofNat, map_natCast]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝¹ : AddCommGroup A := Module.addCommMonoidToAddCommGroup R
src✝ : Semiring A := inferInstance
z : ℕ
⊢ IntCast.intCast (Int.negSucc z) = -↑(z + 1)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h)⁻¹ (x • m') = m'
[PROOFSTEP]
apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) (↑↑(IsUnit.unit h)⁻¹ (x • m')) = ↑↑(IsUnit.unit h) m'
[PROOFSTEP]
erw [End_isUnit_apply_inv_apply_of_isUnit]
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ x • m' = ↑↑(IsUnit.unit h) m'
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ m' = ↑↑(IsUnit.unit h)⁻¹ (x • m')
[PROOFSTEP]
apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) m' = ↑↑(IsUnit.unit h) (↑↑(IsUnit.unit h)⁻¹ (x • m'))
[PROOFSTEP]
erw [End_isUnit_apply_inv_apply_of_isUnit]
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) m' = x • m'
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ ↑f (↑(algebraMap R A) r * a) = ↑(algebraMap R B) r * ↑f a
[PROOFSTEP]
rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ ↑f (a * ↑(algebraMap R A) r) = ↑f a * ↑(algebraMap R B) r
[PROOFSTEP]
rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]
[GOAL]
R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
⊢ P = Q
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
r✝ : ℕ
⊢ ↑(algebraMap ℕ R) r✝ = ↑(algebraMap ℕ R) r✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Nontrivial A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ Function.Injective ↑(algebraMap R A)
[PROOFSTEP]
have := @smul_left_injective R A CommRing.toRing Ring.toAddCommGroup Algebra.toModule ‹_› 1 one_ne_zero
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Nontrivial A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
this : Function.Injective fun c => c • 1
⊢ Function.Injective ↑(algebraMap R A)
[PROOFSTEP]
simpa only [algebraMap_eq_smul_one'] using this
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module A N
inst✝¹ : Module R N
inst✝ : IsScalarTower R A N
r : R
m : M
⊢ r • m = ↑(algebraMap R A) r • m
[PROOFSTEP]
rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]
[GOAL]
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
⊢ NoZeroSMulDivisors R M
[PROOFSTEP]
refine' ⟨fun {r m} h => _⟩
[GOAL]
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : r • m = 0
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
rw [algebra_compatible_smul A r m] at h 
[GOAL]
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
cases' smul_eq_zero.1 h with H H
[GOAL]
case inl
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : ↑(algebraMap R A) r = 0
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
have : Function.Injective (algebraMap R A) := NoZeroSMulDivisors.iff_algebraMap_injective.1 inferInstance
[GOAL]
case inl
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : ↑(algebraMap R A) r = 0
this : Function.Injective ↑(algebraMap R A)
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
left
[GOAL]
case inl.h
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : ↑(algebraMap R A) r = 0
this : Function.Injective ↑(algebraMap R A)
⊢ r = 0
[PROOFSTEP]
exact (injective_iff_map_eq_zero _).1 this _ H
[GOAL]
case inr
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : m = 0
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
right
[GOAL]
case inr.h
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : m = 0
⊢ m = 0
[PROOFSTEP]
exact H
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module A N
inst✝¹ : Module R N
inst✝ : IsScalarTower R A N
r : R
a : A
m : M
⊢ r • a • m = a • r • m
[PROOFSTEP]
rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ← algebra_compatible_smul]
