-- Mathlib/Algebra/Module/LinearMap/End.lean
@[simp]
lemma smulRight_apply_eq_zero_iff {f : M₁ →ₗ[R] S} {x : M} [NoZeroSMulDivisors S M] :
    f.smulRight x = 0 ↔ f = 0 ∨ x = 0

Proof state:
case inr
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
h : f.smulRight x = 0
⊢ f = 0

Tactic:
ext v

Result:
case inr.h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
h : f.smulRight x = 0
v : M₁
⊢ f v = 0 v

Proof state:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
h : f.smulRight x = 0
v : M₁
⊢ f v • x = 0

Tactic:
simpa only [LinearMap.zero_apply] using LinearMap.congr_fun h v

Result:
no goals

Proof state:
case inl
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
inst✝ : NoZeroSMulDivisors S M
⊢ f.smulRight 0 = 0 ↔ f = 0 ∨ 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
h : f = 0 ∨ x = 0
⊢ f.smulRight x = 0

Tactic:
simp [h.resolve_right hx]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
⊢ f.smulRight x = 0 ↔ f = 0 ∨ x = 0

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
inst✝ : NoZeroSMulDivisors S M
⊢ f.smulRight 0 = 0 ↔ f = 0 ∨ 0 = 0

case inr
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
⊢ f.smulRight x = 0 ↔ f = 0 ∨ x = 0

Proof state:
case inr
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
⊢ f.smulRight x = 0 ↔ f = 0 ∨ x = 0

Tactic:
refine ⟨fun h ↦ Or.inl ?_, fun h ↦ by simp [h.resolve_right hx]⟩

Result:
case inr
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
h : f.smulRight x = 0
⊢ f = 0

Proof state:
case inr.h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
v : M₁
h : f v = 0 ∨ x = 0
⊢ f v = 0 v

Tactic:
tauto

Result:
no goals

Proof state:
case inr.h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
v : M₁
h : f v • x = 0
⊢ f v = 0 v

Tactic:
rw [smul_eq_zero] at h

Result:
case inr.h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
v : M₁
h : f v = 0 ∨ x = 0
⊢ f v = 0 v

Proof state:
case inr.h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
h : f.smulRight x = 0
v : M₁
⊢ f v = 0 v

Tactic:
replace h : f v • x = 0 := by simpa only [LinearMap.zero_apply] using LinearMap.congr_fun h v

Result:
case inr.h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : Module R M₁
inst✝⁴ : Semiring S
inst✝³ : Module R S
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
inst✝ : NoZeroSMulDivisors S M
hx : x ≠ 0
v : M₁
h : f v • x = 0
⊢ f v = 0 v