awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (hypothesis)
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
⊢ q₁ = q₂ ∧ r₁₁ = r₁₂ ∧ r₂₁ = r₂₂
have hr₂ : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.PartialFractions (goal)
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₂₂
have 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))
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)⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ a = b
have rw : revAtFun N (revAtFun N a) = b
Tactic: rw [← @revAtFun_invol N a, hab, revAtFun_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
rw : revAtFun N (revAtFun N a) = b
⊢ a = b
have rw₁ : revAtFun N (revAtFun N b) = b
Tactic: rw [← @revAtFun_invol N a, hab, revAtFun_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ a = b
have rw₂ : b = b
Tactic: rw [← @revAtFun_invol N a, hab, revAtFun_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
N O n o : ℕ
hn : n ≤ N
ho : o ≤ O
⊢ (revAt (N + O) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt N : (a : ℕ) → ℕ) n : ℕ) ((revAt O : (a : ℕ) → ℕ) o : ℕ)
have rcases : ∀ (n' : ℕ) (hn : n ≤ n + n'),
  (revAt (n + n' + O) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt (n + n') : (a : ℕ) → ℕ) n : ℕ) ((revAt O : (a : ℕ) → ℕ) o : ℕ)
Tactic: rcases Nat.le.dest hn with ⟨n', rfl⟩
Cleared hypotheses: N, hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
O n o : ℕ
ho : o ≤ O
n' : ℕ
hn : n ≤ n + n'
⊢ (revAt (n + n' + O) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (α := ℕ) (β := ℕ) ((revAt (n + n') : (a : ℕ) → ℕ) n : ℕ) ((revAt O : (a : ℕ) → ℕ) o : ℕ)
have 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 : ℕ)
Tactic: rcases Nat.le.dest ho with ⟨o', rfl⟩
Cleared hypotheses: O, ho
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
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 : ℕ)
have rw : (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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) =
    HAdd.hAdd (β := ℕ) (n + n' - n) ((revAt (o + o') : (a : ℕ) → ℕ) o : ℕ)
have rw : (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) = n + n' - n + (o + o' - o)
Tactic: rw [revAt_le (le_add_right rfl.le)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
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 : ℕ)
have repeat' : (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) = n + n' - n + (o + o' - o)
Tactic: repeat' rw [revAt_le (le_add_right rfl.le)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o')) : (a : ℕ) → ℕ) (n + o) = n + n' - n + (o + o' - o)
have rw : n + o + (n' + o') - (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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
have rw : n' + o' = n + n' - n + (o + o' - o)
Tactic: rw [add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n + n' - n + (o + o' - o)
have rw : n' + o' = n' + (o + o' - o)
Tactic: rw [add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + (o + o' - o)
have rw : n' + o' = n' + o'
Tactic: rw [add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
have repeat' : n' + o' = n + n' - n + (o + o' - o)
Tactic: repeat' rw [add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
repeat' repeat'₁ repeat'₂ : n' + o' = n + n' - n + (o + o' - o)
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
have repeat'₃ : n' + o' = n' + (o + o' - o)
Tactic: repeat' rw [add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
f : R[X]
⊢ (reflect N f).support = image (⇑(revAt N) : (a : ℕ) → ℕ) f.support
have rcases : ∀ (toFinsupp : AddMonoidAlgebra R ℕ),
  (reflect N { toFinsupp := toFinsupp : R[X] }).support =
    image (⇑(revAt N) : (a : ℕ) → ℕ) { toFinsupp := toFinsupp : R[X] }.support
Tactic: rcases f with ⟨⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
toFinsupp : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := toFinsupp : R[X] }).support =
    image (⇑(revAt N) : (a : ℕ) → ℕ) { toFinsupp := toFinsupp : R[X] }.support
have h : ∀ (a : ℕ),
  a ∈ (reflect N { toFinsupp := toFinsupp : R[X] }).support ↔
    Membership.mem (γ := Finset ℕ) (image (⇑(revAt N) : (a : ℕ) → ℕ) { toFinsupp := toFinsupp : R[X] }.support) a
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
f : R[X]
i : ℕ
⊢ (reflect N f).coeff i = f.coeff ((revAt N : (a : ℕ) → ℕ) i)
have rcases : ∀ (f : AddMonoidAlgebra R ℕ),
  (reflect N { toFinsupp := f : R[X] }).coeff i = { toFinsupp := f : R[X] }.coeff ((revAt N : (a : ℕ) → ℕ) i)
Tactic: rcases f with ⟨f⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ (reflect N { toFinsupp := f : R[X] }).coeff i = { toFinsupp := f : R[X] }.coeff ((revAt N : (a : ℕ) → ℕ) i)
have simp : Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R) ((f : (a : ℕ) → R) ((revAt N : (a : ℕ) → ℕ) i : ℕ) : R)
Tactic: simp only [reflect, coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N i : ℕ
f : AddMonoidAlgebra 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)
have rw : Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R)
Tactic: rw [revAt_invol]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ Eq (α := R) ((embDomain (revAt N) f : (a : ℕ) → R) i : R) ((f : (a : ℕ) → R) ((revAt N : (a : ℕ) → ℕ) i : ℕ) : R)
have 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)
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 _ _ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
p : R[X]
⊢ reflect N (reflect N p) = p
have a : ∀ (n : ℕ), (reflect N (reflect N p)).coeff n = p.coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
f : R[X]
⊢ reflect N f = 0 ↔ f = 0
have rw : (reflect N f).toFinsupp = 0 ↔ f = 0
Tactic: rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
f : R[X]
rw : (reflect N f).toFinsupp = 0 ↔ f = 0
⊢ reflect N f = 0 ↔ f = 0
have rw₁ : { toFinsupp := embDomain (revAt N) f.toFinsupp : R[X] }.toFinsupp = 0 ↔ f = 0
Tactic: rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ reflect N f = 0 ↔ f = 0
have rw₂ : f.toFinsupp = 0 ↔ f = 0
Tactic: rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ reflect N f = 0 ↔ f = 0
have rw₃ : f.toFinsupp = 0 ↔ f.toFinsupp = 0
Tactic: rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
N : ℕ
⊢ reflect N (f + g) = reflect N f + reflect N g
have a : ∀ (n : ℕ), (reflect N (f + g)).coeff n = (reflect N f + reflect N g).coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
r : R
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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N n : ℕ
c : R
⊢ 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 : ℕ))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
N : ℕ
| reflect N ((C : (a : R) → R[X]) r)
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X N)
Tactic: rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
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)
have 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)
Tactic: conv_lhs => rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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)
⊢ 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)
have 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)
Tactic: conv_lhs => rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N n : ℕ
⊢ reflect N (HPow.hPow (α := R[X]) X n) = HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)
have rw : reflect N (1 * 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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 : ℕ)
⊢ reflect N (HPow.hPow (α := R[X]) X n) = HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)
have rw₁ : reflect N (1 * HPow.hPow (α := R[X]) X n) = 1 * 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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 : ℕ)
⊢ reflect N (HPow.hPow (α := R[X]) X n) = HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)
have 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 : ℕ)
Tactic: rw [← one_mul (X ^ n), ← one_mul (X ^ revAt N n), ← C_1, reflect_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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 : ℕ)
⊢ reflect N (HPow.hPow (α := R[X]) X n) = HPow.hPow (α := R[X]) (β := ℕ) X ((revAt N : (a : ℕ) → ℕ) n : ℕ)
have 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 : ℕ)
Tactic: rw [← one_mul (X ^ n), ← one_mul (X ^ revAt N n), ← C_1, reflect_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ reflect n (map f p) = map f (reflect n p)
have a : ∀ (n_1 : ℕ), (reflect n (map f p)).coeff n_1 = (map f (reflect n p)).coeff n_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ reflect n 1 = HPow.hPow (α := R[X]) X n
have rw : reflect n ((C : (a : R) → R[X]) 1) = HPow.hPow (α := R[X]) X n
Tactic: rw [← C.map_one, reflect_C, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
rw : reflect n ((C : (a : R) → R[X]) 1) = HPow.hPow (α := R[X]) X n
⊢ reflect n 1 = HPow.hPow (α := R[X]) X n
have rw₁ : (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n = HPow.hPow (α := R[X]) X n
Tactic: rw [← C.map_one, reflect_C, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ reflect n 1 = HPow.hPow (α := R[X]) X n
have rw₂ : 1 * HPow.hPow (α := R[X]) X n = HPow.hPow (α := R[X]) X n
Tactic: rw [← C.map_one, reflect_C, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ reflect n 1 = HPow.hPow (α := R[X]) X n
have rw₃ : HPow.hPow (α := R[X]) X n = HPow.hPow (α := R[X]) X n
Tactic: rw [← C.map_one, reflect_C, map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have 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))
Tactic: rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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
⊢ 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))
have 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))
Tactic: simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul,
        reflect_monomial, add_comm, revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ←
        pow_add (X : R[X]), add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
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)
      (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))
have zero₁ : reflect (N + O)
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree) *
        HPow.hPow (α := R[X]) X f.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))
Tactic: simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul,
        reflect_monomial, add_comm, revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ←
        pow_add (X : R[X]), add_comm]