case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ Finset.card (support f) ≤ 1 → ∃ n a, f = ↑(monomial n) a

case mpr
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ (∃ n a, f = ↑(monomial n) a) → Finset.card (support f) ≤ 1
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ Finset.card (support f) ≤ 1 ↔ ∃ n a, f = ↑(monomial n) a
constructor
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
H : Finset.card (support f) ≤ 1
⊢ ∃ n a, f = ↑(monomial n) a
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ Finset.card (support f) ≤ 1 → ∃ n a, f = ↑(monomial n) a
intro H
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
H : ∃ x, support f ⊆ {x}
⊢ ∃ n a, f = ↑(monomial n) a
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
H : Finset.card (support f) ≤ 1
⊢ ∃ n a, f = ↑(monomial n) a
rw [Finset.card_le_one_iff_subset_singleton] at H
case mp.intro
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
⊢ ∃ n a, f = ↑(monomial n) a
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
H : ∃ x, support f ⊆ {x}
⊢ ∃ n a, f = ↑(monomial n) a
rcases H with ⟨n, hn⟩
case mp.intro
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
⊢ f = ↑(monomial n) (coeff f n)
case mp.intro
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
⊢ ∃ n a, f = ↑(monomial n) a
refine' ⟨n, f.coeff n, _⟩
case mp.intro.a
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
case mp.intro
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
⊢ f = ↑(monomial n) (coeff f n)
ext i
case pos
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : i = n
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i

case neg
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
case mp.intro.a
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
by_cases hi : i = n
no goals
case pos
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : i = n
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
simp [hi, coeff_monomial]
case neg
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
this : coeff f i = 0
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
case neg
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
have : f.coeff i = 0 := by
  rw [← not_mem_support_iff]
  exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
no goals
case neg
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
this : coeff f i = 0
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
simp [this, Ne.symm hi, coeff_monomial]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ ¬i ∈ support f
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ coeff f i = 0
rw [← not_mem_support_iff]
no goals
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ ¬i ∈ support f
exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
case mpr.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ Finset.card (support (↑(monomial n) a)) ≤ 1
case mpr
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ (∃ n a, f = ↑(monomial n) a) → Finset.card (support f) ≤ 1
rintro ⟨n, a, rfl⟩
case mpr.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ Finset.card (support (↑(monomial n) a)) ≤ Finset.card {n}
case mpr.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ Finset.card (support (↑(monomial n) a)) ≤ 1
rw [← Finset.card_singleton n]
case mpr.intro.intro.a
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ support (↑(monomial n) a) ⊆ {n}
case mpr.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ Finset.card (support (↑(monomial n) a)) ≤ Finset.card {n}
apply Finset.card_le_of_subset
no goals
case mpr.intro.intro.a
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ support (↑(monomial n) a) ⊆ {n}
exact support_monomial' _ _