awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
⊢ ∀ {α β : Type u_6} (f : MvPolynomial.{u_6, u_3} (α → β) R) (x : MvPolynomial α R),
    Eq (α := MvPolynomial β R)
      (do
        let x_1 ← f
        Functor.map (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) x_1 x : MvPolynomial β R)
      (f <*> x : MvPolynomial β R)

Tactic:
aesop
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β : Type u_6
x : α
f_1 : α → MvPolynomial β R
⊢ bind (m := fun (σ : Type u_6) ↦ MvPolynomial σ R) (pure (f := fun (σ : Type u_6) ↦ MvPolynomial σ R) x) f_1 = f_1 x

Tactic:
simp [pure, bind]

Premises used: Pure.pure, Bind.bind
-- Module: Mathlib.Algebra.MvPolynomial.Monad
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
f : σ → MvPolynomial τ R
α β γ : Type u_6
x : MvPolynomial α R
f_1 : α → MvPolynomial β R
g : β → MvPolynomial γ R
⊢ Eq (α := MvPolynomial γ R)
    (bind (m := fun (σ : Type u_6) ↦ MvPolynomial σ R) (bind (m := fun (σ : Type u_6) ↦ MvPolynomial σ R) x f_1) g :
      MvPolynomial γ R)
    (bind (m := fun (σ : Type u_6) ↦ MvPolynomial σ R) (β := γ) x fun (x : α) ↦
        bind (m := fun (σ : Type u_6) ↦ MvPolynomial σ R) (f_1 x) g :
      MvPolynomial γ R)

Tactic:
simp [bind, ← bind₁_comp_bind₁]

Premises used: MvPolynomial.bind₁_comp_bind₁, Bind.bind
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P

Premises used: Fintype.ofFinite, Fintype.induction_empty_option
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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)
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)
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
refine have := Fintype.ofFinite σ; Fintype.induction_empty_option ?_ ?_ ?_ σ P

Premises used: Fintype.ofFinite
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
this : Fintype σ
α β : Type u_1
refine_1 :
  ∀ [Fintype β] (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)
⊢ ∀ [Fintype β] (e : α ≃ β),
    (∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)) →
      ∀ (x : MvPolynomial β R), IsNilpotent x ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i x)

Tactic:
_
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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
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)
⊢ IsNilpotent P ↔ ∀ (i : β →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
rw [← IsNilpotent.map_iff (rename_injective _ e.symm.injective), h₁,
      (Finsupp.equivCongrLeft e).forall_congr_left]

Premises used: Equiv.forall_congr_left, MvPolynomial.rename_injective, IsNilpotent.map_iff, Equiv.injective, Equiv.symm, Finsupp.equivCongrLeft
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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
⊢ (∀ (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:
simp [Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _ e.symm.injective]

Premises used: MvPolynomial.coeff_rename_mapDomain, Finsupp.equivMapDomain_eq_mapDomain, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
this : Fintype σ
⊢ ∀ (x : MvPolynomial PEmpty.{u_1 + 1} R), IsNilpotent x ↔ ∀ (i : PEmpty.{u_1 + 1} →₀ ℕ), IsNilpotent (coeff i x)

Tactic:
simp [Unique.forall_iff, ← IsNilpotent.map_iff (isEmptyRingEquiv R PEmpty).injective,
      -isEmptyRingEquiv_apply, isEmptyRingEquiv_eq_coeff_zero]

Premises used: MvPolynomial.isEmptyRingEquiv_apply, RingEquiv.injective, PEmpty, Unique.forall_iff, IsNilpotent.map_iff, MvPolynomial.isEmptyRingEquiv, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : Finite σ
this : Fintype σ
α : Type u_1
refine_3 :
  ∀ [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)
⊢ ∀ [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:
_
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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
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))
⊢ IsNilpotent P ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
obtain ⟨P, rfl⟩ := (optionEquivLeft _ _).symm.surjective P

Premises used: AlgEquiv.symm, MvPolynomial.optionEquivLeft, AlgEquiv.surjective, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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 : 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:
simp [IsNilpotent.map_iff (optionEquivLeft _ _).symm.injective,
      Polynomial.isNilpotent_iff, H, Finsupp.optionEquiv.forall_congr_left,
      ← optionEquivLeft_coeff_some_coeff_none, Finsupp.coe_update]

Premises used: AlgEquiv.symm, Equiv.forall_congr_left, Finsupp.optionEquiv, Finsupp.coe_update, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, Polynomial.isNilpotent_iff, IsNilpotent.map_iff, AlgEquiv.injective, MvPolynomial.optionEquivLeft
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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)
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)
refine_2₁ :
  ∀ (this : Fintype σ) (x : MvPolynomial PEmpty.{u_1 + 1} R),
    IsNilpotent x ↔ ∀ (i : PEmpty.{u_1 + 1} →₀ ℕ), IsNilpotent (coeff i x)
refine_3₁ 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)
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)

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]

Premises used: MvPolynomial.isEmptyRingEquiv_apply, Fintype.ofFinite, AlgEquiv.symm, Equiv.forall_congr_left, RingEquiv.injective, Finsupp.optionEquiv, PEmpty, Unique.forall_iff, Finsupp.coe_update, Finsupp.equivMapDomain_eq_mapDomain, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, Polynomial.isNilpotent_iff, IsNilpotent.map_iff, AlgEquiv.injective, MvPolynomial.optionEquivLeft, MvPolynomial.isEmptyRingEquiv, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, AlgEquiv.surjective, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
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))
⊢ IsNilpotent P ↔ ∀ (i : σ →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
obtain ⟨n, f, hf, P, rfl⟩ := P.exists_fin_rename

Premises used: MvPolynomial.exists_fin_rename, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
f : Fin n → σ
hf : Function.Injective f
P : MvPolynomial (Fin n) R
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))
⊢ 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:
rw [IsNilpotent.map_iff (rename_injective _ hf), MvPolynomial.isNilpotent_iff_of_fintype]

Premises used: _private.0.MvPolynomial.isNilpotent_iff_of_fintype, MvPolynomial.rename_injective, IsNilpotent.map_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
f : Fin n → σ
hf : Function.Injective f
P : MvPolynomial (Fin n) R
⊢ Function.Injective f

Tactic:
hf
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
f : Fin n → σ
hf : Function.Injective f
P : MvPolynomial (Fin n) R
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))
⊢ (∀ (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:
lift f to Fin n ↪ σ using hf

Premises used: Fin
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H :
  ∀ (i : σ →₀ ℕ),
    IsNilpotent.{u_2} (R := R)
      (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))
i : Fin n →₀ ℕ
⊢ IsNilpotent (coeff i P)

Tactic:
simpa using H (i.embDomain f)

Premises used: Finsupp.embDomain
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
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))
⊢ (∀ (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)⟩
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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))
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))
⊢ 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)

Premises used: Finsupp.embDomain, Set.range
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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 : 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:
aesop
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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
neg₁ : ∀ (u : Fin n →₀ ℕ), Finsupp.mapDomain (⇑f : (a : Fin n) → σ) u = i → coeff u P = 0
⊢ IsNilpotent.{u_2} (R := R)
    (coeff i ((rename (⇑f : (a : Fin n) → σ) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) P))

Tactic:
rw [coeff_rename_eq_zero]

Premises used: MvPolynomial.coeff_rename_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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) 0

Tactic:
aesop (add simp Finsupp.embDomain_eq_mapDomain)

Premises used: Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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)
⊢ ∀ (u : Fin n →₀ ℕ), Finsupp.mapDomain (⇑f : (a : Fin n) → σ) u = i → coeff u P = 0

Tactic:
aesop (add simp Finsupp.embDomain_eq_mapDomain)

Premises used: Finsupp.embDomain_eq_mapDomain
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
inst_1 : IsReduced R
⊢ IsReduced (MvPolynomial σ R)

Tactic:
simp [isReduced_iff, isNilpotent_iff, MvPolynomial.ext_iff]

Premises used: isReduced_iff, MvPolynomial.ext_iff, MvPolynomial.isNilpotent_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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)

Tactic:
⟨fun H ↦ ⟨H.map constantCoeff, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩

Premises used: _private.0.MvPolynomial.isUnit_iff.match_1, IsUnit, And.intro, Iff.intro, IsUnit.map, MvPolynomial.constantCoeff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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)
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
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)

Tactic:
refine ⟨fun H ↦ ⟨H.map constantCoeff, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
⊢ ∃ (i : σ), Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
simpa [Finsupp.ext_iff] using hn

Premises used: Finsupp.ext_iff
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
P : MvPolynomial σ R
H : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
refine_1 : ∀ (i : σ) (hi : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), IsNilpotent (coeff n P)
⊢ IsNilpotent (coeff n P)

Tactic:
obtain ⟨i, hi⟩ : ∃ i, n i ≠ 0 := by simpa [Finsupp.ext_iff] using hn
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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 (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
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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))
⊢ ∀ (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

Premises used: MvPolynomial.isNilpotent_iff, ne_eq
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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.{u_2} (R := R)
    (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)))

Tactic:
H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some

Premises used: Finsupp.some, Finsupp.equivMapDomain, Equiv.optionSubtypeNe, Equiv.symm
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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)))
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
⊢ IsNilpotent (coeff n P)

Tactic:
convert! ← H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some

Premises used: Finsupp.some, Finsupp.equivMapDomain, Equiv.optionSubtypeNe, Equiv.symm
-- Module: Mathlib.Algebra.MvPolynomial.Nilpotent
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

Tactic:
(optionEquivLeft_coeff_some_coeff_none _ _ _ _).trans ?_

Premises used: Multiset.sum, Multiset.foldr, Option.casesOn', Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, Finset.sum, Eq.trans