awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
⊢ coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p
have monomial : ∀ (u : τ →₀ ℕ) (a : R),
  Eq.{u_4 + 1} (α := R)
    (coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial u : (a : R) → MvPolynomial τ R) a)))
    (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) a))
Tactic: apply p.induction_on' (P := fun p ↦ (p.killCompl hf).coeff s = p.coeff (s.mapDomain f))
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
monomial :
  ∀ (u : τ →₀ ℕ) (a : R),
    Eq.{u_4 + 1} (α := R)
      (coeff s
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) a)))
      (coeff (Finsupp.mapDomain f s) ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) a))
⊢ coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p
have add : ∀ (p q : MvPolynomial τ R),
  coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p →
    coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) q) = coeff (Finsupp.mapDomain f s) q →
      coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) (p + q)) =
        coeff (Finsupp.mapDomain f s) (p + q)
Tactic: apply p.induction_on' (P := fun p ↦ (p.killCompl hf).coeff s = p.coeff (s.mapDomain f))
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
⊢ Eq.{u_4 + 1} (α := R)
    (coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial u : (a : R) → MvPolynomial τ R) r)))
    (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
have monomial : Eq.{u_4 + 1} (α := R)
  (coeff s
    (if (↑u.support : Set τ) ⊆ range f then (monomial (Finsupp.comapDomain f u sorry) : (a : R) → MvPolynomial σ R) r
    else 0))
  (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
Tactic: rw [killCompl_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
⊢ Eq.{u_4 + 1} (α := R)
    (coeff s
      (if (↑u.support : Set τ) ⊆ range f then (monomial (Finsupp.comapDomain f u ⋯) : (a : R) → MvPolynomial σ R) r
      else 0))
    (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
have pos : ∀ (h : (↑u.support : Set τ) ⊆ range f),
  Eq.{u_4 + 1} (α := R) (coeff s ((monomial (Finsupp.comapDomain f u sorry) : (a : R) → MvPolynomial σ R) r))
    (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
pos :
  ∀ (h : (↑u.support : Set τ) ⊆ range f),
    Eq.{u_4 + 1} (α := R) (coeff s ((monomial (Finsupp.comapDomain f u ⋯) : (a : R) → MvPolynomial σ R) r))
      (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
⊢ Eq.{u_4 + 1} (α := R)
    (coeff s
      (if (↑u.support : Set τ) ⊆ range f then (monomial (Finsupp.comapDomain f u ⋯) : (a : R) → MvPolynomial σ R) r
      else 0))
    (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
have neg : ∀ (h : ¬(↑u.support : Set τ) ⊆ range f),
  Eq.{u_4 + 1} (α := R) (coeff s 0) (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
h : ¬(↑u.support : Set τ) ⊆ range f
⊢ Eq.{u_4 + 1} (α := R) (coeff s 0) (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
have neg : u = Finsupp.mapDomain f s → 0 = r
Tactic: simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
u : τ →₀ ℕ
r : R
h : ¬(↑u.support : Set τ) ⊆ range f
⊢ Eq.{u_4 + 1} (α := R) (coeff s 0) (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) r))
have neg : u = Finsupp.mapDomain f s → 0 = r
Tactic: simp? says simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : ¬(↑(Finsupp.mapDomain f s).support : Set τ) ⊆ range f
⊢ 0 = r
have neg : ∀ (h : 0 ≠ r), (↑(Finsupp.mapDomain f s).support : Set τ) ⊆ range f
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
r : R
h : 0 ≠ r
⊢ (↑(Finsupp.mapDomain f s).support : Set τ) ⊆ range f
have neg : (↑(Finset.image f s.support) : Set τ) ⊆ range f
Tactic: apply subset_trans <| SetLike.coe_subset_coe.mpr <| Finsupp.mapDomain_support
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
⊢ coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p
have monomial : ∀ (u : τ →₀ ℕ) (a : R),
  Eq.{u_4 + 1} (α := R)
    (coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial u : (a : R) → MvPolynomial τ R) a)))
    (coeff (Finsupp.mapDomain f s) ((monomial u : (a : R) → MvPolynomial τ R) a))
Tactic: classical
  apply p.induction_on' (P := fun p ↦ (p.killCompl hf).coeff s = p.coeff (s.mapDomain f))
  · intro u r
    rw [killCompl_monomial]
    split_ifs with h
    · simp [← (Finsupp.mapDomain_injective hf).eq_iff, u.mapDomain_comapDomain _ hf h]
    · simp? says simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]
      intro rfl
      contrapose! h
      apply subset_trans <| SetLike.coe_subset_coe.mpr <| Finsupp.mapDomain_support
      simp
  · simp_intro ..
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
s : σ →₀ ℕ
monomial :
  ∀ (u : τ →₀ ℕ) (a : R),
    Eq.{u_4 + 1} (α := R)
      (coeff s
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
          ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) a)))
      (coeff (Finsupp.mapDomain f s) ((MvPolynomial.monomial u : (a : R) → MvPolynomial τ R) a))
⊢ coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p
have add : ∀ (p q : MvPolynomial τ R),
  coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) = coeff (Finsupp.mapDomain f s) p →
    coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) q) = coeff (Finsupp.mapDomain f s) q →
      coeff s ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) (p + q)) =
        coeff (Finsupp.mapDomain f s) (p + q)
Tactic: classical
  apply p.induction_on' (P := fun p ↦ (p.killCompl hf).coeff s = p.coeff (s.mapDomain f))
  · intro u r
    rw [killCompl_monomial]
    split_ifs with h
    · simp [← (Finsupp.mapDomain_injective hf).eq_iff, u.mapDomain_comapDomain _ hf h]
    · simp? says simp only [coeff_zero, coeff_monomial, right_eq_ite_iff]
      intro rfl
      contrapose! h
      apply subset_trans <| SetLike.coe_subset_coe.mpr <| Finsupp.mapDomain_support
      simp
  · simp_intro ..
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
p : MvPolynomial τ R
⊢ support.{u_4, u_1} (R := R) ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) =
    p.support.preimage (Finsupp.mapDomain f) ⋯
have h : ∀ (x : σ →₀ ℕ),
  Membership.mem (γ := Finset (σ →₀ ℕ))
      (support.{u_4, u_1} (R := R) ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p)) x ↔
    x ∈ p.support.preimage (Finsupp.mapDomain f) sorry
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ ≃ τ
p : MvPolynomial σ R
⊢ (rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    p
have rw : (rename (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := τ) (⇑f.symm : (a : τ) → σ) (⇑f : (a : σ) → τ)) :
      (a : MvPolynomial σ R) → MvPolynomial σ R)
    p =
  p
Tactic: rw [rename_rename, f.symm_comp_self, rename_id_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ ≃ τ
p : MvPolynomial σ R
rw :
  (rename (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := τ) (⇑f.symm : (a : τ) → σ) (⇑f : (a : σ) → τ)) :
        (a : MvPolynomial σ R) → MvPolynomial σ R)
      p =
    p
⊢ (rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    p
have rw₁ : (rename id : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
Tactic: rw [rename_rename, f.symm_comp_self, rename_id_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ ≃ τ
p : MvPolynomial σ R
rw :
  (rename (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := τ) (⇑f.symm : (a : τ) → σ) (⇑f : (a : σ) → τ)) :
        (a : MvPolynomial σ R) → MvPolynomial σ R)
      p =
    p
rw₁ : (rename id : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
⊢ (rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) p) =
    p
have rw₂ : p = p
Tactic: rw [rename_rename, f.symm_comp_self, rename_id_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ ≃ τ
p : MvPolynomial τ R
⊢ (rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
      ((rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) p) =
    p
have rw : (rename (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := σ) (⇑f : (a : σ) → τ) (⇑f.symm : (a : τ) → σ)) :
      (a : MvPolynomial τ R) → MvPolynomial τ R)
    p =
  p
Tactic: rw [rename_rename, f.self_comp_symm, rename_id_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ ≃ τ
p : MvPolynomial τ R
rw :
  (rename (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := σ) (⇑f : (a : σ) → τ) (⇑f.symm : (a : τ) → σ)) :
        (a : MvPolynomial τ R) → MvPolynomial τ R)
      p =
    p
⊢ (rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
      ((rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) p) =
    p
have rw₁ : (rename id : (a : MvPolynomial τ R) → MvPolynomial τ R) p = p
Tactic: rw [rename_rename, f.self_comp_symm, rename_id_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ ≃ τ
p : MvPolynomial τ R
rw :
  (rename (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := σ) (⇑f : (a : σ) → τ) (⇑f.symm : (a : τ) → σ)) :
        (a : MvPolynomial τ R) → MvPolynomial τ R)
      p =
    p
rw₁ : (rename id : (a : MvPolynomial τ R) → MvPolynomial τ R) p = p
⊢ (rename (⇑f : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
      ((rename (⇑f.symm : (a : τ) → σ) : (a : MvPolynomial τ R) → MvPolynomial σ R) p) =
    p
have rw₂ : p = p
Tactic: rw [rename_rename, f.self_comp_symm, rename_id_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p
have C : ∀ (a : R),
  eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a)) =
    eval₂ f (g ∘ k) ((C : (a : R) → MvPolynomial σ R) a)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
C :
  ∀ (a : R),
    eval₂ f g
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ f (g ∘ k) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
⊢ eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p
have add : ∀ (p q : MvPolynomial σ R),
  eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p →
    eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) q) = eval₂ f (g ∘ k) q →
      eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) = eval₂ f (g ∘ k) (p + q)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
C :
  ∀ (a : R),
    eval₂ f g
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) =
      eval₂ f (g ∘ k) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p →
      eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) q) = eval₂ f (g ∘ k) q →
        eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) = eval₂ f (g ∘ k) (p + q)
⊢ eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ),
  eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) = eval₂ f (g ∘ k) p →
    eval₂ f g ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X n)) = eval₂ f (g ∘ k) (p * X n)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ C (g ∘ k) p) : MvPolynomial τ R)
    (eval₂ C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
have C : ∀ (a : R),
  Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ C (g ∘ k) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)
    (eval₂ C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial τ R)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial τ R)
      ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R)
          (eval₂ MvPolynomial.C (g ∘ k) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
      (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) p) : MvPolynomial τ R)
    (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
have add : ∀ (p q : MvPolynomial σ R),
  Eq (α := MvPolynomial τ R)
      ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) p) : MvPolynomial τ R)
      (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
        MvPolynomial τ R) →
    Eq (α := MvPolynomial τ R)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) q) : MvPolynomial τ R)
        (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
            ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
          MvPolynomial τ R) →
      Eq (α := MvPolynomial τ R)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) (p + q)) :
          MvPolynomial τ R)
        (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
            ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) :
          MvPolynomial τ R)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
k : σ → τ
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := MvPolynomial τ R)
      ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R)
          (eval₂ MvPolynomial.C (g ∘ k) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
      (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        MvPolynomial τ R)
add :
  ∀ (p q : MvPolynomial σ R),
    Eq (α := MvPolynomial τ R)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) p) : MvPolynomial τ R)
        (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
            ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
          MvPolynomial τ R) →
      Eq (α := MvPolynomial τ R)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) q) : MvPolynomial τ R)
          (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
              ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) q) :
            MvPolynomial τ R) →
        Eq (α := MvPolynomial τ R)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) (p + q)) :
            MvPolynomial τ R)
          (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
              ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p + q)) :
            MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) p) : MvPolynomial τ R)
    (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
        ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
      MvPolynomial τ R)
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ),
  Eq (α := MvPolynomial τ R)
      ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) p) : MvPolynomial τ R)
      (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) p) :
        MvPolynomial τ R) →
    Eq (α := MvPolynomial τ R)
      ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (eval₂ MvPolynomial.C (g ∘ k) (p * X n)) :
        MvPolynomial τ R)
      (eval₂ MvPolynomial.C ((⇑(rename k) : (a : MvPolynomial σ R) → MvPolynomial τ R) ∘ g)
          ((rename k : (a : MvPolynomial σ R) → MvPolynomial τ R) (p * X n)) :
        MvPolynomial τ R)
Tactic: apply MvPolynomial.induction_on p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (eval₂ C g p) : MvPolynomial (τ × σ) R)
    (eval₂ C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x)) p :
      MvPolynomial (τ × σ) R)
have C : ∀ (a : R),
  Eq (α := MvPolynomial (τ × σ) R)
    ((rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R)
        (eval₂ C g ((C : (a : R) → MvPolynomial σ R) a)) :
      MvPolynomial (τ × σ) R)
    (eval₂ C (fun (x : σ) ↦ (rename (Prod.mk j) : (a : MvPolynomial σ R) → MvPolynomial (τ × σ) R) (g x))
        ((C : (a : R) → MvPolynomial σ R) a) :
      MvPolynomial (τ × σ) R)
Tactic: apply MvPolynomial.induction_on p