awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H1 :
  r.degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)
H2 :
  HPow.hPow (α := A⟦X⟧) X
      (order.{u_1} (R := IsLocalRing.ResidueField A)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat =
    g * q + (↑r : A⟦X⟧)
H1₁ :
  let n :=
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat;
  r.degree < (↑n : WithBot ℕ)
⊢ let n :=
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat;
  HPow.hPow (α := A⟦X⟧) X n = g * q + (↑r : A⟦X⟧)

Tactic:
set n := (g.map (IsLocalRing.residue A)).order.toNat

Premises used: IsLocalRing.residue, PowerSeries.map, PowerSeries.order, ENat.toNat, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 : HPow.hPow (α := A⟦X⟧) X n = g * q + (↑r : A⟦X⟧)
⊢ Eq (α := IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (HPow.hPow (α := A⟦X⟧) X n)) :
      IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * q + (↑r : A⟦X⟧))) :
      IsLocalRing.ResidueField A)

Tactic:
replace H2 := congr(coeff n (($H2).map (IsLocalRing.residue A)))
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq (α := IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (HPow.hPow (α := A⟦X⟧) X n)) :
      IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * q + (↑r : A⟦X⟧))) :
      IsLocalRing.ResidueField A)
⊢ Eq (α := IsLocalRing.ResidueField A) (1 : IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        (HMul.hMul (α := (IsLocalRing.ResidueField A)⟦X⟧) (β := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q :
            (IsLocalRing.ResidueField A)⟦X⟧)) :
      IsLocalRing.ResidueField A)

Tactic:
simp_rw [map_pow, map_X, coeff_X_pow_self, map_add, map_mul, coeff_map,
    Polynomial.coeff_coe, Polynomial.coeff_eq_zero_of_degree_lt H1, map_zero, add_zero] at H2

Premises used: map_zero, map_add, map_pow, PowerSeries.map_X, map_mul, PowerSeries.coeff_map, PowerSeries.coeff_X_pow_self, add_zero, Polynomial.coeff_coe, Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq (α := IsLocalRing.ResidueField A) (1 : IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        (HMul.hMul (α := (IsLocalRing.ResidueField A)⟦X⟧) (β := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q :
            (IsLocalRing.ResidueField A)⟦X⟧)) :
      IsLocalRing.ResidueField A)
rw :
  IsUnit (M := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
      IsLocalRing.ResidueField A)
⊢ IsUnit q

Tactic:
rw [isUnit_iff_constantCoeff, ← isUnit_map_iff (IsLocalRing.residue A)]

Premises used: PowerSeries.isUnit_iff_constantCoeff, IsLocalRing.residue, isUnit_map_iff
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
⊢ {(n, 0)} ⊆ @Finset.antidiagonal _ Nat.instAddMonoid _ n

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  1 =
    HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
      ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
        IsLocalRing.ResidueField A)
      ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((coeff (n, 0).1 : (a : A⟦X⟧) → A) g) :
        IsLocalRing.ResidueField A)
⊢ IsUnit (M := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
      IsLocalRing.ResidueField A)

Tactic:
.of_mul_eq_one _ H2.symm

Premises used: IsUnit.of_mul_eq_one, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  1 =
    HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
      ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
        IsLocalRing.ResidueField A)
      ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((coeff (n, 0).1 : (a : A⟦X⟧) → A) g) :
        IsLocalRing.ResidueField A)
⊢ IsUnit (M := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
      IsLocalRing.ResidueField A)

Tactic:
exact .of_mul_eq_one _ H2.symm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p ∉ {(n, 0)}
rw :
  HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A) (0 : IsLocalRing.ResidueField A)
      ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
        IsLocalRing.ResidueField A) =
    0
rw₁ :
  (↑p.1 : ℕ∞) <
    order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)
⊢ HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
      ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
        IsLocalRing.ResidueField A)
      ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
        IsLocalRing.ResidueField A) =
    0

Tactic:
rw [coeff_of_lt_order p.1 ?_]

Premises used: PowerSeries.coeff_of_lt_order, Prod.fst
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p ∉ {(n, 0)}
rw rw₁ : Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 0 0
⊢ HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A) (0 : IsLocalRing.ResidueField A)
      ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
        IsLocalRing.ResidueField A) =
    0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p ∉ {(n, 0)}
rw :
  p.1 <
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
⊢ (↑p.1 : ℕ∞) <
    order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)

Tactic:
rw [← ENat.lt_lift_iff (h := order_finite_iff_ne_zero.2 hg), ENat.lift_eq_toNat_of_lt_top]

Premises used: ENat.lt_lift_iff, ENat.lift_eq_toNat_of_lt_top
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p ∉ {(n, 0)}
⊢ p.1 <
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat

Tactic:
(Finset.antidiagonal.fst_le hp).lt_of_ne ?_

Premises used: LE.le.lt_of_ne, Finset.antidiagonal.fst_le
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p ∉ {(n, 0)}
refine : p.1 ≠ n
⊢ p.1 <
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat

Tactic:
refine (Finset.antidiagonal.fst_le hp).lt_of_ne ?_

Premises used: LE.le.lt_of_ne, Finset.antidiagonal.fst_le
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p ∉ {(n, 0)}
contrapose : ∀ (hnotMem : p.1 = n), Membership.mem (γ := Finset (ℕ × ℕ)) {(n, 0)} p
⊢ p.1 ≠ n

Tactic:
contrapose hnotMem
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p.1 = n
⊢ (n, 0) ∈ @Finset.antidiagonal _ AddRightCancelMonoid.toAddMonoid _ n

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p.1 = n
rwa : p = (n, 0)
rwa₁ rwa₂ rwa₃ rwa₄ : p.1 = (n, 0).1
⊢ Membership.mem (γ := Finset (ℕ × ℕ)) {(n, 0)} p

Tactic:
rwa [Finset.mem_singleton, Finset.antidiagonal_congr hp (by simp)]

Premises used: Finset.mem_singleton, Finset.antidiagonal_congr
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
⊢ r.degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)

Tactic:
have H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat := H.1