awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
__1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (ord R x + ord R y) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R x) :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R y) :
        WithZero (Multiplicative ℤ))
have pos : ∀ (x' : ℕ∞),
  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (x' + ord R y) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          x' :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R y) :
        WithZero (Multiplicative ℤ))
Tactic: generalize ord R x = x'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
__1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
x' : ℕ∞
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (x' + ord R y) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          x' :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R y) :
        WithZero (Multiplicative ℤ))
have pos : ∀ (y' : ℕ∞),
  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (x' + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          x' :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
Tactic: generalize ord R y = y'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
__1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
x' y' : ℕ∞
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (x' + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          x' :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
have pos : ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
    (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
    (⊤ + y') =
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        ⊤ :
      WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        y' :
      WithZero (Multiplicative ℤ))
Tactic: cases x'
Cleared hypotheses: x'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
__1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
x' y' : ℕ∞
pos :
  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (⊤ + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (x' + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          x' :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
have pos₁ : ∀ (a : ℕ),
  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      ((↑a : ℕ∞) + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
Tactic: cases x'
Cleared hypotheses: x'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
__1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
y' : ℕ∞
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (⊤ + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
have pos : ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
    (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
    (HAdd.hAdd (α := ℕ∞) ⊤ ⊤) =
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        ⊤ :
      WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        ⊤ :
      WithZero (Multiplicative ℤ))
Tactic: cases y'
Cleared hypotheses: y'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
__1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
y' : ℕ∞
pos :
  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (HAdd.hAdd (α := ℕ∞) ⊤ ⊤) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (⊤ + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
have pos₁ : ∀ (a : ℕ),
  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (HAdd.hAdd (α := ℕ∞) ⊤ (↑a : ℕ∞)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
Tactic: cases y'
Cleared hypotheses: y'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
__1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
y' : ℕ∞
a : ℕ
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      ((↑a : ℕ∞) + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
have pos : ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
    (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
    (HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) ⊤) =
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (↑a : ℕ∞) :
      WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        ⊤ :
      WithZero (Multiplicative ℤ))
Tactic: cases y'
Cleared hypotheses: y'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : AddCommMonoid M
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Nontrivial R
x y : R
__1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
y' : ℕ∞
a : ℕ
pos :
  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) ⊤) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      ((↑a : ℕ∞) + y') =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          y' :
        WithZero (Multiplicative ℤ))
have pos₁ : ∀ (a_1 : ℕ),
  ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (HAdd.hAdd (α := ℕ∞) (↑a : ℕ∞) (↑a_1 : ℕ∞)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a_1 : ℕ∞) :
        WithZero (Multiplicative ℤ))
Tactic: cases y'
Cleared hypotheses: y'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑y : R) :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    ord R (↑y : R) = ⊤
have simp : Eq (α := WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R (↑y : R)) :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ)) ↔
  ord R (↑y : R) = ⊤
Tactic: simp only [ordMonoidWithZeroHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, SetLike.coe_mem,
    ↓reduceIte]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R (↑y : R)) :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    ord R (↑y : R) = ⊤
have generalize : ∀ (k : ℕ∞),
  Eq (α := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          k :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    k = ⊤
Tactic: generalize ord R y = k
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
y : ↥(nonZeroDivisors R)
k : ℕ∞
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          k :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    k = ⊤
have top : Eq (α := WithZero (Multiplicative ℤ))
    (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        ⊤ :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ)) ↔
  Eq (α := ℕ∞) ⊤ ⊤
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
y : ↥(nonZeroDivisors R)
k : ℕ∞
top :
  Eq (α := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    Eq (α := ℕ∞) ⊤ ⊤
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          k :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    k = ⊤
have coe : ∀ (a : ℕ),
  Eq (α := WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    Eq (α := ℕ∞) (↑a : ℕ∞) ⊤
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ IsFiniteLength R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
have rw : IsNoetherian R (HasQuotient.Quotient R (B := Ideal R) (span {x})) ∧
  IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
Tactic: rw [isFiniteLength_iff_isNoetherian_isArtinian]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : KrullDimLE 1 R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ IsNoetherian R (HasQuotient.Quotient R (B := Ideal R) (span {x})) ∧
    IsArtinian R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
have suffices : IsArtinianRing.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x}))
Tactic: suffices IsArtinianRing (R ⧸ Ideal.span {x}) from
    ⟨isNoetherian_quotient (Ideal.span {x}),
      isArtinian_of_surjective_algebraMap (Ideal.Quotient.mk_surjective (I := .span {x}))⟩