Theorem: MvPolynomial.nonTorsionWeight_of_nonZero (DividedPowers/ForMathlib/WeightedHomogeneous.lean)

State before:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
⊢ NonTorsionWeight w
Tactic:
intro n x
State after:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
⊢ n • w x = 0 → n = 0

State before:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
⊢ n • w x = 0 → n = 0
Tactic:
rw [smul_eq_zero]
State after:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
⊢ n = 0 ∨ w x = 0 → n = 0

State before:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
⊢ n = 0 ∨ w x = 0 → n = 0
Tactic:
intro hnx
State after:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hnx : n = 0 ∨ w x = 0
⊢ n = 0

State before:
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hnx : n = 0 ∨ w x = 0
⊢ n = 0
Tactic:
cases' hnx with hn hx
State after:
case inl
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hn : n = 0
⊢ n = 0

case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ n = 0

State before:
case inl
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hn : n = 0
⊢ n = 0

case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ n = 0
Tactic:
exact hn
State after:
case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ n = 0

State before:
case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ n = 0
Tactic:
exfalso
State after:
case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ False

State before:
case inr
R : Type ?u.38955
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_2
inst✝¹ : CanonicallyOrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
n : ℕ
x : σ
hx : w x = 0
⊢ False
Tactic:
exact hw x hx
State after:
no goals