-- Mathlib/Algebra/Polynomial/Monomial.lean
theorem card_support_le_one_iff_monomial {f : R[X]} :
    Finset.card f.support ≤ 1 ↔ ∃ n a, f = monomial n a

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = 0

Tactic:
rw [← not_mem_support_iff]

Result:
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ i ∉ f.support

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ i ∉ f.support

Tactic:
exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))

Result:
no goals

Proof state:
case mpr.intro.intro.a
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support ⊆ {n}

Tactic:
exact support_monomial' _ _

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f.support.card ≤ 1 → ∃ n a, f = (monomial n) a

Tactic:
intro H

Result:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : f.support.card ≤ 1
⊢ ∃ n a, f = (monomial n) a

Proof state:
case mp.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ f = (monomial n) (f.coeff n)

Tactic:
ext i

Result:
case mp.intro.a
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Proof state:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : ∃ x, f.support ⊆ {x}
⊢ ∃ n a, f = (monomial n) a

Tactic:
rcases H with ⟨n, hn⟩

Result:
case mp.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ ∃ n a, f = (monomial n) a

Proof state:
case mpr.intro.intro
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support.card ≤ 1

Tactic:
rw [← Finset.card_singleton n]

Result:
case mpr.intro.intro
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support.card ≤ {n}.card

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f.support.card ≤ 1 ↔ ∃ n a, f = (monomial n) a

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f.support.card ≤ 1 → ∃ n a, f = (monomial n) a

case mpr
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ (∃ n a, f = (monomial n) a) → f.support.card ≤ 1

Proof state:
case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
have : f.coeff i = 0 := by
  rw [← not_mem_support_iff]
  exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))

Result:
case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
this : f.coeff i = 0
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Proof state:
case mp.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ ∃ n a, f = (monomial n) a

Tactic:
refine ⟨n, f.coeff n, ?_⟩

Result:
case mp.intro
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
⊢ f = (monomial n) (f.coeff n)

Proof state:
case mp.intro.a
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
by_cases hi : i = n

Result:
case pos
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Proof state:
case pos
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
simp [hi, coeff_monomial]

Result:
no goals

Proof state:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : f.support.card ≤ 1
⊢ ∃ n a, f = (monomial n) a

Tactic:
rw [Finset.card_le_one_iff_subset_singleton] at H

Result:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
H : ∃ x, f.support ⊆ {x}
⊢ ∃ n a, f = (monomial n) a

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ (∃ n a, f = (monomial n) a) → f.support.card ≤ 1

Tactic:
rintro ⟨n, a, rfl⟩

Result:
case mpr.intro.intro
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support.card ≤ 1

Proof state:
case mpr.intro.intro
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support.card ≤ {n}.card

Tactic:
apply Finset.card_le_card

Result:
case mpr.intro.intro.a
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support ⊆ {n}

Proof state:
case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
this : f.coeff i = 0
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
simp [this, Ne.symm hi, coeff_monomial]

Result:
no goals