Theorem: ContinuousLinearMap.smulRight_ne_zero (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
⊢ c.smulRight f ≠ 0
Tactic:
rcases ContinuousLinearMap.exists_ne_zero c0 with ⟨x,cx⟩
State after:
case intro
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
x : A
cx : c x ≠ 0
⊢ c.smulRight f ≠ 0

State before:
case intro
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
x : A
cx : c x ≠ 0
⊢ c.smulRight f ≠ 0
Tactic:
simp only [Ne, ContinuousLinearMap.ext_iff, not_forall, ContinuousLinearMap.zero_apply,
  ContinuousLinearMap.smulRight_apply, smul_eq_zero, not_or]
State after:
case intro
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
x : A
cx : c x ≠ 0
⊢ ∃ x, ¬c x = 0 ∧ ¬f = 0

State before:
case intro
n : ℕ
𝕜 : Type
inst✝¹¹ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝¹⁰ : Semiring R✝
R A B : Type
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace A
inst✝⁷ : AddCommMonoid A
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace B
inst✝³ : AddCommMonoid B
inst✝² : Module R B
inst✝¹ : ContinuousSMul R B
inst✝ : NoZeroSMulDivisors R B
c : A →L[R] R
f : B
c0 : c ≠ 0
f0 : f ≠ 0
x : A
cx : c x ≠ 0
⊢ ∃ x, ¬c x = 0 ∧ ¬f = 0
Tactic:
use x
State after:
no goals