awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
φ : MvPowerSeries σ R
⊢ IsUnit φ ∨ IsUnit (1 - φ)
have inl : ∀ (u : Rˣ) (h : (↑u : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ), IsUnit φ
Tactic: obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ) <;>
        [left; right]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
φ : MvPowerSeries σ R
inl : ∀ (u : Rˣ) (h : (↑u : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ), IsUnit φ
⊢ IsUnit φ ∨ IsUnit (1 - φ)
have inr : ∀ (u : Rˣ) (h : (↑u : R) = HSub.hSub (α := R) (β := R) (1 : R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)),
  IsUnit (1 - φ)
Tactic: obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ) <;>
        [left; right]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : (↑u : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ
⊢ IsUnit φ
have inl : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
Tactic: refine .of_mul_eq_one _ (mul_invOfUnit _ u ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : (↑u : R) = HSub.hSub (α := R) (β := R) (1 : R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
⊢ IsUnit (1 - φ)
have inr : (constantCoeff : (a : MvPowerSeries σ R) → R) (1 - φ) = (↑u : R)
Tactic: refine .of_mul_eq_one _ (mul_invOfUnit _ u ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (↑ψ : MvPowerSeries σ S) = (map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ
⊢ IsUnit φ
have h₁ : Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
  ((constantCoeff : (a : MvPowerSeries σ S) → S)
      ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
    S)
Tactic: replace h := congr_arg constantCoeff h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((constantCoeff : (a : MvPowerSeries σ S) → S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
      S)
⊢ IsUnit φ
have h₁ : Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
  ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
Tactic: rw [constantCoeff_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
⊢ IsUnit φ
have this : IsUnit.{u_3} (M := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
Tactic: have : IsUnit (constantCoeff ψ.val) := isUnit_constantCoeff _ ψ.isUnit
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
this : IsUnit.{u_3} (M := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
⊢ IsUnit φ
have this₁ : IsUnit.{u_3} (M := S) ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
this : IsUnit.{u_3} (M := S) ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
⊢ IsUnit φ
have rcases : ∀ (c : Rˣ) (hc : (↑c : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ), IsUnit φ
Tactic: rcases isUnit_of_map_unit f _ this with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
have rw : Eq.{u_3 + 1} (α := k) ((coeff 0 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
  (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
rw :
  Eq.{u_3 + 1} (α := k) ((coeff 0 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
have rw₁ : Eq.{u_3 + 1} (α := k)
  (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
    else
      HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
        (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
            if x.2 < 0 then
              HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
            else 0 :
          k) :
    k)
  (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
rw :
  Eq.{u_3 + 1} (α := k) ((coeff 0 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
rw₁ :
  Eq.{u_3 + 1} (α := k)
    (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
              if x.2 < 0 then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
have rw₂ : Eq.{u_3 + 1} (α := k) (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
  (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
have rw : Eq.{u_3 + 1} (α := k) ((coeff 0 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
  (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
Tactic: classical
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
rw :
  Eq.{u_3 + 1} (α := k) ((coeff 0 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
have rw₁ : Eq.{u_3 + 1} (α := k)
  (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
    else
      HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
        (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
            if x.2 < 0 then
              HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
            else 0 :
          k) :
    k)
  (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
Tactic: classical
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
rw :
  Eq.{u_3 + 1} (α := k) ((coeff 0 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
rw₁ :
  Eq.{u_3 + 1} (α := k)
    (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
              if x.2 < 0 then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
have rw₂ : Eq.{u_3 + 1} (α := k) (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
  (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
Tactic: classical
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := k) ((coeff n : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
have rw : Eq.{u_3 + 1} (α := k)
  (if n = 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
    else
      HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
        (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
            if x.2 < n then
              HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
            else 0 :
          k) :
    k)
  ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
Tactic: rw [coeff_inv]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := k)
    (if n = 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
have pos : n = 0 →
  Eq.{u_3 + 1} (α := k) (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
pos :
  n = 0 →
    Eq.{u_3 + 1} (α := k) (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
      ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
⊢ Eq.{u_3 + 1} (α := k)
    (if n = 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
have neg : ¬n = 0 →
  HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
      (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
              ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
          else 0 :
        k) =
    (coeff n : (a : MvPowerSeries σ k) → k) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := k) ((coeff n : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
have rw : Eq.{u_3 + 1} (α := k)
  (if n = 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
    else
      HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
        (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
            if x.2 < n then
              HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
            else 0 :
          k) :
    k)
  ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
Tactic: classical
      rw [coeff_inv]
      split_ifs <;>
        simp only [h, map_zero, zero_mul, inv_zero, neg_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
⊢ Eq (α := MvPowerSeries σ k) 0⁻¹ 0
have rw : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) 0 : k) (0 : k)
Tactic: rw [inv_eq_zero, constantCoeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
rw : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) 0 : k) (0 : k)
⊢ Eq (α := MvPowerSeries σ k) 0⁻¹ 0
have rw₁ : Eq.{u_3 + 1} (α := k) 0 0
Tactic: rw [inv_eq_zero, constantCoeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff : (a : MvPowerSeries σ k) → k) φ = (↑u : k)
⊢ φ.invOfUnit u = φ⁻¹
have rw : φ.invOfUnit u = φ.invOfUnit (Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) sorry)
Tactic: rw [← invOfUnit_eq φ (h.symm ▸ u.ne_zero)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff : (a : MvPowerSeries σ k) → k) φ = (↑u : k)
⊢ φ.invOfUnit u = φ.invOfUnit (Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯)
have apply : u = Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) sorry
Tactic: apply congrArg (invOfUnit φ)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
u : kˣ
h : (constantCoeff : (a : MvPowerSeries σ k) → k) φ = (↑u : k)
⊢ u = Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) ⋯
have rw : (↑u : k) = (↑(Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) sorry) : k)
Tactic: rw [Units.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
⊢ φ * φ⁻¹ = 1
have rw : φ * φ.invOfUnit (Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) h) = 1
Tactic: rw [← invOfUnit_eq φ h, mul_invOfUnit φ (Units.mk0 _ h) rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
rw : φ * φ.invOfUnit (Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) h) = 1
⊢ φ * φ⁻¹ = 1
have rw₁ : Eq (α := MvPowerSeries σ k) 1 1
Tactic: rw [← invOfUnit_eq φ h, mul_invOfUnit φ (Units.mk0 _ h) rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
⊢ φ⁻¹ * φ = 1
have rw : φ * φ⁻¹ = 1
Tactic: rw [mul_comm, φ.mul_inv_cancel h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
rw : φ * φ⁻¹ = 1
⊢ φ⁻¹ * φ = 1
have rw₁ : Eq (α := MvPowerSeries σ k) 1 1
Tactic: rw [mul_comm, φ.mul_inv_cancel h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
⊢ φ = ψ⁻¹ ↔ φ * ψ = 1
have rw : φ = ψ⁻¹ ↔ φ = 1 * ψ⁻¹
Tactic: rw [← MvPowerSeries.eq_mul_inv_iff_mul_eq h, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
rw : φ = ψ⁻¹ ↔ φ = 1 * ψ⁻¹
⊢ φ = ψ⁻¹ ↔ φ * ψ = 1
have rw₁ : φ = ψ⁻¹ ↔ φ = ψ⁻¹
Tactic: rw [← MvPowerSeries.eq_mul_inv_iff_mul_eq h, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
⊢ ψ⁻¹ = φ ↔ φ * ψ = 1
have rw : φ = ψ⁻¹ ↔ φ * ψ = 1
Tactic: rw [eq_comm, MvPowerSeries.eq_inv_iff_mul_eq_one h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
rw : φ = ψ⁻¹ ↔ φ * ψ = 1
⊢ ψ⁻¹ = φ ↔ φ * ψ = 1
have rw₁ : φ * ψ = 1 ↔ φ * ψ = 1
Tactic: rw [eq_comm, MvPowerSeries.eq_inv_iff_mul_eq_one h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
have pos : ∀ (h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)), (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
Tactic: by_cases h : constantCoeff (φ * ψ) = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
pos :
  ∀ (h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)),
    (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
have neg : ∀ (h : ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)),
  (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
Tactic: by_cases h : constantCoeff (φ * ψ) = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
have pos : 0 = ψ⁻¹ * φ⁻¹
Tactic: rw [inv_eq_zero.mpr h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (hypothesis)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)
⊢ 0 = ψ⁻¹ * φ⁻¹
have h₁ : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∨
  Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
Tactic: simp only [map_mul, mul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h :
  Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∨
    Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
⊢ 0 = ψ⁻¹ * φ⁻¹
have pos : ∀ (h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)), 0 = ψ⁻¹ * φ⁻¹
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h :
  Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∨
    Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
pos : ∀ (h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)), 0 = ψ⁻¹ * φ⁻¹
⊢ 0 = ψ⁻¹ * φ⁻¹
have pos₁ : ∀ (h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)), 0 = ψ⁻¹ * φ⁻¹
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
have neg : ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
Tactic: rw [MvPowerSeries.inv_eq_iff_mul_eq_one h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (hypothesis)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h : ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) (φ * ψ) : k) (0 : k)
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
have h₁ : ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∧
  ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
Tactic: simp only [not_or, map_mul, mul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ ψ : MvPowerSeries σ k
h :
  ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k) ∧
    ¬Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) ψ : k) (0 : k)
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
have neg : ψ⁻¹ * φ⁻¹ * φ * ψ = 1
Tactic: rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
      MvPowerSeries.inv_mul_cancel _ h.right]