awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
inst_2 : IsPrincipalIdealRing R
inst_3 : IsDomain R
w : R
w_1 : Set R⟦X⟧
h₁ : Ne (α := Ideal R⟦X⟧) (span w_1) ⊥
h₂ : IsPrime (span w_1)
hXP : X ∉ span w_1
h_1 : Eq (α := Submodule R R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span w_1)) (R ∙ w)
left : w_1.Finite
h : w_1.ncard = ncard (α := R) {w}
⊢ ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span w_1) x ∧ Prime x
have h₃ : ∃ (a : R⟦X⟧), w_1 = {a}
Tactic: simp only [ncard_singleton, ncard_eq_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R⟦X⟧
S : Set R
P : Ideal R⟦X⟧
inst_1 : P.IsPrime
inst_2 : IsPrincipalIdealRing R
inst_3 : IsDomain R
w : R
w_1 : Set R⟦X⟧
h₁ : Ne (α := Ideal R⟦X⟧) (span w_1) ⊥
h₂ : IsPrime (span w_1)
hXP : X ∉ span w_1
h_1 : Eq (α := Submodule R R) (Ideal.map (F := R⟦X⟧ →+* R) constantCoeff (span w_1)) (R ∙ w)
left : w_1.Finite
h : ∃ (a : R⟦X⟧), w_1 = {a}
⊢ ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span w_1) x ∧ Prime x
have neg : ∀ (w_2 : R⟦X⟧) (h₁ : Ne (α := Ideal R⟦X⟧) (span {w_2}) ⊥) (h₂ : IsPrime (α := R⟦X⟧) (span {w_2})) (hXP : X ∉ span {w_2})
  (h : Eq (α := Submodule R R) (Ideal.map (R := R⟦X⟧) (F := R⟦X⟧ →+* R) constantCoeff (span {w_2})) (R ∙ w)),
  Set.Finite (α := R⟦X⟧) {w_2} → ∃ (x : R⟦X⟧), Membership.mem (γ := Ideal R⟦X⟧) (span {w_2}) x ∧ Prime x
Tactic: obtain ⟨_, rfl⟩ := h
Cleared hypotheses: w_1, h₁, h₂, hXP, h_1, left, h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (coeff n : (a : R⟦X⟧) → R) (inv.aux a φ) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (inv.aux a φ) : R)
          else 0
have rw : (if Eq (α := Unit →₀ ℕ) (single () n) 0 then a
  else
    -a *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
        if x.2 < single () n then
          HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
            ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0) =
  if n = 0 then a
  else
    -a *
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        if x.2 < n then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
            ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0
Tactic: rw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (if Eq (α := Unit →₀ ℕ) (single () n) 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
          if x.2 < single () n then
            HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
              ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0
have simp : (if n = 0 then a
  else
    -a *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
        if x.2 < single () n then
          HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
            ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0) =
  if n = 0 then a
  else
    -a *
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        if x.2 < n then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
            ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0
Tactic: simp only [Finsupp.single_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
          if x.2 < single () n then
            HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
              ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0
have pos : n = 0 → a = a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
pos : n = 0 → a = a
⊢ (if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
          if x.2 < single () n then
            HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
              ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
          else 0
have neg : ¬n = 0 →
  (-a *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
        if x.2 < single () n then
          HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
            ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0) =
    -a *
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        if x.2 < n then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
            ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
⊢ (-a *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
        if x.2 < single () n then
          HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
            ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0) =
    -a *
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        if x.2 < n then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
            ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
        else 0
have neg : Eq.{u_1 + 1} (α := R)
  (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
    if x.2 < single () n then
      HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
        ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    if x.2 < n then
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
have neg : Eq.{u_1 + 1} (α := R)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    if x.2 < n then
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0)
  (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
    if x.2 < single () n then
      HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
        ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
have neg : ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  Membership.mem (α := (Unit →₀ ℕ) × (Unit →₀ ℕ)) (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ)))
    (@antidiagonal _ Finsupp.instAddMonoid _ (single () n))
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
      | (a, b) => (single () a, single () b) :
      (Unit →₀ ℕ) × (Unit →₀ ℕ))
Tactic: apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b))
    fun (f, g) ↦ (f (), g ())
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
neg :
  ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    Membership.mem (α := (Unit →₀ ℕ) × (Unit →₀ ℕ)) (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ)))
      (@antidiagonal _ Finsupp.instAddMonoid _ (single () n))
      (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
        | (a, b) => (single () a, single () b) :
        (Unit →₀ ℕ) × (Unit →₀ ℕ))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
have neg₁ : ∀ (a : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
  Membership.mem (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ))) (@antidiagonal _ Finsupp.instAddMonoid _ (single () n)) a →
    Membership.mem (α := ℕ × ℕ) (@antidiagonal _ Nat.instAddMonoid _ n)
      (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ) a with
        | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ()) :
        ℕ × ℕ)
Tactic: apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b))
    fun (f, g) ↦ (f (), g ())
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
neg :
  ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    Membership.mem (α := (Unit →₀ ℕ) × (Unit →₀ ℕ)) (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ)))
      (@antidiagonal _ Finsupp.instAddMonoid _ (single () n))
      (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
        | (a, b) => (single () a, single () b) :
        (Unit →₀ ℕ) × (Unit →₀ ℕ))
neg₁ :
  ∀ (a : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    Membership.mem (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ))) (@antidiagonal _ Finsupp.instAddMonoid _ (single () n)) a →
      Membership.mem (α := ℕ × ℕ) (@antidiagonal _ Nat.instAddMonoid _ n)
        (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ) a with
          | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ()) :
          ℕ × ℕ)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
have neg₂ : ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ)
      match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
      | (a, b) => (single () a, single () b) with
    | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ())) =
    a
Tactic: apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b))
    fun (f, g) ↦ (f (), g ())
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
neg :
  ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    Membership.mem (α := (Unit →₀ ℕ) × (Unit →₀ ℕ)) (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ)))
      (@antidiagonal _ Finsupp.instAddMonoid _ (single () n))
      (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
        | (a, b) => (single () a, single () b) :
        (Unit →₀ ℕ) × (Unit →₀ ℕ))
neg₁ :
  ∀ (a : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    Membership.mem (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ))) (@antidiagonal _ Finsupp.instAddMonoid _ (single () n)) a →
      Membership.mem (α := ℕ × ℕ) (@antidiagonal _ Nat.instAddMonoid _ n)
        (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ) a with
          | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ()) :
          ℕ × ℕ)
neg₂ :
  ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ)
        match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ())) =
      a
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
have neg₃ : ∀ (a : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
  Membership.mem (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ))) (@antidiagonal _ Finsupp.instAddMonoid _ (single () n)) a →
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ))
        match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ) a with
        | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ()) with
      | (a, b) => (single () a, single () b)) =
      a
Tactic: apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b))
    fun (f, g) ↦ (f (), g ())
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0
have neg : ∀ (H : n ≤ j),
  (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0
Tactic: obtain H | H := le_or_gt n j
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
neg :
  ∀ (H : n ≤ j),
    (if (i, j).2 < n then
        HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0) =
      if
          LT.lt (α := Unit →₀ ℕ)
            (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
              | (a, b) => (single () a, single () b)).2
            (single () n) then
        HMul.hMul (α := R) (β := R)
          ((MvPowerSeries.coeff
                  (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                    | (a, b) => (single () a, single () b)).1 :
                (a : MvPowerSeries Unit R) → R)
              φ :
            R)
          ((MvPowerSeries.coeff
                  (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                    | (a, b) => (single () a, single () b)).2 :
                (a : MvPowerSeries Unit R) → R)
              (MvPowerSeries.inv.aux a φ) :
            R)
      else 0
⊢ (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0
have neg₁ : ∀ (H : j < n),
  (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0
Tactic: obtain H | H := le_or_gt n j
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
⊢ (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0
have neg : HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
    ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R) =
  HMul.hMul (α := R) (β := R)
    ((MvPowerSeries.coeff
            (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
              | (a, b) => (single () a, single () b)).1 :
          (a : MvPowerSeries Unit R) → R)
        φ :
      R)
    ((MvPowerSeries.coeff
            (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
              | (a, b) => (single () a, single () b)).2 :
          (a : MvPowerSeries Unit R) → R)
        (MvPowerSeries.inv.aux a φ) :
      R)
Tactic: rw [if_pos H, if_pos]