awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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)
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have neg : ∀ (h1 : ¬n ≤ p.natDegree + p.natTrailingDegree),
  0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
Tactic: by_cases h1 : n ≤ p.natDegree + p.natTrailingDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : n ≤ p.natDegree + p.natTrailingDegree
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have pos : p.natDegree + p.natTrailingDegree - n < p.natTrailingDegree
Tactic: rw [revAt_le h1, coeff_eq_zero_of_lt_natTrailingDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : ¬n ≤ p.natDegree + p.natTrailingDegree
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have neg : 0 = p.coeff (revAtFun (p.natDegree + p.natTrailingDegree) n)
Tactic: rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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)
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have neg₁ : 0 = p.coeff (if n ≤ p.natDegree + p.natTrailingDegree then p.natDegree + p.natTrailingDegree - n else n)
Tactic: rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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)
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have neg₂ : 0 = p.coeff n
Tactic: rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have neg₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← revAtFun_eq, revAtFun, if_neg h1, coeff_eq_zero_of_natDegree_lt h2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : ¬p.natDegree < n
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have h2₁ : n ≤ p.natDegree
Tactic: rw [not_lt] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n)
have neg : p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
Tactic: rw [revAt_le (h2.trans (Nat.le_add_right _ _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have pos : ∀ (h3 : p.natTrailingDegree ≤ n), p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
Tactic: by_cases h3 : p.natTrailingDegree ≤ n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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)
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have neg : ∀ (h3 : ¬p.natTrailingDegree ≤ n), p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
Tactic: by_cases h3 : p.natTrailingDegree ≤ n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : p.natTrailingDegree ≤ n
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have pos : p.mirror.coeff n = p.coeff (p.natDegree - n + p.natTrailingDegree)
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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)
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have pos₁ : p.mirror.coeff n = p.coeff (p.natDegree - (n - p.natTrailingDegree))
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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))
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have pos₂ : (p.reverse * HPow.hPow (α := R[X]) X p.natTrailingDegree).coeff n = p.coeff (p.natDegree - (n - p.natTrailingDegree))
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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))
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have pos₃ : (if p.natTrailingDegree ≤ n then p.reverse.coeff (n - p.natTrailingDegree) else 0) =
  p.coeff (p.natDegree - (n - p.natTrailingDegree))
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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))
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have pos₄ : p.reverse.coeff (n - p.natTrailingDegree) = p.coeff (p.natDegree - (n - p.natTrailingDegree))
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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))
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have pos₅ : p.coeff ((revAt p.natDegree : (a : ℕ) → ℕ) (n - p.natTrailingDegree)) =
  p.coeff (p.natDegree - (n - p.natTrailingDegree))
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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))
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have pos₆ : p.coeff (p.natDegree - (n - p.natTrailingDegree)) = p.coeff (p.natDegree - (n - p.natTrailingDegree))
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : ¬p.natTrailingDegree ≤ n
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have h3₁ : n < p.natTrailingDegree
Tactic: rw [not_le] at h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
have neg : p.mirror.coeff n = 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt (lt_tsub_iff_right.mpr (Nat.add_lt_add_left h3 _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ eval 1 p.mirror = eval 1 p
have 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)
Tactic: simp_rw [eval_eq_sum_range, one_pow, mul_one, mirror_natDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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)
have refine_1 : (a : ℕ) → a ∈ Finset.range (p.natDegree + 1) → p.mirror.coeff a ≠ 0 → ℕ
Tactic: refine Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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 → ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x)
    (∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x)
have 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 : ℕ)
Tactic: refine Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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 : ℕ)
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x)
    (∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x)
have 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₂
Tactic: refine Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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₂
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x)
    (∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x)
have 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
Tactic: refine Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ Finset.range (p.natDegree + 1), p.mirror.coeff x)
    (∑ x ∈ Finset.range (p.natDegree + 1), p.coeff x)
have 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)
Tactic: refine Finset.sum_bij_ne_zero ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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
⊢ Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)
have refine_2 : ∀ (hn : n ≤ p.natDegree) (hp : p.mirror.coeff n ≠ 0),
  (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n ≤ p.natDegree
Tactic: rw [Finset.mem_range_succ_iff] at *
Cleared hypotheses: hn, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n ≤ p.natDegree
have refine_2 : p.natDegree + p.natTrailingDegree - n ≤ p.natDegree
Tactic: rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree
have refine_2 : p.mirror.natTrailingDegree ≤ n
Tactic: rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right, ← mirror_natTrailingDegree]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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 : ℕ)
⊢ n₁ = x
have rw : (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n₁ : ℕ) =
  x
Tactic: rw [← @revAt_invol _ n₁, h, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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₁ : ℕ
⊢ n₁ = x
have rw₂ : (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) x : ℕ) =
  x
Tactic: rw [← @revAt_invol _ n₁, h, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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
⊢ n₁ = x
have rw₃ : x = x
Tactic: rw [← @revAt_invol _ n₁, h, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ ∃ (a : ℕ) (_ : a ∈ Finset.range (p.natDegree + 1)) (_ : p.mirror.coeff a ≠ 0),
    (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) a = n
have 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
Tactic: use revAt (p.natDegree + p.natTrailingDegree) n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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
have h : Membership.mem (α := ℕ) (Finset.range (p.natDegree + 1))
  ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)
Tactic: refine ⟨?_, ?_, revAt_invol⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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 : ℕ)
⊢ ∃ (_ :
    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
have h₁ : p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n) ≠ 0
Tactic: refine ⟨?_, ?_, revAt_invol⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
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 : ℕ)
have h : ∀ (hn : n ≤ p.natDegree) (hp : p.coeff n ≠ 0), (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n ≤ p.natDegree
Tactic: rw [Finset.mem_range_succ_iff] at *
Cleared hypotheses: hn, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n ≤ p.natDegree
have h : p.natDegree + p.natTrailingDegree - n ≤ p.natDegree
Tactic: rw [revAt_le (hn.trans (Nat.le_add_right _ _))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree
have h : p.natTrailingDegree ≤ n
Tactic: rw [tsub_le_iff_tsub_le, add_comm, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
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) : (a : ℕ) → ℕ) n) ≠ 0
have h : p.coeff
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
      ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) ≠
  0
Tactic: rwa [coeff_mirror, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
⊢ p.mirror.mirror.coeff n = p.coeff n
have rw : p.mirror.coeff ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n) = p.coeff n
Tactic: rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Mirror (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
rw : p.mirror.coeff ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n) = p.coeff n
⊢ p.mirror.mirror.coeff n = p.coeff n
have rw₁ : p.coeff
    ((revAt (p.natDegree + p.natTrailingDegree) : (a : ℕ) → ℕ)
      ((revAt (p.mirror.natDegree + p.mirror.natTrailingDegree) : (a : ℕ) → ℕ) n : ℕ)) =
  p.coeff n
Tactic: rw [coeff_mirror, coeff_mirror, mirror_natDegree, mirror_natTrailingDegree, revAt_invol]