[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
⊢ Subsingleton R → (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b
[PROOFSTEP]
intro
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
a✝ : Subsingleton R
⊢ (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ p = X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
[PROOFSTEP]
conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
| p
[PROOFSTEP]
rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
| p
[PROOFSTEP]
rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
| p
[PROOFSTEP]
rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ ↑C (coeff p (natDegree p)) * X ^ natDegree p + ∑ x in range (natDegree p), ↑C (coeff p x) * X ^ x =
    X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
[PROOFSTEP]
suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
this : ↑C (coeff p (natDegree p)) = 1
⊢ ↑C (coeff p (natDegree p)) * X ^ natDegree p + ∑ x in range (natDegree p), ↑C (coeff p x) * X ^ x =
    X ^ natDegree p + ∑ i in range (natDegree p), ↑C (coeff p i) * X ^ i
[PROOFSTEP]
rw [this, one_mul]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ ↑C (coeff p (natDegree p)) = 1
[PROOFSTEP]
exact congr_arg C hp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
hq : Monic q
⊢ q ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r : R[X]
hp : p ≠ 0
hq : Monic 0
⊢ False
[PROOFSTEP]
rw [Monic.def, leadingCoeff_zero] at hq
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r : R[X]
hp : p ≠ 0
hq : 0 = 1
⊢ False
[PROOFSTEP]
rw [← mul_one p, ← C_1, ← hq, C_0, mul_zero] at hp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r : R[X]
hp : 0 ≠ 0
hq : 0 = 1
⊢ False
[PROOFSTEP]
exact hp rfl
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
⊢ Monic (Polynomial.map f p)
[PROOFSTEP]
unfold Monic
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
⊢ Polynomial.leadingCoeff (Polynomial.map f p) = 1
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
⊢ Polynomial.leadingCoeff (Polynomial.map f p) = 1
[PROOFSTEP]
have : f p.leadingCoeff ≠ 0 := by
  rw [show _ = _ from hp, f.map_one]
  exact one_ne_zero
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
⊢ ↑f (Polynomial.leadingCoeff p) ≠ 0
[PROOFSTEP]
rw [show _ = _ from hp, f.map_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
this : ↑f (Polynomial.leadingCoeff p) ≠ 0
⊢ Polynomial.leadingCoeff (Polynomial.map f p) = 1
[PROOFSTEP]
rw [Polynomial.leadingCoeff, coeff_map]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
this : ↑f (Polynomial.leadingCoeff p) ≠ 0
⊢ ↑f (coeff p (natDegree (Polynomial.map f p))) = 1
[PROOFSTEP]
suffices p.coeff (p.map f).natDegree = 1 by simp [this]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
this✝ : ↑f (Polynomial.leadingCoeff p) ≠ 0
this : coeff p (natDegree (Polynomial.map f p)) = 1
⊢ ↑f (coeff p (natDegree (Polynomial.map f p))) = 1
[PROOFSTEP]
simp [this]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
✝ : Nontrivial S
this : ↑f (Polynomial.leadingCoeff p) ≠ 0
⊢ coeff p (natDegree (Polynomial.map f p)) = 1
[PROOFSTEP]
rwa [natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f this)]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
⊢ Monic (↑C b * p)
[PROOFSTEP]
unfold Monic
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
⊢ leadingCoeff (↑C b * p) = 1
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
✝ : Nontrivial R
⊢ leadingCoeff (↑C b * p) = 1
[PROOFSTEP]
rw [leadingCoeff_mul' _]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
✝ : Nontrivial R
⊢ leadingCoeff (↑C b) * leadingCoeff p = 1
[PROOFSTEP]
simp [leadingCoeff_C b, hp]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : b * leadingCoeff p = 1
✝ : Nontrivial R
⊢ leadingCoeff (↑C b) * leadingCoeff p ≠ 0
[PROOFSTEP]
simp [leadingCoeff_C b, hp]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
⊢ Monic (p * ↑C b)
[PROOFSTEP]
unfold Monic
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
⊢ leadingCoeff (p * ↑C b) = 1
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
✝ : Nontrivial R
⊢ leadingCoeff (p * ↑C b) = 1
[PROOFSTEP]
rw [leadingCoeff_mul' _]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
✝ : Nontrivial R
⊢ leadingCoeff p * leadingCoeff (↑C b) = 1
[PROOFSTEP]
simp [leadingCoeff_C b, hp]
[GOAL]
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
✝ : Nontrivial R
⊢ leadingCoeff p * leadingCoeff (↑C b) ≠ 0
[PROOFSTEP]
simp [leadingCoeff_C b, hp]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
n : ℕ
H1 : degree p ≤ ↑n
H2 : coeff p n = 1
H : ¬degree p < ↑n
⊢ Monic p
[PROOFSTEP]
rwa [Monic, Polynomial.leadingCoeff, natDegree, (lt_or_eq_of_le H1).resolve_left H]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
n : ℕ
H : degree p ≤ ↑n
H1 : degree p < ↑(n + 1)
⊢ coeff (X ^ (n + 1) + p) (n + 1) = 1
[PROOFSTEP]
rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H1, add_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
h0 : ¬0 = 1
⊢ Monic (p * q)
[PROOFSTEP]
have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
h0 : ¬0 = 1
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
h0 : ¬0 = 1
this : Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
⊢ Monic (p * q)
[PROOFSTEP]
rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ Monic (p ^ (n + 1))
[PROOFSTEP]
rw [pow_succ]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ Monic (p * p ^ n)
[PROOFSTEP]
exact hp.mul (Monic.pow hp n)
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ Monic (p + q)
[PROOFSTEP]
rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hq : Monic q
hpq : degree p < degree q
⊢ Monic (p + q)
[PROOFSTEP]
rwa [Monic, leadingCoeff_add_of_degree_lt hpq]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hpq : Monic (p * q)
⊢ Monic q
[PROOFSTEP]
contrapose! hpq
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hpq : ¬Monic q
⊢ ¬Monic (p * q)
[PROOFSTEP]
rw [Monic.def] at hpq ⊢
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hpq : ¬Polynomial.leadingCoeff q = 1
⊢ ¬Polynomial.leadingCoeff (p * q) = 1
[PROOFSTEP]
rwa [leadingCoeff_monic_mul hp]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hq : Monic q
hpq : Monic (p * q)
⊢ Monic p
[PROOFSTEP]
contrapose! hpq
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hq : Monic q
hpq : ¬Monic p
⊢ ¬Monic (p * q)
[PROOFSTEP]
rw [Monic.def] at hpq ⊢
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hq : Monic q
hpq : ¬Polynomial.leadingCoeff p = 1
⊢ ¬Polynomial.leadingCoeff (p * q) = 1
[PROOFSTEP]
rwa [leadingCoeff_mul_monic hq]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ natDegree p = 0 ↔ p = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ natDegree p = 0 → p = 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ p = 1 → natDegree p = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = 1
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree p = 0
[PROOFSTEP]
swap
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree p = 0
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree 1 = 0
[PROOFSTEP]
exact natDegree_one
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = 1
[PROOFSTEP]
have : p = C (p.coeff 0) := by
  rw [← Polynomial.degree_le_zero_iff]
  rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = ↑C (coeff p 0)
[PROOFSTEP]
rw [← Polynomial.degree_le_zero_iff]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ degree p ≤ 0
[PROOFSTEP]
rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
this : p = ↑C (coeff p 0)
⊢ p = 1
[PROOFSTEP]
rw [this]
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
this : p = ↑C (coeff p 0)
⊢ ↑C (coeff p 0) = 1
[PROOFSTEP]
rw [← h, ← Polynomial.leadingCoeff, Monic.def.1 hp, C_1]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ degree p ≤ 0 ↔ p = 1
[PROOFSTEP]
rw [← hp.natDegree_eq_zero_iff_eq_one, natDegree_eq_zero_iff_degree_le_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
⊢ natDegree (p * q) = natDegree p + natDegree q
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ natDegree (p * q) = natDegree p + natDegree q
[PROOFSTEP]
apply natDegree_mul'
[GOAL]
case h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
simp [hp.leadingCoeff, hq.leadingCoeff]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
⊢ degree (p * q) = degree (q * p)
[PROOFSTEP]
by_cases h : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : q = 0
⊢ degree (p * q) = degree (q * p)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ degree (p * q) = degree (q * p)
[PROOFSTEP]
rw [degree_mul', hp.degree_mul]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ degree p + degree q = degree q + degree p
[PROOFSTEP]
exact add_comm _ _
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : q ≠ 0
⊢ natDegree (p * q) = natDegree p + natDegree q
[PROOFSTEP]
rw [natDegree_mul', add_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : q ≠ 0
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
⊢ natDegree (p * q) = natDegree (q * p)
[PROOFSTEP]
by_cases h : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : q = 0
⊢ natDegree (p * q) = natDegree (q * p)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ natDegree (p * q) = natDegree (q * p)
[PROOFSTEP]
rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hp : Monic p
q : R[X]
h : ¬q = 0
⊢ Polynomial.leadingCoeff q * Polynomial.leadingCoeff p ≠ 0
[PROOFSTEP]
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h0 : q ≠ 0
hl : natDegree q < natDegree p
⊢ ¬p ∣ q
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r✝ : R[X]
hp : Monic p
r : R[X]
h0 : p * r ≠ 0
hl : natDegree (p * r) < natDegree p
⊢ False
[PROOFSTEP]
rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r✝ : R[X]
hp : Monic p
r : R[X]
h0 : p * r ≠ 0
hl : natDegree p + natDegree r < natDegree p
⊢ False
[PROOFSTEP]
exact hl.not_le (Nat.le_add_right _ _)
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
⊢ nextCoeff (p * q) = nextCoeff p + nextCoeff q
[PROOFSTEP]
nontriviality
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ nextCoeff (p * q) = nextCoeff p + nextCoeff q
[PROOFSTEP]
simp only [← coeff_one_reverse]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ coeff (reverse (p * q)) 1 = coeff (reverse p) 1 + coeff (reverse q) 1
[PROOFSTEP]
rw [reverse_mul]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ coeff (reverse p * reverse q) 1 = coeff (reverse p) 1 + coeff (reverse q) 1
[PROOFSTEP]
simp [coeff_mul, Nat.antidiagonal, hp.leadingCoeff, hq.leadingCoeff, add_comm, show Nat.succ 0 = 1 from rfl]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
hq : Monic q
✝ : Nontrivial R
⊢ Polynomial.leadingCoeff p * Polynomial.leadingCoeff q ≠ 0
[PROOFSTEP]
simp [coeff_mul, Nat.antidiagonal, hp.leadingCoeff, hq.leadingCoeff, add_comm, show Nat.succ 0 = 1 from rfl]
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
⊢ p = 1
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
⊢ p = 1
[PROOFSTEP]
have hdeg : p.degree = 0 :=
  by
  rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
  · rw [hp.leadingCoeff, f.map_one]
    exact one_ne_zero
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
⊢ degree p = 0
[PROOFSTEP]
rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
⊢ ↑f (Polynomial.leadingCoeff p) ≠ 0
[PROOFSTEP]
rw [hp.leadingCoeff, f.map_one]
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
hdeg : degree p = 0
⊢ p = 1
[PROOFSTEP]
have hndeg : p.natDegree = 0 := WithBot.coe_eq_coe.mp ((degree_eq_natDegree hp.ne_zero).symm.trans hdeg)
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
hdeg : degree p = 0
hndeg : natDegree p = 0
⊢ p = 1
[PROOFSTEP]
convert eq_C_of_degree_eq_zero hdeg
[GOAL]
case h.e'_3
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p q r : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : Monic p
map_eq : Polynomial.map f p = 1
✝ : Nontrivial R
hdeg : degree p = 0
hndeg : natDegree p = 0
⊢ 1 = ↑C (coeff p 0)
[PROOFSTEP]
rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
⊢ natDegree (p ^ n) = n * natDegree p
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ natDegree (p ^ Nat.zero) = Nat.zero * natDegree p
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
n : ℕ
hn : natDegree (p ^ n) = n * natDegree p
⊢ natDegree (p ^ Nat.succ n) = Nat.succ n * natDegree p
[PROOFSTEP]
rw [pow_succ, hp.natDegree_mul (hp.pow n), hn, Nat.succ_mul, add_comm]
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ natDegree ((X + ↑C r) ^ n) = n
[PROOFSTEP]
rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hm : Monic p
hpu : IsUnit p
⊢ p = 1
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
⊢ p = 1
[PROOFSTEP]
obtain ⟨q, h⟩ := hpu.exists_right_inv
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
⊢ p = 1
[PROOFSTEP]
have := hm.natDegree_mul' (right_ne_zero_of_mul_eq_one h)
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree (p * q) = natDegree p + natDegree q
⊢ p = 1
[PROOFSTEP]
rw [h, natDegree_one, eq_comm, add_eq_zero_iff] at this
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q✝ r : R[X]
hm : Monic p
hpu : IsUnit p
✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : natDegree p = 0 ∧ natDegree q = 0
⊢ p = 1
[PROOFSTEP]
exact hm.natDegree_eq_zero_iff_eq_one.mp this.1
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
ht : ∀ (i : ι), i ∈ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f t))
[PROOFSTEP]
revert ht
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ t → Monic (f i)) → Monic (Multiset.prod (Multiset.map f t))
[PROOFSTEP]
refine' t.induction_on _ _
[GOAL]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ 0 → Monic (f i)) → Monic (Multiset.prod (Multiset.map f 0))
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ ∀ ⦃a : ι⦄ {s : Multiset ι},
    ((∀ (i : ι), i ∈ s → Monic (f i)) → Monic (Multiset.prod (Multiset.map f s))) →
      (∀ (i : ι), i ∈ a ::ₘ s → Monic (f i)) → Monic (Multiset.prod (Multiset.map f (a ::ₘ s)))
[PROOFSTEP]
intro a t ih ht
[GOAL]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ (i : ι), i ∈ t → Monic (f i)) → Monic (Multiset.prod (Multiset.map f t))
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f (a ::ₘ t)))
[PROOFSTEP]
rw [Multiset.map_cons, Multiset.prod_cons]
[GOAL]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ (i : ι), i ∈ t → Monic (f i)) → Monic (Multiset.prod (Multiset.map f t))
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (f a * Multiset.prod (Multiset.map f t))
[PROOFSTEP]
exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
h : ∀ (i : ι), i ∈ t → Monic (f i)
⊢ nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
[PROOFSTEP]
revert h
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
[PROOFSTEP]
refine' Multiset.induction_on t _ fun a t ih ht => _
[GOAL]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ (∀ (i : ι), i ∈ 0 → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f 0)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) 0)
[PROOFSTEP]
simp only [Multiset.not_mem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero, Multiset.prod_zero,
  Multiset.sum_zero, not_false_iff, forall_true_iff]
[GOAL]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff 1 = 0
[PROOFSTEP]
rw [← C_1]
[GOAL]
case refine'_1
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t : Multiset ι
f : ι → R[X]
⊢ nextCoeff (↑C 1) = 0
[PROOFSTEP]
rw [nextCoeff_C_eq_zero]
[GOAL]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ nextCoeff (Multiset.prod (Multiset.map f (a ::ₘ t))) =
    Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) (a ::ₘ t))
[PROOFSTEP]
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, Monic.nextCoeff_mul, ih]
[GOAL]
case refine'_2
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ ∀ (i : ι), i ∈ t → Monic (f i)
case refine'_2.hp
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (f a)
case refine'_2.hq
R : Type u
S : Type v
a✝ b : R
m n : ℕ
ι : Type y
inst✝ : CommSemiring R
p : R[X]
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih :
  (∀ (i : ι), i ∈ t → Monic (f i)) →
    nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun i => nextCoeff (f i)) t)
ht : ∀ (i : ι), i ∈ a ::ₘ t → Monic (f i)
⊢ Monic (Multiset.prod (Multiset.map f t))
[PROOFSTEP]
exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
  monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ natDegree (Polynomial.map f P) = natDegree P
[PROOFSTEP]
refine' le_antisymm (natDegree_map_le _ _) (le_natDegree_of_ne_zero _)
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ coeff (Polynomial.map f P) (natDegree P) ≠ 0
[PROOFSTEP]
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
⊢ degree (Polynomial.map f P) = degree P
[PROOFSTEP]
by_cases hP : P = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : P = 0
⊢ degree (Polynomial.map f P) = degree P
[PROOFSTEP]
simp [hP]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ degree (Polynomial.map f P) = degree P
[PROOFSTEP]
refine' le_antisymm (degree_map_le _ _) _
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ degree P ≤ degree (Polynomial.map f P)
[PROOFSTEP]
rw [degree_eq_natDegree hP]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ ↑(natDegree P) ≤ degree (Polynomial.map f P)
[PROOFSTEP]
refine' le_degree_of_ne_zero _
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ coeff (Polynomial.map f P) (natDegree P) ≠ 0
[PROOFSTEP]
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : Monic P
f : R →+* S
hP : ¬P = 0
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : p = 0
⊢ degree (map f p) = degree p
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : ¬p = 0
⊢ ↑f (leadingCoeff p) ≠ 0
[PROOFSTEP]
rw [← f.map_zero]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h : ¬p = 0
⊢ ↑f (leadingCoeff p) ≠ ↑f 0
[PROOFSTEP]
exact mt hf.eq_iff.1 (mt leadingCoeff_eq_zero.1 h)
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ leadingCoeff (map f p) = ↑f (leadingCoeff p)
[PROOFSTEP]
unfold leadingCoeff
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ coeff (map f p) (natDegree (map f p)) = ↑f (coeff p (natDegree p))
[PROOFSTEP]
rw [coeff_map, natDegree_map_eq_of_injective hf p]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ nextCoeff (map f p) = ↑f (nextCoeff p)
[PROOFSTEP]
unfold nextCoeff
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ (if natDegree (map f p) = 0 then 0 else coeff (map f p) (natDegree (map f p) - 1)) =
    ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
[PROOFSTEP]
rw [natDegree_map_eq_of_injective hf]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ (if natDegree p = 0 then 0 else coeff (map f p) (natDegree p - 1)) =
    ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h✝ : natDegree p = 0
⊢ 0 = ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
[PROOFSTEP]
simp [*]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
h✝ : ¬natDegree p = 0
⊢ coeff (map f p) (natDegree p - 1) = ↑f (if natDegree p = 0 then 0 else coeff p (natDegree p - 1))
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ leadingCoeff (map f p) = ↑f (leadingCoeff p)
[PROOFSTEP]
delta leadingCoeff
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
⊢ coeff (map f p) (natDegree (map f p)) = ↑f (coeff p (natDegree p))
[PROOFSTEP]
rw [coeff_map f, natDegree_map_eq_of_injective hf p]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
hp : Monic (map f p)
⊢ Monic p
[PROOFSTEP]
apply hf
[GOAL]
case a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ↑f
p : R[X]
hp : Monic (map f p)
⊢ ↑f (leadingCoeff p) = ↑f 1
[PROOFSTEP]
rw [← leadingCoeff_of_injective hf, hp.leadingCoeff, f.map_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p : R[X]
x : R
⊢ Monic (X - ↑C x)
[PROOFSTEP]
simpa only [sub_eq_add_neg, C_neg] using monic_X_add_C (-x)
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Ring R
p : R[X]
n : ℕ
H : degree p ≤ ↑n
⊢ Monic (X ^ (n + 1) - p)
[PROOFSTEP]
simpa [sub_eq_add_neg] using monic_X_pow_add (show degree (-p) ≤ n by rwa [← degree_neg p] at H )
[GOAL]
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Ring R
p : R[X]
n : ℕ
H : degree p ≤ ↑n
⊢ degree (-p) ≤ ↑n
[PROOFSTEP]
rwa [← degree_neg p] at H
[GOAL]
R✝ : Type u
S : Type v
a✝ b : R✝
m n✝ : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ Monic (X ^ n - ↑C a)
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
[GOAL]
case intro
R✝ : Type u
S : Type v
a✝ b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
k : ℕ
h : Nat.succ k ≠ 0
⊢ Monic (X ^ Nat.succ k - ↑C a)
[PROOFSTEP]
apply monic_X_pow_sub _
[GOAL]
R✝ : Type u
S : Type v
a✝ b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
k : ℕ
h : Nat.succ k ≠ 0
⊢ degree (↑C a) ≤ ↑k
[PROOFSTEP]
exact le_trans degree_C_le Nat.WithBot.coe_nonneg
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
m n✝ : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
⊢ ¬IsUnit (X ^ n - 1)
[PROOFSTEP]
intro h
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
m n✝ : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
⊢ False
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : IsUnit (X ^ 0 - 1)
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
case inr
R✝ : Type u
S : Type v
a b : R✝
m n✝ : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ False
[PROOFSTEP]
apply hn
[GOAL]
case inr
R✝ : Type u
S : Type v
a b : R✝
m n✝ : ℕ
ι : Type y
inst✝² : Ring R✝
p : R✝[X]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = 0
[PROOFSTEP]
rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ Monic (p - q)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ Monic (p + -q)
[PROOFSTEP]
apply hp.add_of_left
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ degree (-q) < degree p
[PROOFSTEP]
rwa [degree_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
⊢ Monic (p - q)
[PROOFSTEP]
have : (-q).coeff (-q).natDegree = 1 := by rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
⊢ coeff (-q) (natDegree (-q)) = 1
[PROOFSTEP]
rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ Monic (p - q)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ Monic (p + -q)
[PROOFSTEP]
apply Monic.add_of_right this
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ degree p < degree (-q)
[PROOFSTEP]
rwa [degree_neg]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
⊢ q * p ≠ 0
[PROOFSTEP]
by_cases h : p = 1
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0
[PROOFSTEP]
simpa [h]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ q * p ≠ 0
[PROOFSTEP]
rw [Ne.def, ← degree_eq_bot, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬degree p = ⊥
[PROOFSTEP]
refine' ⟨hq, _⟩
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬degree p = ⊥
[PROOFSTEP]
rw [← hp.degree_le_zero_iff_eq_one, not_le] at h
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ¬degree p = ⊥
[PROOFSTEP]
refine' (lt_trans _ h).ne'
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ⊥ < 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
⊢ p * q ≠ 0
[PROOFSTEP]
by_cases h : p = 1
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0
[PROOFSTEP]
simpa [h]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0
[PROOFSTEP]
rw [Ne.def, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬degree p = ⊥
[PROOFSTEP]
refine' ⟨hq, _⟩
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬degree p = ⊥
[PROOFSTEP]
rw [← hp.degree_le_zero_iff_eq_one, not_le] at h
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ¬degree p = ⊥
[PROOFSTEP]
refine' (lt_trans _ h).ne'
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ⊥ < 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
[PROOFSTEP]
suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
this : 0 < natDegree p ↔ natDegree p ≠ 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
[PROOFSTEP]
simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ 0 < natDegree p ↔ natDegree p ≠ 0
[PROOFSTEP]
exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : ¬q = 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
[PROOFSTEP]
simp [h.natDegree_mul', hq]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
⊢ p * q = 0 ↔ q = 0
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ p * q = 0 ↔ q = 0
[PROOFSTEP]
simp [h.mul_right_ne_zero, hq]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : ¬q = 0
⊢ p * q = 0 ↔ q = 0
[PROOFSTEP]
simp [h.mul_right_ne_zero, hq]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
⊢ q * p = 0 ↔ q = 0
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ q * p = 0 ↔ q = 0
[PROOFSTEP]
simp [h.mul_left_ne_zero, hq]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : ¬q = 0
⊢ q * p = 0 ↔ q = 0
[PROOFSTEP]
simp [h.mul_left_ne_zero, hq]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsRegular p
[PROOFSTEP]
constructor
[GOAL]
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsLeftRegular p
[PROOFSTEP]
intro q r h
[GOAL]
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : (fun x => p * x) q = (fun x => p * x) r
⊢ q = r
[PROOFSTEP]
dsimp only at h
[GOAL]
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : p * q = p * r
⊢ q = r
[PROOFSTEP]
rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
[GOAL]
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsRightRegular p
[PROOFSTEP]
intro q r h
[GOAL]
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : (fun x => x * p) q = (fun x => x * p) r
⊢ q = r
[PROOFSTEP]
simp only at h
[GOAL]
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : q * p = r * p
⊢ q = r
[PROOFSTEP]
rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree (k • p) = degree p
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree (k • p) ≤ degree p
[PROOFSTEP]
rw [degree_le_iff_coeff_zero]
[GOAL]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), degree p < ↑m → coeff (k • p) m = 0
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : degree p < ↑m
⊢ coeff (k • p) m = 0
[PROOFSTEP]
rw [degree_lt_iff_coeff_zero] at hm
[GOAL]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff p m_1 = 0
⊢ coeff (k • p) m = 0
[PROOFSTEP]
simp [hm m le_rfl]
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree p ≤ degree (k • p)
[PROOFSTEP]
rw [degree_le_iff_coeff_zero]
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), degree (k • p) < ↑m → coeff p m = 0
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : degree (k • p) < ↑m
⊢ coeff p m = 0
[PROOFSTEP]
rw [degree_lt_iff_coeff_zero] at hm
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff (k • p) m_1 = 0
⊢ coeff p m = 0
[PROOFSTEP]
refine' h _
[GOAL]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff (k • p) m_1 = 0
⊢ (fun x => k • x) (coeff p m) = (fun x => k • x) 0
[PROOFSTEP]
simpa using hm m le_rfl
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ natDegree (k • p) = natDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : p = 0
⊢ natDegree (k • p) = natDegree p
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ natDegree (k • p) = natDegree p
[PROOFSTEP]
rw [← WithBot.coe_eq_coe, ← Nat.cast_withBot, ← Nat.cast_withBot, ← degree_eq_natDegree hp, ← degree_eq_natDegree,
  degree_smul_of_smul_regular p h]
[GOAL]
case neg
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ k • p ≠ 0
[PROOFSTEP]
contrapose! hp
[GOAL]
case neg
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = 0
⊢ p = 0
[PROOFSTEP]
rw [← smul_zero k] at hp
[GOAL]
case neg
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp✝ : k • p = 0
hp : k • p = k • 0
⊢ p = 0
[PROOFSTEP]
exact h.polynomial hp
[GOAL]
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ leadingCoeff (k • p) = k • leadingCoeff p
[PROOFSTEP]
rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul, natDegree_smul_of_smul_regular p h]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ Monic ((IsUnit.unit h)⁻¹ • p)
[PROOFSTEP]
rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ ↑(IsUnit.unit h)⁻¹ • leadingCoeff p = 1
[PROOFSTEP]
obtain ⟨k, hk⟩ := h
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = leadingCoeff p
⊢ ↑(IsUnit.unit (_ : ∃ u, ↑u = leadingCoeff p))⁻¹ • leadingCoeff p = 1
[PROOFSTEP]
simp only [← hk, smul_eq_mul, ← Units.val_mul, Units.val_eq_one, inv_mul_eq_iff_eq_mul]
[GOAL]
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
k : Rˣ
hk : ↑k = leadingCoeff p
⊢ k = IsUnit.unit (_ : IsUnit ↑k) * 1
[PROOFSTEP]
simp [Units.ext_iff, IsUnit.unit_spec]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ p * q = 0 ↔ q = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ p * q = 0 → q = 0
[PROOFSTEP]
intro hp
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : p * q = 0
⊢ q = 0
[PROOFSTEP]
rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
⊢ q = 0
[PROOFSTEP]
have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
  ext
  simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
  refine' sum_congr rfl fun x _ => _
  rw [← mul_assoc]
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
⊢ (IsUnit.unit h)⁻¹ • (p * q) = (IsUnit.unit h)⁻¹ • p * q
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ coeff ((IsUnit.unit h)⁻¹ • (p * q)) n✝ = coeff ((IsUnit.unit h)⁻¹ • p * q) n✝
[PROOFSTEP]
simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
[GOAL]
case a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
⊢ ∑ x in Nat.antidiagonal n✝, ↑(IsUnit.unit h)⁻¹ * (coeff p x.fst * coeff q x.snd) =
    ∑ x in Nat.antidiagonal n✝, ↑(IsUnit.unit h)⁻¹ * coeff p x.fst * coeff q x.snd
[PROOFSTEP]
refine' sum_congr rfl fun x _ => _
[GOAL]
case a
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
n✝ : ℕ
x : ℕ × ℕ
x✝ : x ∈ Nat.antidiagonal n✝
⊢ ↑(IsUnit.unit h)⁻¹ * (coeff p x.fst * coeff q x.snd) = ↑(IsUnit.unit h)⁻¹ * coeff p x.fst * coeff q x.snd
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • (p * q) = 0
this : (IsUnit.unit h)⁻¹ • (p * q) = (IsUnit.unit h)⁻¹ • p * q
⊢ q = 0
[PROOFSTEP]
rwa [this, Monic.mul_right_eq_zero_iff] at hp
[GOAL]
case mp.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp✝ : p * q = 0
hp : (IsUnit.unit h)⁻¹ • p * q = 0
this : (IsUnit.unit h)⁻¹ • (p * q) = (IsUnit.unit h)⁻¹ • p * q
⊢ Monic ((IsUnit.unit h)⁻¹ • p)
[PROOFSTEP]
exact monic_of_isUnit_leadingCoeff_inv_smul _
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q = 0 → p * q = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ p * 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q * p = 0 ↔ q = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q * p = 0 → q = 0
[PROOFSTEP]
intro hp
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * p = 0
⊢ q = 0
[PROOFSTEP]
replace hp := congr_arg (· * C ↑h.unit⁻¹) hp
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : (fun x => x * ↑C ↑(IsUnit.unit h)⁻¹) (q * p) = (fun x => x * ↑C ↑(IsUnit.unit h)⁻¹) 0
⊢ q = 0
[PROOFSTEP]
simp only [zero_mul] at hp
[GOAL]
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * p * ↑C ↑(IsUnit.unit h)⁻¹ = 0
⊢ q = 0
[PROOFSTEP]
rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp
[GOAL]
case mp.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * (p * ↑C ↑(IsUnit.unit h)⁻¹) = 0
⊢ Monic (p * ↑C ↑(IsUnit.unit h)⁻¹)
[PROOFSTEP]
refine' monic_mul_C_of_leadingCoeff_mul_eq_one _
[GOAL]
case mp.h
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
hp : q * (p * ↑C ↑(IsUnit.unit h)⁻¹) = 0
⊢ leadingCoeff p * ↑(IsUnit.unit h)⁻¹ = 1
[PROOFSTEP]
simp [Units.mul_inv_eq_iff_eq_mul, IsUnit.unit_spec]
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
q : R[X]
⊢ q = 0 → q * p = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : IsUnit (leadingCoeff p)
⊢ 0 * p = 0
[PROOFSTEP]
rw [zero_mul]


[GOAL]
l : List Bool
b : Bool
⊢ count (!b) l + count b l = length l
[PROOFSTEP]
simp only [length_eq_countp_add_countp (· == !b), count, add_right_inj]
[GOAL]
l : List Bool
b : Bool
⊢ countp (fun x => x == b) l = countp (fun a => decide ¬(a == !b) = true) l
[PROOFSTEP]
suffices : (fun x => x == b) = (fun a => decide ¬(a == !b) = true)
[GOAL]
l : List Bool
b : Bool
this : (fun x => x == b) = fun a => decide ¬(a == !b) = true
⊢ countp (fun x => x == b) l = countp (fun a => decide ¬(a == !b) = true) l
case this l : List Bool b : Bool ⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
[PROOFSTEP]
rw [this]
[GOAL]
case this
l : List Bool
b : Bool
⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
[PROOFSTEP]
ext x
[GOAL]
case this.h
l : List Bool
b x : Bool
⊢ (x == b) = decide ¬(x == !b) = true
[PROOFSTEP]
cases x
[GOAL]
case this.h.false
l : List Bool
b : Bool
⊢ (false == b) = decide ¬(false == !b) = true
[PROOFSTEP]
cases b
[GOAL]
case this.h.true
l : List Bool
b : Bool
⊢ (true == b) = decide ¬(true == !b) = true
[PROOFSTEP]
cases b
[GOAL]
case this.h.false.false
l : List Bool
⊢ (false == false) = decide ¬(false == !false) = true
[PROOFSTEP]
rfl
[GOAL]
case this.h.false.true
l : List Bool
⊢ (false == true) = decide ¬(false == !true) = true
[PROOFSTEP]
rfl
[GOAL]
case this.h.true.false
l : List Bool
⊢ (true == false) = decide ¬(true == !false) = true
[PROOFSTEP]
rfl
[GOAL]
case this.h.true.true
l : List Bool
⊢ (true == true) = decide ¬(true == !true) = true
[PROOFSTEP]
rfl
[GOAL]
l : List Bool
b : Bool
⊢ count b l + count (!b) l = length l
[PROOFSTEP]
rw [add_comm, count_not_add_count]
[GOAL]
b x : Bool
l : List Bool
h : Chain (fun x x_1 => x ≠ x_1) b (x :: l)
⊢ count (!b) (x :: l) = count b (x :: l) + length (x :: l) % 2
[PROOFSTEP]
obtain rfl : b = !x := Bool.eq_not_iff.2 (rel_of_chain_cons h)
[GOAL]
x : Bool
l : List Bool
h : Chain (fun x x_1 => x ≠ x_1) (!x) (x :: l)
⊢ count (!!x) (x :: l) = count (!x) (x :: l) + length (x :: l) % 2
[PROOFSTEP]
rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self, Chain.count_not (chain_of_chain_cons h), length,
  add_assoc, Nat.mod_two_add_succ_mod_two]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
h2 : Even (length l)
b : Bool
⊢ count (!b) l = count b l
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
h2 : Even (length [])
⊢ count (!b) [] = count b []
[PROOFSTEP]
rfl
[GOAL]
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : Even (length (x :: l))
⊢ count (!b) (x :: l) = count b (x :: l)
[PROOFSTEP]
rw [length_cons, Nat.even_add_one, Nat.not_even_iff] at h2
[GOAL]
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
⊢ count (!b) (x :: l) = count b (x :: l)
[PROOFSTEP]
suffices count (!x) (x :: l) = count x (x :: l) by
  -- Porting note: old proof is
      -- cases b <;> cases x <;> try exact this;cases b <;> cases x <;> revert this <;>
          simp only [Bool.not_false, Bool.not_true] <;>
        intro this <;>
      (try exact this) <;>
    exact this.symm
[GOAL]
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
this : count (!x) (x :: l) = count x (x :: l)
⊢ count (!b) (x :: l) = count b (x :: l)
[PROOFSTEP]
cases b
[GOAL]
case false
x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
this : count (!x) (x :: l) = count x (x :: l)
⊢ count (!false) (x :: l) = count false (x :: l)
[PROOFSTEP]
cases x
[GOAL]
case true
x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
this : count (!x) (x :: l) = count x (x :: l)
⊢ count (!true) (x :: l) = count true (x :: l)
[PROOFSTEP]
cases x
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count (!false) (false :: l) = count false (false :: l)
⊢ count (!false) (false :: l) = count false (false :: l)
[PROOFSTEP]
revert this
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count (!true) (true :: l) = count true (true :: l)
⊢ count (!false) (true :: l) = count false (true :: l)
[PROOFSTEP]
revert this
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count (!false) (false :: l) = count false (false :: l)
⊢ count (!true) (false :: l) = count true (false :: l)
[PROOFSTEP]
revert this
[GOAL]
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count (!true) (true :: l) = count true (true :: l)
⊢ count (!true) (true :: l) = count true (true :: l)
[PROOFSTEP]
revert this
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
⊢ count (!false) (false :: l) = count false (false :: l) → count (!false) (false :: l) = count false (false :: l)
[PROOFSTEP]
simp only [Bool.not_false, Bool.not_true]
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
⊢ count (!true) (true :: l) = count true (true :: l) → count (!false) (true :: l) = count false (true :: l)
[PROOFSTEP]
simp only [Bool.not_false, Bool.not_true]
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
⊢ count (!false) (false :: l) = count false (false :: l) → count (!true) (false :: l) = count true (false :: l)
[PROOFSTEP]
simp only [Bool.not_false, Bool.not_true]
[GOAL]
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
⊢ count (!true) (true :: l) = count true (true :: l) → count (!true) (true :: l) = count true (true :: l)
[PROOFSTEP]
simp only [Bool.not_false, Bool.not_true]
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
⊢ count true (false :: l) = count false (false :: l) → count true (false :: l) = count false (false :: l)
[PROOFSTEP]
intro this
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
⊢ count false (true :: l) = count true (true :: l) → count true (true :: l) = count false (true :: l)
[PROOFSTEP]
intro this
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
⊢ count true (false :: l) = count false (false :: l) → count false (false :: l) = count true (false :: l)
[PROOFSTEP]
intro this
[GOAL]
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
⊢ count false (true :: l) = count true (true :: l) → count false (true :: l) = count true (true :: l)
[PROOFSTEP]
intro this
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count true (false :: l) = count false (false :: l)
[PROOFSTEP]
try exact this
[GOAL]
case false.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count true (false :: l) = count false (false :: l)
[PROOFSTEP]
exact this
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count true (true :: l) = count false (true :: l)
[PROOFSTEP]
try exact this
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count true (true :: l) = count false (true :: l)
[PROOFSTEP]
exact this
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count false (false :: l) = count true (false :: l)
[PROOFSTEP]
try exact this
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count false (false :: l) = count true (false :: l)
[PROOFSTEP]
exact this
[GOAL]
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count false (true :: l) = count true (true :: l)
[PROOFSTEP]
try exact this
[GOAL]
case true.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count false (true :: l) = count true (true :: l)
[PROOFSTEP]
exact this
[GOAL]
case false.true
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (true :: l)
this : count false (true :: l) = count true (true :: l)
⊢ count true (true :: l) = count false (true :: l)
[PROOFSTEP]
exact this.symm
[GOAL]
case true.false
l : List Bool
h2 : length l % 2 = 1
hl : Chain' (fun x x_1 => x ≠ x_1) (false :: l)
this : count true (false :: l) = count false (false :: l)
⊢ count false (false :: l) = count true (false :: l)
[PROOFSTEP]
exact this.symm
[GOAL]
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : length l % 2 = 1
⊢ count (!x) (x :: l) = count x (x :: l)
[PROOFSTEP]
rw [count_cons_of_ne x.not_ne_self, hl.count_not, h2, count_cons_self]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ count (!b) l ≤ count b l + 1
[PROOFSTEP]
cases' l with x l
[GOAL]
case nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
⊢ count (!b) [] ≤ count b [] + 1
[PROOFSTEP]
exact zero_le _
[GOAL]
case cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count (!b) (x :: l) ≤ count b (x :: l) + 1
[PROOFSTEP]
obtain rfl | rfl : b = x ∨ b = !x := by simp only [Bool.eq_not_iff, em]
[GOAL]
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ b = x ∨ b = !x
[PROOFSTEP]
simp only [Bool.eq_not_iff, em]
[GOAL]
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (b :: l)
⊢ count (!b) (b :: l) ≤ count b (b :: l) + 1
[PROOFSTEP]
rw [count_cons_of_ne b.not_ne_self, count_cons_self, hl.count_not, add_assoc]
[GOAL]
case cons.inl
b : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (b :: l)
⊢ count b l + length l % 2 ≤ count b l + (1 + 1)
[PROOFSTEP]
exact add_le_add_left (Nat.mod_lt _ two_pos).le _
[GOAL]
case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count (!!x) (x :: l) ≤ count (!x) (x :: l) + 1
[PROOFSTEP]
rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self, hl.count_not]
[GOAL]
case cons.inr
x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
⊢ count x l + 1 ≤ count x l + length l % 2 + 1
[PROOFSTEP]
exact add_le_add_right (le_add_right le_rfl) _
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
h2 : Even (length l)
b : Bool
⊢ 2 * count b l = length l
[PROOFSTEP]
rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ 2 * count b l =
    if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
[PROOFSTEP]
by_cases h2 : Even (length l)
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h2 : Even (length l)
⊢ 2 * count b l =
    if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
[PROOFSTEP]
rw [if_pos h2, hl.two_mul_count_bool_of_even h2]
[GOAL]
case neg
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h2 : ¬Even (length l)
⊢ 2 * count b l =
    if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
[PROOFSTEP]
cases' l with x l
[GOAL]
case neg.nil
b : Bool
hl : Chain' (fun x x_1 => x ≠ x_1) []
h2 : ¬Even (length [])
⊢ 2 * count b [] =
    if Even (length []) then length [] else if (some b == head? []) = true then length [] + 1 else length [] - 1
[PROOFSTEP]
exact (h2 even_zero).elim
[GOAL]
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : ¬Even (length (x :: l))
⊢ 2 * count b (x :: l) =
    if Even (length (x :: l)) then length (x :: l)
    else if (some b == head? (x :: l)) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
simp only [if_neg h2, count_cons', mul_add, head?, Option.mem_some_iff, @eq_comm _ x]
[GOAL]
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : ¬Even (length (x :: l))
⊢ (2 * count b l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
rw [length_cons, Nat.even_add_one, not_not] at h2
[GOAL]
case neg.cons
b x : Bool
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) (x :: l)
h2 : Even (length l)
⊢ (2 * count b l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
replace hl : l.Chain' (· ≠ ·) := hl.tail
[GOAL]
case neg.cons
b x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (2 * count b l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
rw [hl.two_mul_count_bool_of_even h2]
[GOAL]
case neg.cons
b x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if b = x then 1 else 0) =
    if (some b == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
cases b
[GOAL]
case neg.cons.false
x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if false = x then 1 else 0) =
    if (some false == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
cases x
[GOAL]
case neg.cons.true
x : Bool
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if true = x then 1 else 0) =
    if (some true == some x) = true then length (x :: l) + 1 else length (x :: l) - 1
[PROOFSTEP]
cases x
[GOAL]
case neg.cons.false.false
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if false = false then 1 else 0) =
    if (some false == some false) = true then length (false :: l) + 1 else length (false :: l) - 1
[PROOFSTEP]
split_ifs
[GOAL]
case neg.cons.false.true
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if false = true then 1 else 0) =
    if (some false == some true) = true then length (true :: l) + 1 else length (true :: l) - 1
[PROOFSTEP]
split_ifs
[GOAL]
case neg.cons.true.false
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if true = false then 1 else 0) =
    if (some true == some false) = true then length (false :: l) + 1 else length (false :: l) - 1
[PROOFSTEP]
split_ifs
[GOAL]
case neg.cons.true.true
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
⊢ (length l + 2 * if true = true then 1 else 0) =
    if (some true == some true) = true then length (true :: l) + 1 else length (true :: l) - 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : false = false
h✝ : (some false == some false) = true
⊢ length l + 2 * 1 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : false = false
h✝ : ¬(some false == some false) = true
⊢ length l + 2 * 1 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬false = false
h✝ : (some false == some false) = true
⊢ length l + 2 * 0 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬false = false
h✝ : ¬(some false == some false) = true
⊢ length l + 2 * 0 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : False
h✝ : (some false == some true) = true
⊢ length l + 2 * 1 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : False
h✝ : ¬(some false == some true) = true
⊢ length l + 2 * 1 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : ¬False
h✝ : (some false == some true) = true
⊢ length l + 2 * 0 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : ¬False
h✝ : ¬(some false == some true) = true
⊢ length l + 2 * 0 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : False
h✝ : (some false == some true) = true
⊢ length l + 2 * 1 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : False
h✝ : ¬(some false == some true) = true
⊢ length l + 2 * 1 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : ¬False
h✝ : (some false == some true) = true
⊢ length l + 2 * 0 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : ¬False
h✝ : ¬(some false == some true) = true
⊢ length l + 2 * 0 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : False
h✝ : (some true == some false) = true
⊢ length l + 2 * 1 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : False
h✝ : ¬(some true == some false) = true
⊢ length l + 2 * 1 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : ¬False
h✝ : (some true == some false) = true
⊢ length l + 2 * 0 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : ¬False
h✝ : ¬(some true == some false) = true
⊢ length l + 2 * 0 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : False
h✝ : (some true == some false) = true
⊢ length l + 2 * 1 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : False
h✝ : ¬(some true == some false) = true
⊢ length l + 2 * 1 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : ¬False
h✝ : (some true == some false) = true
⊢ length l + 2 * 0 = length (false :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : ¬False
h✝ : ¬(some true == some false) = true
⊢ length l + 2 * 0 = length (false :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : true = true
h✝ : (some true == some true) = true
⊢ length l + 2 * 1 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : true = true
h✝ : ¬(some true == some true) = true
⊢ length l + 2 * 1 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬true = true
h✝ : (some true == some true) = true
⊢ length l + 2 * 0 = length (true :: l) + 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬true = true
h✝ : ¬(some true == some true) = true
⊢ length l + 2 * 0 = length (true :: l) - 1
[PROOFSTEP]
simp
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : false = false
h✝ : ¬(some false == some false) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬false = false
h✝ : (some false == some false) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : False
h✝ : ¬(some false == some true) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : false = true
h✝¹ : ¬False
h✝ : (some false == some true) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : False
h✝ : ¬(some false == some true) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬false = true
h✝¹ : ¬False
h✝ : (some false == some true) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : False
h✝ : ¬(some true == some false) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : true = false
h✝¹ : ¬False
h✝ : (some true == some false) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : False
h✝ : ¬(some true == some false) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝² : ¬true = false
h✝¹ : ¬False
h✝ : (some true == some false) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
case neg
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : true = true
h✝ : ¬(some true == some true) = true
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case pos
l : List Bool
h2 : Even (length l)
hl : Chain' (fun x x_1 => x ≠ x_1) l
h✝¹ : ¬true = true
h✝ : (some true == some true) = true
⊢ length l = Nat.succ (length l) + 1
[PROOFSTEP]
contradiction
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - 1 ≤ 2 * count b l
[PROOFSTEP]
rw [hl.two_mul_count_bool_eq_ite]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - 1 ≤ if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝ : Even (length l)
⊢ length l - 1 ≤ length l
[PROOFSTEP]
simp [le_tsub_add, Nat.le_succ_of_le]
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝¹ : ¬Even (length l)
h✝ : (some b == head? l) = true
⊢ length l - 1 ≤ length l + 1
[PROOFSTEP]
simp [le_tsub_add, Nat.le_succ_of_le]
[GOAL]
case neg
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝¹ : ¬Even (length l)
h✝ : ¬(some b == head? l) = true
⊢ length l - 1 ≤ length l - 1
[PROOFSTEP]
simp [le_tsub_add, Nat.le_succ_of_le]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l / 2 ≤ count b l
[PROOFSTEP]
rw [Nat.div_le_iff_le_mul_add_pred two_pos, ← tsub_le_iff_right]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ length l - (2 - 1) ≤ 2 * count b l
[PROOFSTEP]
exact length_sub_one_le_two_mul_count_bool hl b
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ 2 * count b l ≤ length l + 1
[PROOFSTEP]
rw [hl.two_mul_count_bool_eq_ite]
[GOAL]
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
⊢ (if Even (length l) then length l else if (some b == head? l) = true then length l + 1 else length l - 1) ≤
    length l + 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝ : Even (length l)
⊢ length l ≤ length l + 1
[PROOFSTEP]
simp [Nat.le_succ_of_le]
[GOAL]
case pos
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝¹ : ¬Even (length l)
h✝ : (some b == head? l) = true
⊢ length l + 1 ≤ length l + 1
[PROOFSTEP]
simp [Nat.le_succ_of_le]
[GOAL]
case neg
l : List Bool
hl : Chain' (fun x x_1 => x ≠ x_1) l
b : Bool
h✝¹ : ¬Even (length l)
h✝ : ¬(some b == head? l) = true
⊢ length l - 1 ≤ length l + 1
[PROOFSTEP]
simp [Nat.le_succ_of_le]


[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ List.NodupKeys (List.map Prod.toSigma (Finset.toList (graph f)))
[PROOFSTEP]
rw [List.NodupKeys, List.keys, List.map_map, Prod.fst_comp_toSigma, List.nodup_map_iff_inj_on]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ ∀ (x : α × M), x ∈ Finset.toList (graph f) → ∀ (y : α × M), y ∈ Finset.toList (graph f) → x.fst = y.fst → x = y
[PROOFSTEP]
rintro ⟨b, m⟩ hb ⟨c, n⟩ hc (rfl : b = c)
[GOAL]
case mk.mk
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : (b, m) ∈ Finset.toList (graph f)
n : M
hc : (b, n) ∈ Finset.toList (graph f)
⊢ (b, m) = (b, n)
[PROOFSTEP]
rw [Finset.mem_toList, Finsupp.mem_graph_iff] at hb hc
[GOAL]
case mk.mk
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : ↑f (b, m).fst = (b, m).snd ∧ (b, m).snd ≠ 0
n : M
hc : ↑f (b, n).fst = (b, n).snd ∧ (b, n).snd ≠ 0
⊢ (b, m) = (b, n)
[PROOFSTEP]
dsimp at hb hc
[GOAL]
case mk.mk
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
b : α
m : M
hb : ↑f b = m ∧ ¬m = 0
n : M
hc : ↑f b = n ∧ ¬n = 0
⊢ (b, m) = (b, n)
[PROOFSTEP]
rw [← hc.1, hb.1]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ List.Nodup (Finset.toList (graph f))
[PROOFSTEP]
apply Finset.nodup_toList
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ List.toFinset (AList.keys (toAList f)) = f.support
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a✝ : α
⊢ a✝ ∈ List.toFinset (AList.keys (toAList f)) ↔ a✝ ∈ f.support
[PROOFSTEP]
simp [toAList, AList.mem_keys, AList.keys, List.keys]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ toAList f ↔ ↑f x ≠ 0
[PROOFSTEP]
classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ toAList f ↔ ↑f x ≠ 0
[PROOFSTEP]
rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
⊢ Finset α
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
this : DecidableEq α
⊢ Finset α
[PROOFSTEP]
haveI := Classical.decEq M
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
this✝ : DecidableEq α
this : DecidableEq M
⊢ Finset α
[PROOFSTEP]
exact (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
⊢ a ∈ toFinset (List.keys (filter (fun x => decide (x.snd ≠ 0)) l.entries)) ↔
    (fun a => Option.getD (lookup a l) 0) a ≠ 0
[PROOFSTEP]
classical
simp_rw [@mem_toFinset _ _, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
cases lookup a l <;> simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
⊢ a ∈ toFinset (List.keys (filter (fun x => decide (x.snd ≠ 0)) l.entries)) ↔
    (fun a => Option.getD (lookup a l) 0) a ≠ 0
[PROOFSTEP]
simp_rw [@mem_toFinset _ _, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
⊢ (∃ b, b ∈ lookup a l ∧ decide (b ≠ 0) = true) ↔ Option.getD (lookup a l) 0 ≠ 0
[PROOFSTEP]
cases lookup a l
[GOAL]
case none
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
⊢ (∃ b, b ∈ none ∧ decide (b ≠ 0) = true) ↔ Option.getD none 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x => M
a : α
val✝ : M
⊢ (∃ b, b ∈ some val✝ ∧ decide (b ≠ 0) = true) ↔ Option.getD (some val✝) 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ ↑(lookupFinsupp l) a = Option.getD (lookup a l) 0
[PROOFSTEP]
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ Option.getD (lookup a l) 0 = Option.getD (lookup a l) 0
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (lookupFinsupp l).support = toFinset (List.keys (filter (fun x => decide (x.snd ≠ 0)) l.entries))
[PROOFSTEP]
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
[GOAL]
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ toFinset (List.keys (filter (fun x => decide ¬x.snd = 0) l.entries)) =
    toFinset (List.keys (filter (fun x => decide ¬x.snd = 0) l.entries))
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun a b => Classical.decEq α a b) = fun a b => inst✝¹ a b
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case h.e_3.h.e_a.e_p
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
⊢ (fun x => decide ¬x.snd = 0) = fun x => decide ¬x.snd = 0
[PROOFSTEP]
funext
[GOAL]
case h.e_3.h.e_a.e_p.h
α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x => M
x✝ : (_ : α) × M
⊢ (decide ¬x✝.snd = 0) = decide ¬x✝.snd = 0
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ ↑(lookupFinsupp l) a = x ↔ x ∈ lookup a l
[PROOFSTEP]
rw [lookupFinsupp_apply]
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ Option.getD (lookup a l) 0 = x ↔ x ∈ lookup a l
[PROOFSTEP]
cases' lookup a l with m
[GOAL]
case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ Option.getD none 0 = x ↔ x ∈ none
[PROOFSTEP]
simp [hx.symm]
[GOAL]
case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
m : M
⊢ Option.getD (some m) 0 = x ↔ x ∈ some m
[PROOFSTEP]
simp [hx.symm]
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ ↑(lookupFinsupp l) a = 0 ↔ ¬a ∈ l ∨ 0 ∈ lookup a l
[PROOFSTEP]
rw [lookupFinsupp_apply, ← lookup_eq_none]
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ Option.getD (lookup a l) 0 = 0 ↔ lookup a l = none ∨ 0 ∈ lookup a l
[PROOFSTEP]
cases' lookup a l with m
[GOAL]
case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ Option.getD none 0 = 0 ↔ none = none ∨ 0 ∈ none
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
⊢ Option.getD (some m) 0 = 0 ↔ some m = none ∨ 0 ∈ some m
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ lookupFinsupp ∅ = 0
[PROOFSTEP]
classical
ext
simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ lookupFinsupp ∅ = 0
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
a✝ : α
⊢ ↑(lookupFinsupp ∅) a✝ = ↑0 a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
⊢ lookupFinsupp (insert a m l) = Finsupp.update (lookupFinsupp l) a m
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
⊢ ↑(lookupFinsupp (insert a m l)) b = ↑(Finsupp.update (lookupFinsupp l) a m) b
[PROOFSTEP]
by_cases h : b = a
[GOAL]
case pos
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
h : b = a
⊢ ↑(lookupFinsupp (insert a m l)) b = ↑(Finsupp.update (lookupFinsupp l) a m) b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
h : ¬b = a
⊢ ↑(lookupFinsupp (insert a m l)) b = ↑(Finsupp.update (lookupFinsupp l) a m) b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ lookupFinsupp (singleton a m) = Finsupp.single a m
[PROOFSTEP]
classical
  -- porting note: was `simp [←AList.insert_empty]` but timeout issuessimp only [← AList.insert_empty,
  insert_lookupFinsupp, empty_lookupFinsupp, Finsupp.zero_update]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ lookupFinsupp (singleton a m) = Finsupp.single a m
[PROOFSTEP]
simp only [← AList.insert_empty, insert_lookupFinsupp, empty_lookupFinsupp, Finsupp.zero_update]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ lookupFinsupp (Finsupp.toAList f) = f
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
classical
by_cases h : f a = 0
· suffices f.toAList.lookup a = none by simp [h, this]
  · simp [lookup_eq_none, h]
· suffices f.toAList.lookup a = some (f a) by simp [h, this]
  · apply mem_lookup_iff.2
    simpa using h
[GOAL]
case h
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
by_cases h : f a = 0
[GOAL]
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
suffices f.toAList.lookup a = none by simp [h, this]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
this : lookup a (Finsupp.toAList f) = none
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
simp [h, this]
[GOAL]
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ↑f a = 0
⊢ lookup a (Finsupp.toAList f) = none
[PROOFSTEP]
simp [lookup_eq_none, h]
[GOAL]
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
suffices f.toAList.lookup a = some (f a) by simp [h, this]
[GOAL]
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
this : lookup a (Finsupp.toAList f) = some (↑f a)
⊢ ↑(lookupFinsupp (Finsupp.toAList f)) a = ↑f a
[PROOFSTEP]
simp [h, this]
[GOAL]
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ lookup a (Finsupp.toAList f) = some (↑f a)
[PROOFSTEP]
apply mem_lookup_iff.2
[GOAL]
case neg
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : ¬↑f a = 0
⊢ { fst := a, snd := ↑f a } ∈ (Finsupp.toAList f).entries
[PROOFSTEP]
simpa using h