Theorem: MvPolynomial.vars_X_subset (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
⊢ (X n).vars ⊆ {n}
Tactic:
intro u
State after:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
⊢ u ∈ (X n).vars → u ∈ {n}

State before:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
⊢ u ∈ (X n).vars → u ∈ {n}
Tactic:
rw [X, mem_vars, mem_singleton]
State after:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
⊢ (∃ d ∈ ((monomial (Finsupp.single n 1)) 1).support, u ∈ d.support) → u = n

State before:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
⊢ (∃ d ∈ ((monomial (Finsupp.single n 1)) 1).support, u ∈ d.support) → u = n
Tactic:
rintro ⟨c, hc, hc'⟩
State after:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : c ∈ ((monomial (Finsupp.single n 1)) 1).support
hc' : u ∈ c.support
⊢ u = n

State before:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : c ∈ ((monomial (Finsupp.single n 1)) 1).support
hc' : u ∈ c.support
⊢ u = n
Tactic:
by_contra h'
State after:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : c ∈ ((monomial (Finsupp.single n 1)) 1).support
hc' : u ∈ c.support
h' : ¬u = n
⊢ False

State before:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : c ∈ ((monomial (Finsupp.single n 1)) 1).support
hc' : u ∈ c.support
h' : ¬u = n
⊢ False
Tactic:
rw [mem_support_iff, coeff_monomial, ne_eq] at hc
State after:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
⊢ False

State before:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
⊢ False
Tactic:
by_cases h : Finsupp.single n 1 = c
State after:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ False

case neg
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : ¬Finsupp.single n 1 = c
⊢ False

State before:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ False
Tactic:
rw [← h, Finsupp.mem_support_iff, ne_eq, Finsupp.single_apply] at hc'
State after:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : ¬(if n = u then 1 else 0) = 0
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ False

State before:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : ¬(if n = u then 1 else 0) = 0
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ False
Tactic:
apply hc'
State after:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : ¬(if n = u then 1 else 0) = 0
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ (if n = u then 1 else 0) = 0

State before:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : ¬(if n = u then 1 else 0) = 0
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ (if n = u then 1 else 0) = 0
Tactic:
rw [if_neg (Ne.symm h')]
State after:
no goals

State before:
case neg
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : ¬Finsupp.single n 1 = c
⊢ False
Tactic:
apply hc
State after:
case neg
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : ¬Finsupp.single n 1 = c
⊢ (if Finsupp.single n 1 = c then 1 else 0) = 0

State before:
case neg
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : ¬Finsupp.single n 1 = c
⊢ (if Finsupp.single n 1 = c then 1 else 0) = 0
Tactic:
rw [if_neg h]
State after:
no goals