awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)
have refine_1 : ∀ (this : Fintype σ) (α β : Type u_1) [Fintype β] (e : α ≃ β),
  (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
    ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)
Tactic: refine have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
refine_1 :
  ∀ (this : Fintype σ) (α β : Type u_1) [Fintype β] (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)
have refine_2 : ∀ (this : Fintype σ) (x : MvPolynomial PEmpty.{u_1 + 1} R),
  IsNilpotent x ↔ ∀ (i : PEmpty.{u_1 + 1} →₀ ℕ), IsNilpotent (coeff i x)
Tactic: refine have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
refine_1 :
  ∀ (this : Fintype σ) (α β : Type u_1) [Fintype β] (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)
refine_2 :
  ∀ (this : Fintype σ) (x : MvPolynomial PEmpty.{u_1 + 1} R),
    IsNilpotent x ↔ ∀ (i : PEmpty.{u_1 + 1} →₀ ℕ), IsNilpotent (coeff i x)
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)
have refine_3 : ∀ (this : Fintype σ) (α : Type u_1) [Fintype α],
  (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
    ∀ (x : MvPolynomial.{u_1, u_2} (Option α) R), IsNilpotent x ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i x)
Tactic: refine have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P_1 : MvPolynomial σ R
inst_1 : Finite σ
this : Fintype σ
α β : Type u_1
inst_2 : Fintype β
e : α ≃ β
h₁ : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial β R
⊢ IsNilpotent P ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i P)
have refine_1 : (∀ (b : β →₀ ℕ),
    IsNilpotent.{u_2} (R := R)
      (coeff.{u_2, u_1} (σ := α) ((Equiv.symm (Finsupp.equivCongrLeft e) : (a : β →₀ ℕ) → α →₀ ℕ) b)
        ((rename (⇑e.symm : (a : β) → α) : (a : MvPolynomial β R) → MvPolynomial α R) P))) ↔
  ∀ (i : β →₀ ℕ), IsNilpotent (coeff i P)
Tactic: rw [← IsNilpotent.map_iff (rename_injective _ e.symm.injective), h₁,
      (Finsupp.equivCongrLeft e).forall_congr_left]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P_1 : MvPolynomial σ R
inst_1 : Finite σ
this : Fintype σ
α : Type u_1
inst_2 : Fintype α
H : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial.{u_1, u_2} (Option α) R
⊢ IsNilpotent P ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i P)
have refine_3 : ∀ (P : Polynomial (MvPolynomial α R)),
  IsNilpotent (R := MvPolynomial.{u_1, u_2} (Option α) R)
      ((AlgEquiv.symm (optionEquivLeft R α) : (a : Polynomial (MvPolynomial α R)) → MvPolynomial (Option α) R) P :
        MvPolynomial.{u_1, u_2} (Option α) R) ↔
    ∀ (i : Option α →₀ ℕ),
      IsNilpotent.{u_2} (R := R)
        (coeff i
          ((AlgEquiv.symm (optionEquivLeft R α) : (a : Polynomial (MvPolynomial α R)) → MvPolynomial (Option α) R) P))
Tactic: obtain ⟨P, rfl⟩ := (optionEquivLeft _ _).symm.surjective P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)
have refine_1 : ∀ (this : Fintype σ) (α β : Type u_1) [Fintype β] (e : α ≃ β),
  (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
    ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)
Tactic: classical
  -- Note: including `Fintype.ofFinite σ` in the entire context interferes with the `rw` below.
  refine have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P
  · intro α β _ e h₁ P
    rw [← IsNilpotent.map_iff (rename_injective _ e.symm.injective), h₁,
      (Finsupp.equivCongrLeft e).forall_congr_left]
    simp [Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective]
  · simp [Unique.forall_iff, ← IsNilpotent.map_iff (isEmptyRingEquiv R PEmpty).injective,
      -isEmptyRingEquiv_apply, isEmptyRingEquiv_eq_coeff_zero]
  · intro α _ H P
    obtain ⟨P, rfl⟩ := (optionEquivLeft _ _).symm.surjective P
    simp [IsNilpotent.map_iff (optionEquivLeft _ _).symm.injective,
      Polynomial.isNilpotent_iff, H, Finsupp.optionEquiv.forall_congr_left,
      ← optionEquivLeft_coeff_some_coeff_none, Finsupp.coe_update]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
refine_1 :
  ∀ (this : Fintype σ) (α β : Type u_1) [Fintype β] (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)
have refine_2 : ∀ (this : Fintype σ) (x : MvPolynomial PEmpty.{u_1 + 1} R),
  IsNilpotent x ↔ ∀ (i : PEmpty.{u_1 + 1} →₀ ℕ), IsNilpotent (coeff i x)
Tactic: classical
  -- Note: including `Fintype.ofFinite σ` in the entire context interferes with the `rw` below.
  refine have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P
  · intro α β _ e h₁ P
    rw [← IsNilpotent.map_iff (rename_injective _ e.symm.injective), h₁,
      (Finsupp.equivCongrLeft e).forall_congr_left]
    simp [Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective]
  · simp [Unique.forall_iff, ← IsNilpotent.map_iff (isEmptyRingEquiv R PEmpty).injective,
      -isEmptyRingEquiv_apply, isEmptyRingEquiv_eq_coeff_zero]
  · intro α _ H P
    obtain ⟨P, rfl⟩ := (optionEquivLeft _ _).symm.surjective P
    simp [IsNilpotent.map_iff (optionEquivLeft _ _).symm.injective,
      Polynomial.isNilpotent_iff, H, Finsupp.optionEquiv.forall_congr_left,
      ← optionEquivLeft_coeff_some_coeff_none, Finsupp.coe_update]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
refine_1 :
  ∀ (this : Fintype σ) (α β : Type u_1) [Fintype β] (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)
refine_2 :
  ∀ (this : Fintype σ) (x : MvPolynomial PEmpty.{u_1 + 1} R),
    IsNilpotent x ↔ ∀ (i : PEmpty.{u_1 + 1} →₀ ℕ), IsNilpotent (coeff i x)
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)
have refine_3 : ∀ (this : Fintype σ) (α : Type u_1) [Fintype α],
  (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
    ∀ (x : MvPolynomial.{u_1, u_2} (Option α) R), IsNilpotent x ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i x)
Tactic: classical
  -- Note: including `Fintype.ofFinite σ` in the entire context interferes with the `rw` below.
  refine have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P
  · intro α β _ e h₁ P
    rw [← IsNilpotent.map_iff (rename_injective _ e.symm.injective), h₁,
      (Finsupp.equivCongrLeft e).forall_congr_left]
    simp [Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective]
  · simp [Unique.forall_iff, ← IsNilpotent.map_iff (isEmptyRingEquiv R PEmpty).injective,
      -isEmptyRingEquiv_apply, isEmptyRingEquiv_eq_coeff_zero]
  · intro α _ H P
    obtain ⟨P, rfl⟩ := (optionEquivLeft _ _).symm.surjective P
    simp [IsNilpotent.map_iff (optionEquivLeft _ _).symm.injective,
      Polynomial.isNilpotent_iff, H, Finsupp.optionEquiv.forall_congr_left,
      ← optionEquivLeft_coeff_some_coeff_none, Finsupp.coe_update]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)
have obtain : ∀ (n : ℕ) (f : Fin n → σ) (hf : Function.Injective f) (P : MvPolynomial (Fin n) R),
  IsNilpotent (R := MvPolynomial σ R)
      ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P : MvPolynomial σ R) ↔
    ∀ (i : σ →₀ ℕ),
      IsNilpotent.{u_2} (R := R) (coeff i ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
Tactic: obtain ⟨n, f, hf, P, rfl⟩ := P.exists_fin_rename
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
f : Fin n → σ
hf : Function.Injective f
P : MvPolynomial (Fin n) R
⊢ IsNilpotent (R := MvPolynomial σ R)
      ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P : MvPolynomial σ R) ↔
    ∀ (i : σ →₀ ℕ),
      IsNilpotent.{u_2} (R := R) (coeff i ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
have rw : (∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)) ↔
  ∀ (i : σ →₀ ℕ), IsNilpotent.{u_2} (R := R) (coeff i ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
Tactic: rw [IsNilpotent.map_iff (rename_injective _ hf), MvPolynomial.isNilpotent_iff_of_fintype]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
f : Fin n → σ
hf : Function.Injective f
P : MvPolynomial (Fin n) R
⊢ (∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)) ↔
    ∀ (i : σ →₀ ℕ),
      IsNilpotent.{u_2} (R := R) (coeff i ((rename f : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
have lift : ∀ (f : Fin n ↪ σ),
  (∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)) ↔
    ∀ (i : σ →₀ ℕ),
      IsNilpotent.{u_2} (R := R)
        (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
Tactic: lift f to Fin n ↪ σ using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
⊢ (∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)) ↔
    ∀ (i : σ →₀ ℕ),
      IsNilpotent.{u_2} (R := R)
        (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
have refine : ∀ (H : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)) (i : σ →₀ ℕ),
  IsNilpotent.{u_2} (R := R)
    (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
Tactic: refine ⟨fun H i ↦ ?_, fun H i ↦ by simpa using H (i.embDomain f)⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
⊢ IsNilpotent.{u_2} (R := R)
    (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
have pos : ∀ (H : Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range (Finsupp.embDomain f)) i),
  IsNilpotent.{u_2} (R := R)
    (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
Tactic: by_cases H : i ∈ Set.range (Finsupp.embDomain f)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
pos :
  ∀ (H : Membership.mem (γ := Set (σ →₀ ℕ)) (Set.range (Finsupp.embDomain f)) i),
    IsNilpotent.{u_2} (R := R)
      (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
⊢ IsNilpotent.{u_2} (R := R)
    (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
have neg : ∀ (H : i ∉ Set.range (Finsupp.embDomain f)),
  IsNilpotent.{u_2} (R := R)
    (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
Tactic: by_cases H : i ∈ Set.range (Finsupp.embDomain f)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H_1 : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∉ Set.range (Finsupp.embDomain f)
⊢ IsNilpotent.{u_2} (R := R)
    (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
have neg : IsNilpotent.{u_2} (R := R) 0
Tactic: rw [coeff_rename_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H_1 : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∉ Set.range (Finsupp.embDomain f)
neg : IsNilpotent.{u_2} (R := R) 0
⊢ IsNilpotent.{u_2} (R := R)
    (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
have neg₁ : ∀ (u : Fin n →₀ ℕ), Finsupp.mapDomain (⇑f : (a : Fin n) → σ) u = i → coeff u P = 0
Tactic: rw [coeff_rename_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
have refine_1 : ∀ (H : IsUnit P) (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
Tactic: refine ⟨fun H ↦ ⟨H.map constantCoeff, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
refine_1 : ∀ (H : IsUnit P) (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
have refine_2 : (IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)) →
  ∀ (h₁ : IsUnit (coeff 0 P)) (h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)), IsUnit P
Tactic: refine ⟨fun H ↦ ⟨H.map constantCoeff, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
⊢ IsNilpotent (coeff n P)
have refine_1 : ∀ (i : σ) (hi : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), IsNilpotent (coeff n P)
Tactic: obtain ⟨i, hi⟩ : ∃ i, n i ≠ 0 := by simpa [Finsupp.ext_iff] using hn
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
e : Polynomial (MvPolynomial.{u_1, u_2} { b : σ // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R { b : σ // b ≠ i })) (renameEquiv R (Equiv.optionSubtypeNe i))
⊢ IsNilpotent (coeff n P)
have H₁ : IsNilpotent (R := MvPolynomial.{u_1, u_2} { b : σ // b ≠ i } R)
  (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // b ≠ i } R)) P)
    ((n : (a : σ) → ℕ) i))
Tactic: have H := (Polynomial.coeff_isUnit_isNilpotent_of_isUnit (H.map e.symm)).2 (n i) hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H_1 : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
e : Polynomial (MvPolynomial.{u_1, u_2} { b : σ // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R { b : σ // b ≠ i })) (renameEquiv R (Equiv.optionSubtypeNe i))
H :
  IsNilpotent (R := MvPolynomial.{u_1, u_2} { b : σ // b ≠ i } R)
    (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // b ≠ i } R)) P)
      ((n : (a : σ) → ℕ) i))
⊢ IsNilpotent (coeff n P)
have H₁ : ∀ (i_1 : { b : σ // ¬b = i } →₀ ℕ),
  IsNilpotent.{u_2} (R := R)
    (coeff i_1
      (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // ¬b = i } R)) P)
        ((n : (a : σ) → ℕ) i)))
Tactic: simp only [ne_eq, isNilpotent_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H_1 : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
e : Polynomial (MvPolynomial.{u_1, u_2} { b : σ // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R { b : σ // b ≠ i })) (renameEquiv R (Equiv.optionSubtypeNe i))
H :
  ∀ (i_1 : { b : σ // ¬b = i } →₀ ℕ),
    IsNilpotent.{u_2} (R := R)
      (coeff i_1
        (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // ¬b = i } R)) P)
          ((n : (a : σ) → ℕ) i)))
⊢ IsNilpotent (coeff n P)
have h : coeff (Finsupp.equivMapDomain (Equiv.optionSubtypeNe i).symm n).some
    (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // ¬b = i } R)) P)
      ((n : (a : σ) → ℕ) i)) =
  coeff n P
Tactic: convert! ← H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H_1 : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
e : Polynomial (MvPolynomial.{u_1, u_2} { b : σ // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (optionEquivLeft R { b : σ // b ≠ i })) (renameEquiv R (Equiv.optionSubtypeNe i))
H :
  ∀ (i_1 : { b : σ // ¬b = i } →₀ ℕ),
    IsNilpotent.{u_2} (R := R)
      (coeff i_1
        (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // ¬b = i } R)) P)
          ((n : (a : σ) → ℕ) i)))
⊢ coeff (Finsupp.equivMapDomain (Equiv.optionSubtypeNe i).symm n).some
      (Polynomial.coeff ((e.symm : (a : MvPolynomial σ R) → Polynomial (MvPolynomial { b : σ // ¬b = i } R)) P)
        ((n : (a : σ) → ℕ) i)) =
    coeff n P
have h : coeff (Finsupp.equivMapDomain (Equiv.optionSubtypeNe i).symm n)
    ((Equiv.symm
          (MulEquiv.toEquiv (RingEquiv.toMulEquiv (AlgEquiv.toRingEquiv (renameEquiv R (Equiv.optionSubtypeNe i))))) :
        (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ i }) R)
      P) =
  coeff n P
Tactic: refine (optionEquivLeft_coeff_some_coeff_none _ _ _ _).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
h : IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
h₁ : IsUnit (coeff 0 P)
h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ IsUnit P
have this : IsNilpotent (HSub.hSub (β := MvPolynomial σ R) P ((C : (a : R) → MvPolynomial σ R) (coeff 0 P) : MvPolynomial σ R))
Tactic: have : IsNilpotent (P - C (P.coeff 0)) := by
      simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
have refine_1 : ∀ (H : IsUnit P) (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
Tactic: classical
  refine ⟨fun H ↦ ⟨H.map constantCoeff, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · intro n hn
    obtain ⟨i, hi⟩ : ∃ i, n i ≠ 0 := by simpa [Finsupp.ext_iff] using hn
    let e := (optionEquivLeft _ _).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
    have H := (Polynomial.coeff_isUnit_isNilpotent_of_isUnit (H.map e.symm)).2 (n i) hi
    simp only [ne_eq, isNilpotent_iff] at H
    convert! ← H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some
    refine (optionEquivLeft_coeff_some_coeff_none _ _ _ _).trans ?_
    simp [Finsupp.equivMapDomain_eq_mapDomain,
      coeff_rename_mapDomain _ (Equiv.optionSubtypeNe i).symm.injective]
  · have : IsNilpotent (P - C (P.coeff 0)) := by
      simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]
    simpa using this.isUnit_add_right_of_commute (h₁.map C) (.all _ _)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
refine_1 : ∀ (H : IsUnit P) (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
have refine_2 : (IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)) →
  ∀ (h₁ : IsUnit (coeff 0 P)) (h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)), IsUnit P
Tactic: classical
  refine ⟨fun H ↦ ⟨H.map constantCoeff, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · intro n hn
    obtain ⟨i, hi⟩ : ∃ i, n i ≠ 0 := by simpa [Finsupp.ext_iff] using hn
    let e := (optionEquivLeft _ _).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
    have H := (Polynomial.coeff_isUnit_isNilpotent_of_isUnit (H.map e.symm)).2 (n i) hi
    simp only [ne_eq, isNilpotent_iff] at H
    convert! ← H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some
    refine (optionEquivLeft_coeff_some_coeff_none _ _ _ _).trans ?_
    simp [Finsupp.equivMapDomain_eq_mapDomain,
      coeff_rename_mapDomain _ (Equiv.optionSubtypeNe i).symm.injective]
  · have : IsNilpotent (P - C (P.coeff 0)) := by
      simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]
    simpa using this.isUnit_add_right_of_commute (h₁.map C) (.all _ _)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ P.totalDegree = 0
have h : P.totalDegree = 0 ↔ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
Tactic: convert! isUnit_iff (P := P)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
⊢ P.totalDegree = 0 ↔ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
have h : (∀ m ∈ P.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)) ↔
  ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
Tactic: rw [totalDegree_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
⊢ IsUnit P ↔ ∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r
have rw : IsUnit (coeff 0 P) ∧ P = (C : (a : R) → MvPolynomial σ R) (coeff 0 P) ↔
  ∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r
Tactic: rw [isUnit_iff_totalDegree_of_isReduced, totalDegree_eq_zero_iff_eq_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Nilpotent (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
⊢ IsUnit (coeff 0 P) ∧ P = (C : (a : R) → MvPolynomial σ R) (coeff 0 P) ↔
    ∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r
have refine : (∃ (r : R), IsUnit r ∧ P = (C : (a : R) → MvPolynomial σ R) r) →
  IsUnit (coeff 0 P) ∧ P = (C : (a : R) → MvPolynomial σ R) (coeff 0 P)
Tactic: refine ⟨fun H ↦ ⟨_, H⟩, ?_⟩