awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime_1 : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf :
  (↑q₁ : K) + HDiv.hDiv (α := K) (↑r₁₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₁ : K) (↑g₂ : K) =
    (↑q₂ : K) + HDiv.hDiv (α := K) (↑r₁₂ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₂ : K) (↑g₂ : K)
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
r₁ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₂ r₁₂ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
hcoprime : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
hr₁ : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₁ i).degree < (g i).degree
⊢ ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₂ i).degree < (g i).degree

Tactic:
have hr₂ (i : Bool) (_ : i ∈ Finset.univ) : (r₂ i).degree < (g i).degree := Bool.rec hr₂₂ hr₁₂ i
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime_1 : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf :
  (↑q₁ : K) + HDiv.hDiv (α := K) (↑r₁₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₁ : K) (↑g₂ : K) =
    (↑q₂ : K) + HDiv.hDiv (α := K) (↑r₁₂ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₂ : K) (↑g₂ : K)
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
r₁ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₂ r₁₂ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
hcoprime : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
hr₁ : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₁ i).degree < (g i).degree
hr₂ : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₂ i).degree < (g i).degree
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Tactic:
(quo_add_sum_rem_div_unique K hg hcoprime hr₁ hr₂ ?_).imp_right fun h =>
    ⟨h true (Finset.mem_univ true), h false (Finset.mem_univ false)⟩

Premises used: Polynomial.quo_add_sum_rem_div_unique, And.intro, And.imp_right
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime_1 : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf :
  (↑q₁ : K) + HDiv.hDiv (α := K) (↑r₁₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₁ : K) (↑g₂ : K) =
    (↑q₂ : K) + HDiv.hDiv (α := K) (↑r₁₂ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₂ : K) (↑g₂ : K)
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
r₁ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₂ r₁₂ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
hcoprime : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
hr₁ : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₁ i).degree < (g i).degree
hr₂ : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₂ i).degree < (g i).degree
refine :
  HAdd.hAdd (α := K) (↑q₁ : K) (∑ i : Bool, HDiv.hDiv (α := K) (↑(r₁ i) : K) (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q₂ : K) (∑ i : Bool, HDiv.hDiv (α := K) (↑(r₂ i) : K) (↑(g i) : K))
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂

Tactic:
refine (quo_add_sum_rem_div_unique K hg hcoprime hr₁ hr₂ ?_).imp_right fun h =>
    ⟨h true (Finset.mem_univ true), h false (Finset.mem_univ false)⟩

Premises used: Polynomial.quo_add_sum_rem_div_unique, And.imp_right
-- Module: Mathlib.Algebra.Polynomial.PartialFractions
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra.{u_1, u_2} R[X] K
inst_3 : FaithfulSMul.{u_1, u_2} R[X] K
g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
hcoprime_1 : IsCoprime g₁ g₂
q₁ q₂ r₁₁ r₁₂ r₂₁ r₂₂ : R[X]
hr₁₁ : r₁₁.degree < g₁.degree
hr₁₂ : r₁₂.degree < g₁.degree
hr₂₁ : r₂₁.degree < g₂.degree
hr₂₂ : r₂₂.degree < g₂.degree
hf :
  (↑q₁ : K) + HDiv.hDiv (α := K) (↑r₁₁ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₁ : K) (↑g₂ : K) =
    (↑q₂ : K) + HDiv.hDiv (α := K) (↑r₁₂ : K) (↑g₁ : K) + HDiv.hDiv (α := K) (↑r₂₂ : K) (↑g₂ : K)
g : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) g₂ g₁ t
r₁ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₁ r₁₁ t
r₂ : Bool → R[X] := fun (t : Bool) ↦ Bool.rec (motive := fun (x : Bool) ↦ R[X]) r₂₂ r₁₂ t
hg : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (g i).Monic
hcoprime : (↑Finset.univ : Set Bool).Pairwise fun (i j : Bool) ↦ IsCoprime (g i) (g j)
hr₁ : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₁ i).degree < (g i).degree
hr₂ : ∀ (i : Bool), Membership.mem (γ := Finset Bool) Finset.univ i → (r₂ i).degree < (g i).degree
⊢ HAdd.hAdd (α := K) (↑q₁ : K) (∑ i : Bool, HDiv.hDiv (α := K) (↑(r₁ i) : K) (↑(g i) : K)) =
    HAdd.hAdd (α := K) (↑q₂ : K) (∑ i : Bool, HDiv.hDiv (α := K) (↑(r₂ i) : K) (↑(g i) : K))

Tactic:
simpa [g, r₁, r₂, add_assoc] using hf

Premises used: add_assoc
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
N i : ℕ
⊢ (if (if i ≤ N then N - i else i) ≤ N then N - if i ≤ N then N - i else i else if i ≤ N then N - i else i) = i

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
rw : revAtFun N (revAtFun N a) = b
rw₁ : revAtFun N (revAtFun N b) = b
rw₂ rw₃ : b = b
⊢ a = b

Tactic:
rw [← @revAtFun_invol N a, hab, revAtFun_invol]

Premises used: Polynomial.revAtFun_invol
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
N i : ℕ
⊢ revAtFun N i = (revAt N : (a : ℕ) → ℕ) i

Tactic:
rfl

Premises used: Polynomial.revAtFun, rfl, ite
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
N i : ℕ
⊢ (revAt N : (a : ℕ) → ℕ) ((revAt N : (a : ℕ) → ℕ) i : ℕ) = i

Tactic:
revAtFun_invol

Premises used: Polynomial.revAtFun_invol, Polynomial.revAtFun, ite
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
N i : ℕ
H : i ≤ N
⊢ (revAt N : (a : ℕ) → ℕ) i = N - i

Tactic:
if_pos H

Premises used: if_pos, ite
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
N i : ℕ
h : N < i
⊢ (revAt N : (a : ℕ) → ℕ) i = i

Tactic:
simp [revAt, Nat.not_le.mpr h]

Premises used: Iff.mpr, Polynomial.revAt, Nat.not_le
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
N O n o : ℕ
hn : n ≤ N
ho : o ≤ O
rcases :
  ∀ (n' : ℕ) (hn : n ≤ n + n'),
    (revAt (n + n' + O) : (a : ℕ) → ℕ) (n + o) =
      HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt (n + n') : (a : ℕ) → ℕ) n : ℕ) ((revAt O : (a : ℕ) → ℕ) o : ℕ)
⊢ (revAt (N + O) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt N : (a : ℕ) → ℕ) n : ℕ) ((revAt O : (a : ℕ) → ℕ) o : ℕ)

Tactic:
rcases Nat.le.dest hn with ⟨n', rfl⟩

Premises used: Nat.le.dest, rfl
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
O n o : ℕ
ho : o ≤ O
n' : ℕ
hn : n ≤ n + n'
rcases :
  ∀ (o' : ℕ) (ho : o ≤ o + o'),
    (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) =
      HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt (n + n') : (a : ℕ) → ℕ) n : ℕ) ((revAt (o + o') : (a : ℕ) → ℕ) o : ℕ)
⊢ (revAt (n + n' + O) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt (n + n') : (a : ℕ) → ℕ) n : ℕ) ((revAt O : (a : ℕ) → ℕ) o : ℕ)

Tactic:
rcases Nat.le.dest ho with ⟨o', rfl⟩

Premises used: Nat.le.dest, rfl
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
rw :
  (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (β := ℕ) (n + n' - n) ((revAt (o + o') : (a : ℕ) → ℕ) o : ℕ)
⊢ (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt (n + n') : (a : ℕ) → ℕ) n : ℕ) ((revAt (o + o') : (a : ℕ) → ℕ) o : ℕ)

Tactic:
rw [revAt_le (le_add_right rfl.le)]

Premises used: Eq.le, Polynomial.revAt_le, rfl, le_add_right
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
rw : (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) = n + n' - n + (o + o' - o)
⊢ (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (β := ℕ) (n + n' - n) ((revAt (o + o') : (a : ℕ) → ℕ) o : ℕ)

Tactic:
rw [revAt_le (le_add_right rfl.le)]

Premises used: Eq.le, Polynomial.revAt_le, rfl, le_add_right
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
repeat' : (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) = n + n' - n + (o + o' - o)
⊢ (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt (n + n') : (a : ℕ) → ℕ) n : ℕ) ((revAt (o + o') : (a : ℕ) → ℕ) o : ℕ)

Tactic:
repeat' rw [revAt_le (le_add_right rfl.le)]

Premises used: Eq.le, Polynomial.revAt_le, rfl, le_add_right
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
rw : n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
⊢ (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) = n + n' - n + (o + o' - o)

Tactic:
rw [add_assoc, add_left_comm n' o, ← add_assoc, revAt_le (le_add_right rfl.le)]

Premises used: add_left_comm, add_assoc, Eq.le, Polynomial.revAt_le, rfl, le_add_right
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
rw : n' + o' = n + n' - n + (o + o' - o)
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)

Tactic:
rw [add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
rw : n' + o' = n' + (o + o' - o)
⊢ n' + o' = n + n' - n + (o + o' - o)

Tactic:
rw [add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
rw rw₁ : n' + o' = n' + o'
⊢ n' + o' = n' + (o + o' - o)

Tactic:
rw [add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
repeat' repeat'₁ repeat'₂ : n' + o' = n + n' - n + (o + o' - o)
repeat'₃ : n' + o' = n' + (o + o' - o)
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)

Tactic:
repeat' rw [add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
N : ℕ
⊢ (revAt N : (a : ℕ) → ℕ) 0 = N

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
f : R[X]
rcases :
  ∀ (toFinsupp : AddMonoidAlgebra R ℕ),
    (reflect N { toFinsupp := toFinsupp : R[X] }).support =
      image (⇑(revAt N) : (a : ℕ) → ℕ) { toFinsupp := toFinsupp : R[X] }.support
⊢ (reflect N f).support = image (⇑(revAt N) : (a : ℕ) → ℕ) f.support

Tactic:
rcases f with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
toFinsupp : AddMonoidAlgebra R ℕ
h :
  ∀ (a : ℕ),
    a ∈ (reflect N { toFinsupp := toFinsupp : R[X] }).support ↔
      Membership.mem (γ := Finset ℕ) (image (⇑(revAt N) : (a : ℕ) → ℕ) { toFinsupp := toFinsupp : R[X] }.support) a
⊢ (reflect N { toFinsupp := toFinsupp : R[X] }).support =
    image (⇑(revAt N) : (a : ℕ) → ℕ) { toFinsupp := toFinsupp : R[X] }.support

Tactic:
ext1
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
toFinsupp : AddMonoidAlgebra R ℕ
a : ℕ
⊢ a ∈ (reflect N { toFinsupp := toFinsupp : R[X] }).support ↔
    Membership.mem (γ := Finset ℕ) (image (⇑(revAt N) : (a : ℕ) → ℕ) { toFinsupp := toFinsupp : R[X] }.support) a

Tactic:
simp only [reflect, support_ofFinsupp, support_embDomain, Finset.mem_map, Finset.mem_image]

Premises used: Finset.mem_image, Polynomial.support_ofFinsupp, Polynomial.reflect, Finset.mem_map, Finsupp.support_embDomain
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
f : R[X]
i : ℕ
rcases :
  ∀ (f : AddMonoidAlgebra R ℕ),
    (reflect N { toFinsupp := f : R[X] }).coeff i = { toFinsupp := f : R[X] }.coeff ((revAt N : (a : ℕ) → ℕ) i)
⊢ (reflect N f).coeff i = f.coeff ((revAt N : (a : ℕ) → ℕ) i)

Tactic:
rcases f with ⟨f⟩
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
simp : Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R) ((f : (a : ℕ) → R) ((revAt N : (a : ℕ) → ℕ) i : ℕ) : R)
⊢ (reflect N { toFinsupp := f : R[X] }).coeff i = { toFinsupp := f : R[X] }.coeff ((revAt N : (a : ℕ) → ℕ) i)

Tactic:
simp only [reflect, coeff]

Premises used: Polynomial.coeff, Polynomial.reflect
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
rw rw₁ : Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R)
⊢ Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R)
    ((embDomain (revAt N) f : (a : ℕ) → R) ((revAt N : (a : ℕ) → ℕ) ((revAt N : (a : ℕ) → ℕ) i : ℕ) : ℕ) : R)

Tactic:
rw [revAt_invol]

Premises used: Polynomial.revAt_invol
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) ((revAt N : (a : ℕ) → ℕ) ((revAt N : (a : ℕ) → ℕ) i : ℕ) : ℕ) : R)
    ((f : (a : ℕ) → R) ((revAt N : (a : ℕ) → ℕ) i : ℕ) : R)

Tactic:
Finsupp.embDomain_apply_self _ _ _

Premises used: Finsupp.embDomain_apply_self
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
f₁ :
  Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R)
    ((embDomain (revAt N) f : (a : ℕ) → R) ((revAt N : (a : ℕ) → ℕ) ((revAt N : (a : ℕ) → ℕ) i : ℕ) : ℕ) : R)
⊢ Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R) ((f : (a : ℕ) → R) ((revAt N : (a : ℕ) → ℕ) i : ℕ) : R)

Tactic:
calc
    Finsupp.embDomain (revAt N) f i = Finsupp.embDomain (revAt N) f (revAt N (revAt N i)) := by
      rw [revAt_invol]
    _ = f (revAt N i) := Finsupp.embDomain_apply_self _ _ _

Premises used: Polynomial.revAt, Finsupp.embDomain_apply_self, Finsupp.embDomain, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
p : R[X]
a : ∀ (n : ℕ), (reflect N (reflect N p)).coeff n = p.coeff n
⊢ reflect N (reflect N p) = p

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
p : R[X]
n : ℕ
⊢ (reflect N (reflect N p)).coeff n = p.coeff n

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) (reflect N 0) 0

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, dite, Multiset.ofList, Polynomial.reflect, Finsupp.embDomain, rfl
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
f : R[X]
rw : (reflect N f).toFinsupp = 0 ↔ f = 0
rw₁ : { toFinsupp := embDomain (revAt N) f.toFinsupp : R[X] }.toFinsupp = 0 ↔ f = 0
rw₂ : f.toFinsupp = 0 ↔ f = 0
rw₃ rw₄ : f.toFinsupp = 0 ↔ f.toFinsupp = 0
⊢ reflect N f = 0 ↔ f = 0

Tactic:
rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]

Premises used: Finsupp.embDomain_eq_zero, Polynomial.reflect, Polynomial.ofFinsupp_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
N : ℕ
a : ∀ (n : ℕ), (reflect N (f + g)).coeff n = (reflect N f + reflect N g).coeff n
⊢ reflect N (f + g) = reflect N f + reflect N g

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
N n : ℕ
⊢ (reflect N (f + g)).coeff n = (reflect N f + reflect N g).coeff n

Tactic:
simp only [coeff_add, coeff_reflect]

Premises used: Polynomial.coeff_reflect, Polynomial.coeff_add
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
r : R
N : ℕ
a :
  ∀ (n : ℕ),
    (reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f)).coeff n =
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (reflect N f)).coeff n
⊢ reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (reflect N f)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
r : R
N n : ℕ
⊢ (reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) f)).coeff n =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (reflect N f)).coeff n

Tactic:
simp only [coeff_reflect, coeff_C_mul]

Premises used: Polynomial.coeff_C_mul, Polynomial.coeff_reflect
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N n : ℕ
c : R
a :
  ∀ (n_1 : ℕ),
    (reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n))).coeff n_1 =
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ))).coeff
        n_1
⊢ reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X])
      (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ))

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N n : ℕ
c : R
n_1 : ℕ
⊢ (reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n))).coeff n_1 =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ))).coeff
      n_1

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
r : R
N : ℕ
rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X N)
| reflect N ((C : (a : R) → R[X]) r)

Tactic:
rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]

Premises used: Polynomial.C, Polynomial.revAt_zero, pow_zero, Polynomial.reflect_C_mul_X_pow, mul_one, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
r : R
N : ℕ
conv_lhs :
  reflect N ((C : (a : R) → R[X]) r) = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X N)
conv_lhs₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X N) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X N)
⊢ reflect N ((C : (a : R) → R[X]) r) = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X N)

Tactic:
conv_lhs => rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]

Premises used: Polynomial.C, Polynomial.revAt_zero, pow_zero, Polynomial.reflect_C_mul_X_pow, mul_one, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N n : ℕ
rw : reflect N (1 * HPow.hPow (α := R[X]) X n) = HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)
rw₁ : reflect N (1 * HPow.hPow (α := R[X]) X n) = 1 * HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)
rw₂ :
  reflect N ((C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n) =
    (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)
rw₃ rw₄ :
  (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ) =
    (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)
⊢ reflect N (HPow.hPow (α := R[X]) X n) = HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)

Tactic:
rw [← one_mul (X ^ n), ← one_mul (X ^ revAt N n), ← C_1, reflect_C_mul_X_pow]

Premises used: Polynomial.C_1, Polynomial.revAt, HPow.hPow, Polynomial.reflect_C_mul_X_pow, Polynomial.X, DFunLike.coe, one_mul
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) (reflect 1 X) 1

Tactic:
simpa using reflect_monomial 1 1 (R := R)

Premises used: Polynomial.reflect_monomial, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
a : ∀ (n_1 : ℕ), (reflect n (map f p)).coeff n_1 = (map f (reflect n p)).coeff n_1
⊢ reflect n (map f p) = map f (reflect n p)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
p : R[X]
n n_1 : ℕ
⊢ (reflect n (map f p)).coeff n_1 = (map f (reflect n p)).coeff n_1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
rw : reflect n ((C : (a : R) → R[X]) 1) = HPow.hPow (α := R[X]) X n
rw₁ : (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n = HPow.hPow (α := R[X]) X n
rw₂ : 1 * HPow.hPow (α := R[X]) X n = HPow.hPow (α := R[X]) X n
rw₃ rw₄ : HPow.hPow (α := R[X]) X n = HPow.hPow (α := R[X]) X n
⊢ reflect n 1 = HPow.hPow (α := R[X]) X n

Tactic:
rw [← C.map_one, reflect_C, map_one, one_mul]

Premises used: Polynomial.C, RingHom.map_one, map_one, Polynomial.reflect_C, one_mul
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
zero :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]

Premises used: Polynomial.C_mul_X_pow_eq_self
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
pos : ∀ (g0 : g = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
neg : ∀ (g0 : ¬g = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
by_cases g0 : g = 0
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
pos : reflect (N + O) (f * 0) = reflect N f * reflect O 0
pos₁ : reflect (N + O) (f * 0) = reflect N f * 0
pos₂ : reflect (N + O) 0 = reflect N f * 0
pos₃ : Eq.{u_1 + 1} (α := R[X]) (reflect (N + O) 0) 0
pos₄ pos₅ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]

Premises used: Polynomial.reflect_zero, MulZeroClass.mul_zero