awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
| fun (b : ι) ↦ (HSMul.hSMul (β := A[X]) (v b) (map (algebraMap R A) (f b))).coeff (f i).natDegree
have h₁ : ∀ (x : ι), (HSMul.hSMul (β := A[X]) (v x) (map (algebraMap R A) (f x))).coeff (f i).natDegree
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
x : ι
| (HSMul.hSMul (β := A[X]) (v x) (map (algebraMap R A) (f x))).coeff (f i).natDegree
have h₁ : (f x).coeff (f i).natDegree • v x
Tactic: rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
| fun (b : ι) ↦ (HSMul.hSMul (β := A[X]) (v b) (map (algebraMap R A) (f b))).coeff (f i).natDegree
have h₁ : ∀ (x : ι), (f x).coeff (f i).natDegree • v x
Tactic: ext
      rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ Ne.{u_1 + 1} (α := A) (∑ b ∈ s, (HSMul.hSMul (β := A[X]) (v b) (map (algebraMap R A) (f b))).coeff (f i).natDegree) 0
have neg : Ne.{u_1 + 1} (α := A) (∑ x ∈ s, (f x).coeff (f i).natDegree • v x) 0
Tactic: conv in (fun _ ↦ _) =>
      ext
      rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
⊢ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) =
    s.sup fun (i : ι) ↦ (f i).natDegree
have a : natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) ≤
  s.sup fun (i : ι) ↦ (f i).natDegree
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
a :
  natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) ≤
    s.sup fun (i : ι) ↦ (f i).natDegree
⊢ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) =
    s.sup fun (i : ι) ↦ (f i).natDegree
have a₁ : (s.sup fun (i : ι) ↦ (f i).natDegree) ≤
  natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
⊢ (s.sup fun (i : ι) ↦ (f i).natDegree) ≤
    natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
have a : ∀ b ∈ s,
  (f b).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
Tactic: apply Finset.sup_le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
⊢ (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
have pos : ∀ (hf : f i = 0),
  (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
Tactic: by_cases hf : f i = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
pos :
  ∀ (hf : f i = 0),
    (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
⊢ (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
have neg : ∀ (hf : ¬f i = 0),
  (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
Tactic: by_cases hf : f i = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommRing R
A : Type u_1
inst_1 : CommRing A
inst_2 : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v (↑s : Set ι)
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ (f i).natDegree ≤ natDegree.{u_1} (R := A) (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i)))
have neg : Ne.{u_1 + 1} (α := A) (coeff (∑ i ∈ s, HSMul.hSMul (β := A[X]) (v i) (map (algebraMap R A) (f i))) (f i).natDegree) 0
Tactic: apply le_natDegree_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
s : Multiset R
⊢ natDegree (R := R)
      (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s)) =
    s.card
have rw : (Multiset.map
      (Function.comp (β := R[X]) natDegree fun (x : R) ↦
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
      s).sum =
  s.card
Tactic: rw [natDegree_multiset_prod_of_monic, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
s : Multiset R
rw :
  (Multiset.map
        (Function.comp (β := R[X]) natDegree fun (x : R) ↦
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
        s).sum =
    s.card
⊢ natDegree (R := R)
      (prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s)) =
    s.card
have h : ∀ (f : R[X]),
  Membership.mem (γ := Multiset R[X])
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) s) f →
    f.Monic
Tactic: rw [natDegree_multiset_prod_of_monic, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
⊢ natDegree.{u} (R := R) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) = #s
have rw : natDegree.{u} (R := R)
    (prod
      (Multiset.map (fun (a : α) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) s.val)) =
  #s
Tactic: rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
rw :
  natDegree.{u} (R := R)
      (prod
        (Multiset.map (fun (a : α) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) s.val)) =
    #s
⊢ natDegree.{u} (R := R) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) = #s
have rw₁ : natDegree (R := R)
    (prod
      (Multiset.map ((fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∘ f) s.val)) =
  #s
Tactic: rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
rw :
  natDegree.{u} (R := R)
      (prod
        (Multiset.map (fun (a : α) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) s.val)) =
    #s
rw₁ :
  natDegree (R := R)
      (prod
        (Multiset.map ((fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∘ f)
          s.val)) =
    #s
⊢ natDegree.{u} (R := R) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) = #s
have rw₂ : natDegree (R := R)
    (prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
        (Multiset.map f s.val))) =
  #s
Tactic: rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
rw :
  natDegree.{u} (R := R)
      (prod
        (Multiset.map (fun (a : α) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) s.val)) =
    #s
rw₁ :
  natDegree (R := R)
      (prod
        (Multiset.map ((fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∘ f)
          s.val)) =
    #s
rw₂ :
  natDegree (R := R)
      (prod
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          (Multiset.map f s.val))) =
    #s
⊢ natDegree.{u} (R := R) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) = #s
have rw₃ : (Multiset.map f s.val).card = #s
Tactic: rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
rw :
  natDegree.{u} (R := R)
      (prod
        (Multiset.map (fun (a : α) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) s.val)) =
    #s
rw₁ :
  natDegree (R := R)
      (prod
        (Multiset.map ((fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∘ f)
          s.val)) =
    #s
rw₂ :
  natDegree (R := R)
      (prod
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          (Multiset.map f s.val))) =
    #s
rw₃ : (Multiset.map f s.val).card = #s
⊢ natDegree.{u} (R := R) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) = #s
have rw₄ : s.val.card = #s
Tactic: rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
α : Type u_1
s : Finset α
f : α → R
rw :
  natDegree.{u} (R := R)
      (prod
        (Multiset.map (fun (a : α) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) s.val)) =
    #s
rw₁ :
  natDegree (R := R)
      (prod
        (Multiset.map ((fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∘ f)
          s.val)) =
    #s
rw₂ :
  natDegree (R := R)
      (prod
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          (Multiset.map f s.val))) =
    #s
rw₃ : (Multiset.map f s.val).card = #s
rw₄ : s.val.card = #s
⊢ natDegree.{u} (R := R) (∏ a ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f a) : R[X])) = #s
have rw₅ : s.val.card = s.val.card
Tactic: rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map,
    natDegree_multiset_prod_X_sub_C_eq_card, Multiset.card_map, Finset.card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
⊢ natDegree.{u} (R := R) (∏ i ∈ s, f i) = ∑ i ∈ s, (f i).natDegree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
h_1 : Nontrivial R
⊢ natDegree.{u} (R := R) (∏ i ∈ s, f i) = ∑ i ∈ s, (f i).natDegree
have h₁ : Ne.{u + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
Tactic: apply natDegree_prod'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
ι : Type w
s : Finset ι
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
h_1 : Nontrivial R
⊢ Ne.{u + 1} (α := R) (∏ i ∈ s, (f i).leadingCoeff) 0
have h₁ : ∀ a ∈ s, (f a).leadingCoeff ≠ 0
Tactic: rw [prod_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
h_1 : Nontrivial R
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum
have h₁ : Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0
Tactic: rw [natDegree_multiset_prod']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
h_1 : Nontrivial R
⊢ Ne (α := R) (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)) 0
have h₁ : ¬∃ a ∈ t, a = 0
Tactic: simp_rw [Ne, Multiset.prod_eq_zero_iff, Multiset.mem_map, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.BigOperators (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
t : Multiset R[X]
⊢ t.prod.leadingCoeff = prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t)
have rw : Eq (α := R) (prod (Multiset.map (⇑leadingCoeffHom : (a : R[X]) → R) t))
  (prod (Multiset.map (fun (f : R[X]) ↦ f.leadingCoeff) t))
Tactic: rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : R[X]
⊢ evalEval x y ((C : (a : R[X]) → R[X][Y]) p) = eval x p
have rw : eval x (eval ((C : (a : R) → R[X]) y) ((C : (a : R[X]) → R[X][Y]) p)) = eval x p
Tactic: rw [evalEval, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : R[X]
rw : eval x (eval ((C : (a : R) → R[X]) y) ((C : (a : R[X]) → R[X][Y]) p)) = eval x p
⊢ evalEval x y ((C : (a : R[X]) → R[X][Y]) p) = eval x p
have rw₁ : eval x p = eval x p
Tactic: rw [evalEval, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : R[X]
⊢ evalEval x y (map C p) = eval y p
have rw : eval x (eval ((C : (a : R) → R[X]) y) (map C p)) = eval y p
Tactic: rw [evalEval, eval_map_apply, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : R[X]
rw : eval x (eval ((C : (a : R) → R[X]) y) (map C p)) = eval y p
⊢ evalEval x y (map C p) = eval y p
have rw₁ : eval x ((C : (a : R) → R[X]) (eval y p)) = eval y p
Tactic: rw [evalEval, eval_map_apply, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : R[X]
rw : eval x (eval ((C : (a : R) → R[X]) y) (map C p)) = eval y p
rw₁ : eval x ((C : (a : R) → R[X]) (eval y p)) = eval y p
⊢ evalEval x y (map C p) = eval y p
have rw₂ : eval y p = eval y p
Tactic: rw [evalEval, eval_map_apply, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y p : R
⊢ evalEval x y (CC p) = p
have rw : eval x ((C : (a : R) → R[X]) p) = p
Tactic: rw [evalEval_C, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y p : R
rw : eval x ((C : (a : R) → R[X]) p) = p
⊢ evalEval x y (CC p) = p
have rw₁ : p = p
Tactic: rw [evalEval_C, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
⊢ evalEval x y Y = y
have rw : eval x (eval ((C : (a : R) → R[X]) y) Y) = y
Tactic: rw [evalEval, eval_X, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
rw : eval x (eval ((C : (a : R) → R[X]) y) Y) = y
⊢ evalEval x y Y = y
have rw₁ : eval x ((C : (a : R) → R[X]) y) = y
Tactic: rw [evalEval, eval_X, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
rw : eval x (eval ((C : (a : R) → R[X]) y) Y) = y
rw₁ : eval x ((C : (a : R) → R[X]) y) = y
⊢ evalEval x y Y = y
have rw₂ : y = y
Tactic: rw [evalEval, eval_X, eval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
l : List R[X][Y]
⊢ evalEval x y l.prod = (List.map (evalEval x y) l).prod
have simp : (List.map (Function.comp (β := R[X]) (eval x) (eval ((C : (a : R) → R[X]) y))) l).prod =
  (List.map (evalEval x y) l).prod
Tactic: simp only [evalEval, eval_list_prod, List.map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x : R
⊢ Eq (α := (y : R) → R[X][Y] →+* R) (evalEvalRingHom x) (eval₂RingHom (evalRingHom x))
have h : ∀ (x_1 x_2 : R),
  Eq (α := R) ((RingHom.comp (RingHom.comp (evalEvalRingHom x x_1) C) C : (a : R) → R) x_2 : R)
    ((RingHom.comp (RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C) C : (a : R) → R) x_2 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x : R
h :
  ∀ (x_1 x_2 : R),
    Eq (α := R) ((RingHom.comp (RingHom.comp (evalEvalRingHom x x_1) C) C : (a : R) → R) x_2 : R)
      ((RingHom.comp (RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C) C : (a : R) → R) x_2 : R)
⊢ Eq (α := (y : R) → R[X][Y] →+* R) (evalEvalRingHom x) (eval₂RingHom (evalRingHom x))
have h₁ : ∀ (x_1 : R),
  Eq (α := R) ((RingHom.comp (evalEvalRingHom x x_1) C : (a : R[X]) → R) X : R)
    ((RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C : (a : R[X]) → R) X : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x : R
h :
  ∀ (x_1 x_2 : R),
    Eq (α := R) ((RingHom.comp (RingHom.comp (evalEvalRingHom x x_1) C) C : (a : R) → R) x_2 : R)
      ((RingHom.comp (RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C) C : (a : R) → R) x_2 : R)
h₁ :
  ∀ (x_1 : R),
    Eq (α := R) ((RingHom.comp (evalEvalRingHom x x_1) C : (a : R[X]) → R) X : R)
      ((RingHom.comp (eval₂RingHom (evalRingHom x) x_1) C : (a : R[X]) → R) X : R)
⊢ Eq (α := (y : R) → R[X][Y] →+* R) (evalEvalRingHom x) (eval₂RingHom (evalRingHom x))
have h₂ : ∀ (x_1 : R),
  Eq (α := R) ((evalEvalRingHom x x_1 : (a : R[X][Y]) → R) Y : R)
    ((eval₂RingHom (evalRingHom x) x_1 : (a : R[X][Y]) → R) Y : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x : R
⊢ Eq (α := (x : R) → (p : R[X][Y]) → R) (eval₂ (evalRingHom x)) (evalEval x)
have h : ∀ (x_1 : R), Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (evalEval x x_1)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x x_1 : R
⊢ Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (evalEval x x_1)
have h : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (⇑(evalEvalRingHom x x_1) : (a : R[X][Y]) → R)
Tactic: rw [← coe_evalEvalRingHom, evalEvalRingHom_eq, coe_eval₂RingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x x_1 : R
h : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (⇑(evalEvalRingHom x x_1) : (a : R[X][Y]) → R)
⊢ Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (evalEval x x_1)
have h₁ : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (⇑(eval₂RingHom (evalRingHom x) x_1) : (a : R[X][Y]) → R)
Tactic: rw [← coe_evalEvalRingHom, evalEvalRingHom_eq, coe_eval₂RingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x x_1 : R
h : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (⇑(evalEvalRingHom x x_1) : (a : R[X][Y]) → R)
h₁ : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (⇑(eval₂RingHom (evalRingHom x) x_1) : (a : R[X][Y]) → R)
⊢ Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (evalEval x x_1)
have h₂ : Eq (α := (p : R[X][Y]) → R) (eval₂ (evalRingHom x) x_1) (eval₂ (evalRingHom x) x_1)
Tactic: rw [← coe_evalEvalRingHom, evalEvalRingHom_eq, coe_eval₂RingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p : R[X][Y]
⊢ eval y (map (evalRingHom x) p) = evalEval x y p
have rw : eval₂ (evalRingHom x) y p = evalEval x y p
Tactic: rw [eval_map, eval₂_evalRingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p : R[X][Y]
rw : eval₂ (evalRingHom x) y p = evalEval x y p
⊢ eval y (map (evalRingHom x) p) = evalEval x y p
have rw₁ : evalEval x y p = evalEval x y p
Tactic: rw [eval_map, eval₂_evalRingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
⊢ eval (map f q) (map (mapRingHom f) p) = map f (eval q p)
have rw : eval₂ (mapRingHom f) (map f q) p = map f (eval q p)
Tactic: rw [eval_map, ← coe_mapRingHom, eval₂_hom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
rw : eval₂ (mapRingHom f) (map f q) p = map f (eval q p)
⊢ eval (map f q) (map (mapRingHom f) p) = map f (eval q p)
have rw₁ : eval₂ (mapRingHom f) ((mapRingHom f : (a : R[X]) → S[X]) q) p = (mapRingHom f : (a : R[X]) → S[X]) (eval q p)
Tactic: rw [eval_map, ← coe_mapRingHom, eval₂_hom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
rw : eval₂ (mapRingHom f) (map f q) p = map f (eval q p)
rw₁ : eval₂ (mapRingHom f) ((mapRingHom f : (a : R[X]) → S[X]) q) p = (mapRingHom f : (a : R[X]) → S[X]) (eval q p)
⊢ eval (map f q) (map (mapRingHom f) p) = map f (eval q p)
have rw₂ : Eq.{u_2 + 1} (α := S[X]) ((mapRingHom f : (a : R[X]) → S[X]) (eval q p) : S[X])
  ((mapRingHom f : (a : R[X]) → S[X]) (eval q p) : S[X])
Tactic: rw [eval_map, ← coe_mapRingHom, eval₂_hom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Bivariate (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
r : R
⊢ Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) r) (eval (map f q) (map (mapRingHom f) p)) : S)
    ((f : (a : R) → S) (eval r (eval q p)) : S)
have rw : Eq.{u_2 + 1} (α := S) (eval ((f : (a : R) → S) r) (map f (eval q p)) : S) ((f : (a : R) → S) (eval r (eval q p)) : S)
Tactic: rw [map_mapRingHom_eval_map, eval_map, eval₂_hom]