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

State before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R✝ A✝ B E : Type
inst✝⁵ : Semiring R✝
R A : Type
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Nontrivial A
⊢ 1 ≠ 0
Tactic:
simp only [Ne, ContinuousLinearMap.ext_iff, not_forall, ContinuousLinearMap.zero_apply,
  ContinuousLinearMap.one_apply]
State after:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R✝ A✝ B E : Type
inst✝⁵ : Semiring R✝
R A : Type
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Nontrivial A
⊢ ∃ x, ¬x = 0

State before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R✝ A✝ B E : Type
inst✝⁵ : Semiring R✝
R A : Type
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Nontrivial A
⊢ ∃ x, ¬x = 0
Tactic:
apply exists_ne
State after:
no goals