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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) a ∈ Finset.range (p.natDegree + 1)

pp: case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a₁ ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a₁ ≠ 0 →
      ∀ a₂ ∈ Finset.range (p.natDegree + 1),
        p.mirror.coeff a₂ ≠ 0 →
          (revAt (p.natDegree + p.natTrailingDegree)) a₁ = (revAt (p.natDegree + p.natTrailingDegree)) a₂ → a₁ = a₂

pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

pp: case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → (revAt (p.natDegree + p.natTrailingDegree)) a ∈ Finset.range (p.natDegree + 1)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a₁ ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a₁ ≠ 0 →
      ∀ a₂ ∈ Finset.range (p.natDegree + 1),
        p.mirror.coeff a₂ ≠ 0 →
          (revAt (p.natDegree + p.natTrailingDegree)) a₁ = (revAt (p.natDegree + p.natTrailingDegree)) a₂ → a₁ = a₂

pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

pp: case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)

Tactic:
·

Goal state after:
case refine_3
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a₁ ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a₁ ≠ 0 →
      ∀ a₂ ∈ Finset.range (p.natDegree + 1),
        p.mirror.coeff a₂ ≠ 0 →
          (revAt (p.natDegree + p.natTrailingDegree)) a₁ = (revAt (p.natDegree + p.natTrailingDegree)) a₂ → a₁ = a₂
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b

pp: case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)

Tactic:
·

Goal state after:
case refine_4
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ b ∈ Finset.range (p.natDegree + 1),
    p.coeff b ≠ 0 →
      ∃ a,
        ∃ (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
          (revAt (p.natDegree + p.natTrailingDegree)) a = b
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)

pp: case h.refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0

Tactic:
·

Goal state after:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ∈ Finset.range (p.natDegree + 1)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0

Tactic:
·

Goal state after:
case h.refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)

Tactic:
·

Goal state after:
case refine_5
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ a ∈ Finset.range (p.natDegree + 1),
    p.mirror.coeff a ≠ 0 → p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) a)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ k ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ,
      p.coeff (k, p.natDegree + p.natTrailingDegree - k).1 *
        p.mirror.coeff (k, p.natDegree + p.natTrailingDegree - k).2 =
    p.sum fun x x_1 ↦ x_1 ^ 2

Tactic:
refine
    (Finset.sum_congr rfl fun n hn => ?_).trans
      (p.sum_eq_of_subset (fun _ ↦ (· ^ 2)) (fun _ ↦ zero_pow two_ne_zero) fun n hn ↦
          Finset.mem_range_succ_iff.mpr
            ((le_natDegree_of_mem_supp n hn).trans (Nat.le_add_right _ _))).symm

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ
⊢ p.coeff (n, p.natDegree + p.natTrailingDegree - n).1 * p.mirror.coeff (n, p.natDegree + p.natTrailingDegree - n).2 =
    p.coeff n ^ 2
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * q).mirror = p.mirror * q.mirror

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * q).mirror = p.mirror * q.mirror
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * q).mirror = p.mirror * q.mirror

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * q).mirror = p.mirror * q.mirror
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x y : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x + y)).toFinsupp }.coeff i =
    ({ toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn x).toFinsupp } +
          { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn y).toFinsupp }).coeff
      i
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case not_isUnit
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
⊢ ¬IsUnit f

pp: case isUnit_or_isUnit
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
⊢ ∀ ⦃a b : R[X]⦄, f = a * b → IsUnit a ∨ IsUnit b

Tactic:
·

Goal state after:
case not_isUnit
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
⊢ ¬IsUnit f
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case isUnit_or_isUnit
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
⊢ ∀ ⦃a b : R[X]⦄, f = a * b → IsUnit a ∨ IsUnit b

Tactic:
·

Goal state after:
case isUnit_or_isUnit
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
⊢ ∀ ⦃a b : R[X]⦄, f = a * b → IsUnit a ∨ IsUnit b
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
x : R
p : Fin n → R
i : ℕ
h : ¬i < n
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn (x • p)).toFinsupp }.coeff i =
    ((RingHom.id R) x • { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn p).toFinsupp }).coeff i
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : (ofFn n) v = 0
⊢ ((ofFn n) v).degree < ↑n

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬(ofFn n) v = 0
⊢ ((ofFn n) v).degree < ↑n

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : (ofFn n) v = 0
⊢ ((ofFn n) v).degree < ↑n
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬(ofFn n) v = 0
⊢ ((ofFn n) v).degree < ↑n

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬(ofFn n) v = 0
⊢ ((ofFn n) v).degree < ↑n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case isUnit_or_isUnit.inl
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
⊢ IsUnit g ∨ IsUnit h

pp: case isUnit_or_isUnit.inr.inl
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
⊢ IsUnit g ∨ IsUnit h

pp: case isUnit_or_isUnit.inr.inr.inl
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

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.inl
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
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : n = 0
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
⊢ (ofFn n) v = ∑ i, (monomial ↑i) (v i)
Module: Mathlib.Algebra.Polynomial.Homogenize

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

Tactic:
Finset.sum_eq_single (a := (m, n - m))

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

case h₀
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ∀ b ∈ antidiagonal n,
    b ≠ (m, n - m) → (MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2) (((monomial m) r).coeff b.1) = 0

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.Mirror

Goal state before:
pp: case isUnit_or_isUnit.inr.inl
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
⊢ IsUnit g ∨ IsUnit h

pp: case isUnit_or_isUnit.inr.inr.inl
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

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.inl
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
⊢ IsUnit g ∨ IsUnit h
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case isUnit_or_isUnit.inr.inr.inl
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

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.inl
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: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) =
    (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r

pp: case h₀
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ∀ b ∈ antidiagonal n,
    b ≠ (m, n - m) → (MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2) (((monomial m) r).coeff b.1) = 0

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:
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) =
    (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : i < n
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : i < n
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ p.natDegree < i

Tactic:
by lia

Goal state after:
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
⊢ ∀ b ∈ antidiagonal n,
    b ≠ (m, n - m) → (MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2) (((monomial m) r).coeff b.1) = 0

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
⊢ ∀ b ∈ antidiagonal n,
    b ≠ (m, n - m) → (MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2) (((monomial m) r).coeff b.1) = 0