mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case isUnit_or_isUnit.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
·

Goal state after:
case isUnit_or_isUnit.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f.mirror
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (m, n - m) ∉ antidiagonal n →
    (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) = 0

Tactic:
·

Goal state after:
case h₁
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (m, n - m) ∉ antidiagonal n →
    (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) = 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

pp: case monomial.inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hnk : n < k
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

Tactic:
·

Goal state after:
case monomial.inl
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case monomial.inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hnk : n < k
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

Tactic:
·

Goal state after:
case monomial.inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hnk : n < k
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case monomial.inr
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hnk : n < k
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

Tactic:
· aesop (add simp homogenize_monomial_of_lt) (add simp coeff_monomial)

Goal state after:
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : i ≤ p.natDegree
⊢ p.coeff i = 0

pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : p.natDegree < i
⊢ p.coeff i = 0

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : i ≤ p.natDegree
⊢ p.coeff i = 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : p.natDegree < i
⊢ p.coeff i = 0

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : p.natDegree < i
⊢ p.coeff i = 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ MvPolynomial.eval₂ f g (homogenize 0 n) = eval₂ f (g 0) 0

pp: case C_mul_pow
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (n_1 : ℕ) (r : R),
    r ≠ 0 → n_1 ≤ n → MvPolynomial.eval₂ f g ((C r * X ^ n_1).homogenize n) = eval₂ f (g 0) (C r * X ^ n_1)

pp: case add
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)

pp: case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ MvPolynomial.eval₂ f g (homogenize 0 n) = eval₂ f (g 0) 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case C_mul_pow
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (n_1 : ℕ) (r : R),
    r ≠ 0 → n_1 ≤ n → MvPolynomial.eval₂ f g ((C r * X ^ n_1).homogenize n) = eval₂ f (g 0) (C r * X ^ n_1)

pp: case add
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)

pp: case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n

Tactic:
·

Goal state after:
case C_mul_pow
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (n_1 : ℕ) (r : R),
    r ≠ 0 → n_1 ≤ n → MvPolynomial.eval₂ f g ((C r * X ^ n_1).homogenize n) = eval₂ f (g 0) (C r * X ^ n_1)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case add
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)

pp: case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n

Tactic:
·

Goal state after:
case add
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n

Tactic:
·

Goal state after:
case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : R a b
⊢ a :: destutter' R b l <+ a :: b :: l

pp: case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l

Tactic:
·

Goal state after:
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : R a b
⊢ a :: destutter' R b l <+ a :: b :: l
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l

Tactic:
·

Goal state after:
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
hpq : (MvPolynomial.aeval ![X, 1]) q = p
⊢ p.homogenize n = q

Tactic:
subst p

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
⊢ ((MvPolynomial.aeval ![X, 1]) q).homogenize n = q
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case hq
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (p.homogenize m * q.homogenize n).IsHomogeneous (m + n)

pp: case hpq
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1]) (p.homogenize m * q.homogenize n) = p * q

Tactic:
·

Goal state after:
case hq
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (p.homogenize m * q.homogenize n).IsHomogeneous (m + n)
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case hpq
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1]) (p.homogenize m * q.homogenize n) = p * q

Tactic:
·

Goal state after:
case hpq
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1]) (p.homogenize m * q.homogenize n) = p * q
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : R a b
⊢ a ∈ a :: destutter' R b l

pp: case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : ¬R a b
⊢ a ∈ destutter' R a l

Tactic:
·

Goal state after:
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : R a b
⊢ a ∈ a :: destutter' R b l
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : ¬R a b
⊢ a ∈ destutter' R a l

Tactic:
·

Goal state after:
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : ¬R a b
⊢ a ∈ destutter' R a l
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R[X]
⊢ homogenize 0 (natDegree 0) ∣ (0 * r).homogenize (0 * r).natDegree

pp: case inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
⊢ p.homogenize p.natDegree ∣ (p * 0).homogenize (p * 0).natDegree

pp: case inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R[X]
⊢ homogenize 0 (natDegree 0) ∣ (0 * r).homogenize (0 * r).natDegree
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
⊢ p.homogenize p.natDegree ∣ (p * 0).homogenize (p * 0).natDegree

pp: case inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
⊢ p.homogenize p.natDegree ∣ (p * 0).homogenize (p * 0).natDegree
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree

Tactic:
·

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
i : Fin (n + 1)
⊢ (Fin.snoc r (q %ₘ g) i).degree < g.degree

pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i = q /ₘ g * g ^ (n + 1) + ∑ i, Fin.snoc r (q %ₘ g) i * g ^ ↑i

Tactic:
·

Goal state after:
case succ.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
i : Fin (n + 1)
⊢ (Fin.snoc r (q %ₘ g) i).degree < g.degree
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i = q /ₘ g * g ^ (n + 1) + ∑ i, Fin.snoc r (q %ₘ g) i * g ^ ↑i

Tactic:
·

Goal state after:
case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i = q /ₘ g * g ^ (n + 1) + ∑ i, Fin.snoc r (q %ₘ g) i * g ^ ↑i
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n

pp: case ha
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 1 ≠ 0

pp: case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ k ≤ n

pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 1 ^ 0 = 1

pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ x 0 ^ 0 = 1

pp: case h_zero
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2), x a ^ 0 = 1

pp: case h_add
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ ∀ (a : Fin 2) (b₁ b₂ : ℕ), x a ^ (b₁ + b₂) = x a ^ b₁ * x a ^ b₂

pp: case h
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ (fun₀ | 0 => k) 1 = 0

Tactic:
·

Goal state after:
K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
k : ℕ
hk : k ∈ range n.succ
⊢ p.coeff k * (x 0 ^ k * (x 1 ^ n * (x 1 ^ k)⁻¹)) = p.coeff k * (x 0 / x 1) ^ k * x 1 ^ n
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

pp: case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
·

Goal state after:
case neg.inl
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : R a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous p.natDegree

pp: case «1»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous p.natDegree

Tactic:
·

Goal state after:
case «0»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous p.natDegree
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous p.natDegree

Tactic:
·

Goal state after:
case «1»
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (p.toTupleMvPolynomial ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous p.natDegree
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
·

Goal state after:
case neg.inr
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
hab : ¬R a b
hac : Rᶜ a c
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

pp: case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : ¬R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
·

Goal state after:
case pos
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : ¬R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
·

Goal state after:
case neg
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
hab : ¬R a b
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ s 0 ∈ p.support

pp: case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
n : ℕ
hn : n ∈ p.support
⊢ (fun₀ | 0 => n | 1 => p.natDegree - n) ∈ (p.homogenize p.natDegree).support

pp: case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ (fun₀ | 0 => s 0 | 1 => p.natDegree - s 0) = s

pp: case refine_4
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ f (MvPolynomial.coeff s (p.homogenize p.natDegree)) = f (p.coeff (s 0))

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ s 0 ∈ p.support
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
n : ℕ
hn : n ∈ p.support
⊢ (fun₀ | 0 => n | 1 => p.natDegree - n) ∈ (p.homogenize p.natDegree).support

pp: case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ (fun₀ | 0 => s 0 | 1 => p.natDegree - s 0) = s

pp: case refine_4
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ f (MvPolynomial.coeff s (p.homogenize p.natDegree)) = f (p.coeff (s 0))

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
n : ℕ
hn : n ∈ p.support
⊢ (fun₀ | 0 => n | 1 => p.natDegree - n) ∈ (p.homogenize p.natDegree).support
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ (fun₀ | 0 => s 0 | 1 => p.natDegree - s 0) = s

pp: case refine_4
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ f (MvPolynomial.coeff s (p.homogenize p.natDegree)) = f (p.coeff (s 0))

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ (fun₀ | 0 => s 0 | 1 => p.natDegree - s 0) = s
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case refine_4
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ f (MvPolynomial.coeff s (p.homogenize p.natDegree)) = f (p.coeff (s 0))

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ f (MvPolynomial.coeff s (p.homogenize p.natDegree)) = f (p.coeff (s 0))