R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
refine' ⟨fun {r m} h => _⟩
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
rw [algebra_compatible_smul A r m] at h
case inl
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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

case inr
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
cases' smul_eq_zero.1 h with H H
case inl
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
case inl
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
have : Function.Injective (algebraMap R A) :=
  NoZeroSMulDivisors.iff_algebraMap_injective.1 inferInstance
case inl.h
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
case inl
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
left
no goals
case inl.h
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
exact (injective_iff_map_eq_zero _).1 this _ H
case inr.h
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
case inr
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
right
no goals
case inr.h
R✝ : Type ?u.984855
inst✝²⁰ : CommSemiring R✝
A✝ : Type ?u.984861
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type ?u.984890
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type ?u.986785
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_1
A : Type u_2
M : Type u_3
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
exact H