awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : a = 0
pos : Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) 0)) ((monomial n : (a : R) → R[X]) 0)
pos₁ : Eq.{u_1 + 1} (α := R[X]) (mirror 0) 0
pos₂ pos₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)

Tactic:
rw [ha, monomial_zero_right, mirror_zero]

Premises used: Polynomial.mirror_zero, Polynomial.monomial_zero_right
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
ha : ¬a = 0
neg :
  reverse ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₁ :
  reflect (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₂ :
  reflect (if a = 0 then 0 else n) ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₃ :
  reflect n ((monomial n : (a : R) → R[X]) a) *
      HPow.hPow (α := R[X]) X (natTrailingDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) a)) =
    (monomial n : (a : R) → R[X]) a
neg₄ : reflect n ((monomial n : (a : R) → R[X]) a) * HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
neg₅ :
  reflect n (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₆ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt n : (a : ℕ) → ℕ) n : ℕ)) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₇ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n - n)) * HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₈ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0) *
      HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₉ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (1 : R[X]) * HPow.hPow (α := R[X]) X n =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
neg₁₀ neg₁₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)

Tactic:
rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]

Premises used: le_refl, tsub_self, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.natTrailingDegree_monomial, Polynomial.mirror, Polynomial.revAt_le, pow_zero, Polynomial.natDegree_monomial, Polynomial.reflect_C_mul_X_pow, mul_one, if_neg, Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
pos :
  ∀ (ha : a = 0), Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
neg neg₁ :
  ∀ (ha : ¬a = 0), Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((monomial n : (a : R) → R[X]) a)) ((monomial n : (a : R) → R[X]) a)

Tactic:
classical
    by_cases ha : a = 0
    · rw [ha, monomial_zero_right, mirror_zero]
    · rw [mirror, reverse, natDegree_monomial n a, if_neg ha, natTrailingDegree_monomial ha, ←
        C_mul_X_pow_eq_monomial, reflect_C_mul_X_pow, revAt_le (le_refl n), tsub_self, pow_zero,
        mul_one]

Premises used: le_refl, tsub_self, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.mirror, Polynomial.revAt_le, pow_zero, Polynomial.mirror_zero, Polynomial.reflect_C_mul_X_pow, Polynomial.monomial_zero_right, mul_one, Polynomial.reverse
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror ((C : (a : R) → R[X]) a)) ((C : (a : R) → R[X]) a)

Tactic:
mirror_monomial 0 a

Premises used: Polynomial.mirror_monomial, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) (mirror X) X

Tactic:
mirror_monomial 1 (1 : R)

Premises used: Polynomial.mirror_monomial, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
pos : ∀ (hp : p = 0), p.mirror.natDegree = p.natDegree
neg : ∀ (hp : ¬p = 0), p.mirror.natDegree = p.natDegree
⊢ p.mirror.natDegree = p.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p = 0
pos : natDegree.{u_1} (R := R) (mirror 0) = natDegree.{u_1} (R := R) 0
pos₁ pos₂ : natDegree.{u_1} (R := R) 0 = natDegree.{u_1} (R := R) 0
⊢ p.mirror.natDegree = p.natDegree

Tactic:
rw [hp, mirror_zero]

Premises used: Polynomial.mirror_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
h : Nontrivial R
rw : p.reverse.leadingCoeff * (HPow.hPow (α := R[X]) X p.natTrailingDegree).leadingCoeff ≠ 0
⊢ p.mirror.natDegree = p.natDegree

Tactic:
rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow,
    tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]

Premises used: Polynomial.mirror, tsub_add_cancel_of_le, Polynomial.natDegree_mul', Polynomial.natDegree_X_pow, Polynomial.natTrailingDegree_le_natDegree, Polynomial.reverse_natDegree
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
h : Nontrivial R
rwa : p.reverse.leadingCoeff * 1 ≠ 0
rwa₁ : p.reverse.leadingCoeff ≠ 0
rwa₂ : p.trailingCoeff ≠ 0
rwa₃ : ¬p.trailingCoeff = 0
rwa₄ rwa₅ rwa₆ rwa₇ : ¬p = 0
⊢ p.reverse.leadingCoeff * (HPow.hPow (α := R[X]) X p.natTrailingDegree).leadingCoeff ≠ 0

Tactic:
rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]

Premises used: Ne, Polynomial.leadingCoeff_X_pow, Polynomial.reverse_leadingCoeff, mul_one, Polynomial.trailingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
pos : ∀ (hp : p = 0), p.mirror.natTrailingDegree = p.natTrailingDegree
neg : ∀ (hp : ¬p = 0), p.mirror.natTrailingDegree = p.natTrailingDegree
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : p = 0
pos : natTrailingDegree.{u_1} (R := R) (mirror 0) = natTrailingDegree.{u_1} (R := R) 0
pos₁ pos₂ : natTrailingDegree.{u_1} (R := R) 0 = natTrailingDegree.{u_1} (R := R) 0
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

Tactic:
rw [hp, mirror_zero]

Premises used: Polynomial.mirror_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
hp : ¬p = 0
neg : (p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree).natTrailingDegree = p.natTrailingDegree
neg₁ : p.reverse.natTrailingDegree + p.natTrailingDegree = p.natTrailingDegree
neg₂ : 0 + p.natTrailingDegree = p.natTrailingDegree
neg₃ neg₄ : p.natTrailingDegree = p.natTrailingDegree
⊢ p.mirror.natTrailingDegree = p.natTrailingDegree

Tactic:
rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp),
      natTrailingDegree_reverse, zero_add]

Premises used: Polynomial.reverse_eq_zero, Polynomial.natTrailingDegree_mul_X_pow, Polynomial.mirror, mt, zero_add, Iff.mp, Polynomial.natTrailingDegree_reverse
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
pos : ∀ (h2 : p.natDegree < n), p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
neg :
  ∀ (h2 : ¬p.natDegree < n), p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)

Tactic:
by_cases h2 : p.natDegree < n

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 rwa rwa₁ rwa₂ rwa₃ : p.natDegree < n
⊢ p.mirror.natDegree < n

Tactic:
rwa [mirror_natDegree]

Premises used: Polynomial.mirror_natDegree
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
pos : 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt (by rwa [mirror_natDegree])]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
pos :
  ∀ (h1 : n ≤ p.natDegree + p.natTrailingDegree),
    0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
neg :
  ∀ (h1 : ¬n ≤ p.natDegree + p.natTrailingDegree),
    0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)

Tactic:
by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree

Premises used: Polynomial.natDegree, Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : n ≤ p.natDegree + p.natTrailingDegree
pos : p.natDegree + p.natTrailingDegree - n < p.natTrailingDegree
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)

Tactic:
rw [revAt_le h1, coeff_eq_zero_of_lt_natTrailingDegree]

Premises used: Polynomial.coeff_eq_zero_of_lt_natTrailingDegree, Polynomial.revAt_le
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : n ≤ p.natDegree + p.natTrailingDegree
⊢ p.natDegree + p.natTrailingDegree - n < p.natTrailingDegree

Tactic:
(tsub_lt_iff_left h1).mpr (Nat.add_lt_add_right h2 _)

Premises used: Iff.mpr, tsub_lt_iff_left, Nat.add_lt_add_right
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : n ≤ p.natDegree + p.natTrailingDegree
⊢ p.natDegree + p.natTrailingDegree - n < p.natTrailingDegree

Tactic:
exact (tsub_lt_iff_left h1).mpr (Nat.add_lt_add_right h2 _)

Premises used: Iff.mpr, tsub_lt_iff_left, Nat.add_lt_add_right
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : ¬n ≤ p.natDegree + p.natTrailingDegree
neg : 0 = p.coeff (revAtFun (p.natDegree + p.natTrailingDegree) n)
neg₁ : 0 = p.coeff (if n ≤ p.natDegree + p.natTrailingDegree then p.natDegree + p.natTrailingDegree - n else n)
neg₂ : 0 = p.coeff n
neg₃ neg₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)

Tactic:
rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, Polynomial.revAtFun_eq, Polynomial.revAtFun, if_neg
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : ¬p.natDegree < n
⊢ n ≤ p.natDegree

Tactic:
rw [not_lt] at h2

Premises used: not_lt
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
neg : p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)

Tactic:
rw [revAt_le (h2.trans (Nat.le_add_right _ _))]

Premises used: Nat.le_add_right, Polynomial.revAt_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
pos : ∀ (h3 : p.natTrailingDegree ≤ n), p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
neg : ∀ (h3 : ¬p.natTrailingDegree ≤ n), p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)

Tactic:
by_cases h3 : p.natTrailingDegree ≤ n

Premises used: Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : p.natTrailingDegree ≤ n
pos : p.mirror.coeff n = p.coeff (p.natDegree - n + p.natTrailingDegree)
pos₁ : p.mirror.coeff n = p.coeff (p.natDegree - (n - p.natTrailingDegree))
pos₂ :
  (p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree).coeff n = p.coeff (p.natDegree - (n - p.natTrailingDegree))
pos₃ :
  (if p.natTrailingDegree ≤ n then p.reverse.coeff (n - p.natTrailingDegree) else 0) =
    p.coeff (p.natDegree - (n - p.natTrailingDegree))
pos₄ : p.reverse.coeff (n - p.natTrailingDegree) = p.coeff (p.natDegree - (n - p.natTrailingDegree))
pos₅ :
  p.coeff ((revAt p.natDegree : (a : ℕ) → ℕ) (n - p.natTrailingDegree)) =
    p.coeff (p.natDegree - (n - p.natTrailingDegree))
pos₆ pos₇ : p.coeff (p.natDegree - (n - p.natTrailingDegree)) = p.coeff (p.natDegree - (n - p.natTrailingDegree))
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)

Tactic:
rw [← tsub_add_eq_add_tsub h2, ← tsub_tsub_assoc h2 h3, mirror, coeff_mul_X_pow', if_pos h3,
      coeff_reverse, revAt_le (tsub_le_self.trans h2)]

Premises used: Polynomial.mirror, if_pos, Polynomial.revAt_le, tsub_le_self, tsub_add_eq_add_tsub, tsub_tsub_assoc, LE.le.trans, Polynomial.coeff_mul_X_pow', Polynomial.coeff_reverse
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : ¬p.natTrailingDegree ≤ n
⊢ n < p.natTrailingDegree

Tactic:
rw [not_le] at h3

Premises used: not_le
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
neg : p.mirror.coeff n = 0
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt (lt_tsub_iff_right.mpr (Nat.add_lt_add_left h3 _))]

Premises used: Iff.mpr, lt_tsub_iff_right, Nat.add_lt_add_left, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
rwa rwa₁ rwa₂ rwa₃ : n < p.natTrailingDegree
⊢ n < p.mirror.natTrailingDegree

Tactic:
rwa [mirror_natTrailingDegree]

Premises used: Polynomial.mirror_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ p.mirror.coeff n = 0

Tactic:
exact coeff_eq_zero_of_lt_natTrailingDegree (by rwa [mirror_natTrailingDegree])

Premises used: Polynomial.coeff_eq_zero_of_lt_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
simp_rw :
  Eq.{u_1 + 1} (α := R) (∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x)
    (∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x)
⊢ eval 1 p.mirror = eval 1 p

Tactic:
simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_natDegree]

Premises used: one_pow, Polynomial.mirror_natDegree, Polynomial.eval_eq_sum_range, mul_one
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x)
    (∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x)

Tactic:
Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_

Premises used: Finset.sum_bij_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
refine_1 : (a : ℕ) → a ∈ Finset.range (p.natDegree + 1) → p.mirror.coeff a ≠ 0 → ℕ
refine_2 :
  ∀ (a : ℕ) (h₁ : a ∈ Finset.range (p.natDegree + 1)) (h₂ : p.mirror.coeff a ≠ 0),
    Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a : ℕ)
refine_3 :
  ∀ (a₁ : ℕ) (h₁₁ : a₁ ∈ Finset.range (p.natDegree + 1)) (h₁₂ : p.mirror.coeff a₁ ≠ 0) (a₂ : ℕ)
    (h₂₁ : a₂ ∈ Finset.range (p.natDegree + 1)) (h₂₂ : p.mirror.coeff a₂ ≠ 0),
    Eq (α := ℕ) ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a₁ : ℕ)
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a₂ : ℕ) →
      a₁ = a₂
refine_4 :
  ∀ 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 : ℕ) → ℕ) a = b
refine_5 :
  ∀ (a : ℕ) (h₁ : a ∈ Finset.range (p.natDegree + 1)) (h₂ : p.mirror.coeff a ≠ 0),
    p.mirror.coeff a = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a)
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x)
    (∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x)

Tactic:
refine Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_

Premises used: Finset.sum_bij_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ (a : ℕ) → a ∈ Finset.range (p.natDegree + 1) → p.mirror.coeff a ≠ 0 → ℕ

Tactic:
exact fun n _ _ => revAt (p.natDegree + p.natTrailingDegree) n

Premises used: Polynomial.revAt, HAdd.hAdd, Polynomial.natDegree, Polynomial.natTrailingDegree, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.mirror.coeff n ≠ 0
refine_2 :
  ∀ (hn : n ≤ p.natDegree) (hp : p.mirror.coeff n ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n ≤ p.natDegree
⊢ Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)

Tactic:
rw [Finset.mem_range_succ_iff] at *

Premises used: Finset.mem_range_succ_iff
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
refine_2 : p.natDegree + p.natTrailingDegree - n ≤ p.natDegree
⊢ (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n ≤ p.natDegree

Tactic:
rw [revAt_le (hn.trans (Nat.le_add_right _ _))]

Premises used: Nat.le_add_right, Polynomial.revAt_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
refine_2 : p.mirror.natTrailingDegree ≤ n
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]

Premises used: add_comm, Polynomial.mirror_natTrailingDegree, add_tsub_cancel_right, tsub_le_iff_tsub_le
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.mirror.natTrailingDegree ≤ n

Tactic:
natTrailingDegree_le_of_ne_zero hp

Premises used: Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.mirror.natTrailingDegree ≤ n

Tactic:
exact natTrailingDegree_le_of_ne_zero hp

Premises used: Polynomial.natTrailingDegree_le_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n₁ : ℕ
h_1 : n₁ ∈ Finset.range (p.natDegree + 1)
h_2 : p.mirror.coeff n₁ ≠ 0
x : ℕ
h_3 : x ∈ Finset.range (p.natDegree + 1)
h_4 : p.mirror.coeff x ≠ 0
h :
  Eq (α := ℕ) ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n₁ : ℕ)
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) x : ℕ)
rw :
  (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n₁ : ℕ) =
    x
rw₁ : ℕ
rw₂ :
  (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) x : ℕ) =
    x
rw₃ rw₄ : x = x
⊢ n₁ = x

Tactic:
rw [← @revAt_invol _ n₁, h, revAt_invol]

Premises used: Polynomial.revAt_invol
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ ∀ (a₁ : ℕ) (h₁₁ : a₁ ∈ Finset.range (p.natDegree + 1)) (h₁₂ : p.mirror.coeff a₁ ≠ 0) (a₂ : ℕ)
    (h₂₁ : a₂ ∈ Finset.range (p.natDegree + 1)) (h₂₂ : p.mirror.coeff a₂ ≠ 0),
    Eq (α := ℕ) ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a₁ : ℕ)
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a₂ : ℕ) →
      a₁ = a₂

Tactic:
exact fun n₁ _ _ _ _ _ h => by rw [← @revAt_invol _ n₁, h, revAt_invol]
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
h :
  ∃ (_ :
    Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ))
    (_ : p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ) =
      n
⊢ ∃ (a : ℕ) (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a = n

Tactic:
use revAt (p.natDegree + p.natTrailingDegree) n

Premises used: Polynomial.revAt, HAdd.hAdd, Polynomial.natDegree, Polynomial.natTrailingDegree, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ (_ :
    Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ))
    (_ : p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ) =
      n

Tactic:
⟨?_, ?_, revAt_invol⟩

Premises used: Exists.intro, Polynomial.revAt_invol
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
h :
  Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)
h₁ : p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) ≠ 0
⊢ ∃ (_ :
    Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ))
    (_ : p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
        ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ) =
      n

Tactic:
refine ⟨?_, ?_, revAt_invol⟩
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
h :
  ∀ (hn : n ≤ p.natDegree) (hp : p.coeff n ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n ≤ p.natDegree
⊢ Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)

Tactic:
rw [Finset.mem_range_succ_iff] at *

Premises used: Finset.mem_range_succ_iff