mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ False

Tactic:
·

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w p) f = 0
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit φ → IsUnit (constantCoeff φ)

pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit (constantCoeff φ) → IsUnit φ

Tactic:
·

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit φ → IsUnit (constantCoeff φ)
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit (constantCoeff φ) → IsUnit φ

Tactic:
·

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit (constantCoeff φ) → IsUnit φ
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ False

Tactic:
·

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
H : (weightedHomogeneousComponent w q) g = 0
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = constantCoeff φ
⊢ IsUnit φ

Tactic:
·

Goal state after:
case inl
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = constantCoeff φ
⊢ IsUnit φ
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = 1 - constantCoeff φ
⊢ IsUnit (1 - φ)

Tactic:
·

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : ↑u = 1 - constantCoeff φ
⊢ IsUnit (1 - φ)
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case inl
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : v x ≠ 0 ∧ v x ≠ 1
h : v x ≤ 1
⊢ ∃ x, 1 < ‖x‖

pp: case inr
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : v x ≠ 0 ∧ v x ≠ 1
h : v x⁻¹ ≤ 1
⊢ ∃ x, 1 < ‖x‖

Tactic:
·

Goal state after:
case inl
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : v x ≠ 0 ∧ v x ≠ 1
h : v x ≤ 1
⊢ ∃ x, 1 < ‖x‖
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case inr
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : v x ≠ 0 ∧ v x ≠ 1
h : v x⁻¹ ≤ 1
⊢ ∃ x, 1 < ‖x‖

Tactic:
·

Goal state after:
case inr
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : v x ≠ 0 ∧ v x ≠ 1
h : v x⁻¹ ≤ 1
⊢ ∃ x, 1 < ‖x‖
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

pp: case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
·

Goal state after:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
·

Goal state after:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬constantCoeff (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : ¬weightedOrder w g < ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
·

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : ¬weightedOrder w g < ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (Ideal.span {X}).IsPrime

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X ≠ 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (Ideal.span {X}).IsPrime
Module: Mathlib.RingTheory.PowerSeries.NoZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X ≠ 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : ¬weightedOrder w f < ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g

Tactic:
·

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : ¬weightedOrder w f < ⊤
⊢ weightedOrder w (f * g) ≤ weightedOrder w f + weightedOrder w g
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case inl
σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ (C 0)⁻¹ = C 0⁻¹

pp: case inr
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ (C r)⁻¹ = C r⁻¹

Tactic:
·

Goal state after:
case inl
σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ (C 0)⁻¹ = C 0⁻¹
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : n = 0
⊢ a = a

pp: case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ (-a *
      ∑ x ∈ antidiagonal (single () n),
        if x.2 < single () n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ)
        else 0) =
    -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) (MvPowerSeries.inv.aux a φ) else 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : n = 0
⊢ a = a
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.hi
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match a with
      | (a, b) => (single () a, single () b)) ∈
      antidiagonal (single () n)

pp: case neg.e_a.hj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match a with
      | (f, g) => (f (), g ())) ∈
      antidiagonal n

pp: case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

pp: case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
·

Goal state after:
case neg.e_a.hi
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match a with
      | (a, b) => (single () a, single () b)) ∈
      antidiagonal (single () n)
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.hj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match a with
      | (f, g) => (f (), g ())) ∈
      antidiagonal n

pp: case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

pp: case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
·

Goal state after:
case neg.e_a.hj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match a with
      | (f, g) => (f (), g ())) ∈
      antidiagonal n
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

pp: case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
·

Goal state after:
case neg.e_a.left_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a

pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
·

Goal state after:
case neg.e_a.right_neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match
        match a with
        | (f, g) => (f (), g ()) with
      | (a, b) => (single () a, single () b)) =
      a
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
·

Goal state after:
case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff a_1.1) φ * (coeff a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : n ≤ j
⊢ (if (i, j).2 < n then (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0

pp: case neg.e_a.h.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (if (i, j).2 < n then (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0

Tactic:
·

Goal state after:
case neg.e_a.h.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : n ≤ j
⊢ (if (i, j).2 < n then (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) =
    (MvPowerSeries.coeff
          (match (i, j) with
            | (a, b) => (single () a, single () b)).1)
        φ *
      (MvPowerSeries.coeff
          (match (i, j) with
            | (a, b) => (single () a, single () b)).2)
        (MvPowerSeries.inv.aux a φ)

pp: case neg.e_a.h.inr.hc
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
      | (a, b) => (single () a, single () b)).2 <
    single () n

Tactic:
·

Goal state after:
case neg.e_a.h.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (coeff (i, j).1) φ * (coeff (i, j).2) (MvPowerSeries.inv.aux a φ) =
    (MvPowerSeries.coeff
          (match (i, j) with
            | (a, b) => (single () a, single () b)).1)
        φ *
      (MvPowerSeries.coeff
          (match (i, j) with
            | (a, b) => (single () a, single () b)).2)
        (MvPowerSeries.inv.aux a φ)
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inr.hc.refine_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
      | (a, b) => (single () a, single () b)).2 ≤
    single () n

pp: case neg.e_a.h.inr.hc.refine_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j

Tactic:
·

Goal state after:
case neg.e_a.h.inr.hc.refine_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
      | (a, b) => (single () a, single () b)).2 ≤
    single () n
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case neg.e_a.h.inr.hc.refine_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j

Tactic:
·

Goal state after:
case neg.e_a.h.inr.hc.refine_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case left
k : Type u_2
inst✝ : Field k
⊢ 1 ∉ Ideal.span {X}

pp: case right
k : Type u_2
inst✝ : Field k
⊢ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Tactic:
·

Goal state after:
case left
k : Type u_2
inst✝ : Field k
⊢ 1 ∉ Ideal.span {X}
Module: Mathlib.RingTheory.PowerSeries.Inverse

Goal state before:
pp: case right
k : Type u_2
inst✝ : Field k
⊢ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Tactic:
·

Goal state after:
case right
k : Type u_2
inst✝ : Field k
⊢ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J
Module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v₁ v₂ : HeightOneSpectrum (𝓞 K)
a : v₁ = v₂
⊢ mk v₁ = mk v₂

Tactic:
by rw [a]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : 3 = 0
⊢ ofJ 1728 = ofJ1728 F

pp: case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
·

Goal state after:
case pos
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : 3 = 0
⊢ ofJ 1728 = ofJ1728 F
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ ofJ 1728 = ofJ1728 F

Tactic:
·

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ ofJ 1728 = ofJ1728 F
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
⊢ (ofJ j).IsElliptic

pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).IsElliptic

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
⊢ (ofJ j).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ (ofJ j).IsElliptic

pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).IsElliptic

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : 3 = 0
⊢ (ofJ j).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).IsElliptic

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j = 0
h3 : ¬3 = 0
⊢ (ofJ j).IsElliptic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).IsElliptic

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝² : W.IsElliptic
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : ¬j = 0
⊢ (ofJ j).IsElliptic