awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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 ℤ))
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 ℤ))
⊢ 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:
cases x'
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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 ℤ))
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 ℤ))
⊢ 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 y'
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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 ℤ))
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 ℤ))
⊢ 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 y'
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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
a 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:
simp only [← ENat.coe_add, ENat.recTopCoe_coe, Nat.cast_add (R := ℤ),
          ofAdd_add, WithZero.coe_mul]

Premises used: ofAdd_add, Nat.cast_add, ENat.recTopCoe_coe, WithZero.coe_mul, ENat.coe_add
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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
a 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:
on_goal 4 =>
        simp only [← ENat.coe_add, ENat.recTopCoe_coe, Nat.cast_add (R := ℤ),
          ofAdd_add, WithZero.coe_mul]

Premises used: ofAdd_add, Nat.cast_add, ENat.recTopCoe_coe, WithZero.coe_mul, ENat.coe_add
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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 ℤ)))
      (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:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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
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:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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
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 ℤ)))
          (↑a : ℕ∞) :
        WithZero (Multiplicative ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          ⊤ :
        WithZero (Multiplicative ℤ))

Tactic:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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 : y ∉ nonZeroDivisors R
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (ord R (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 ℤ)))
          (ord R x) :
        WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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)
_ : x ∉ nonZeroDivisors R
h : 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 * y)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ)) (0 : 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:
simp_all [mul_mem_nonZeroDivisors]

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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)
_ : x ∉ nonZeroDivisors R
h : y ∉ nonZeroDivisors R
⊢ ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
      (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
      (ord R (x * y)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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
_ : x * y ∉ nonZeroDivisors R
h : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
h_1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
⊢ 0 =
    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 ℤ))

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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
_ : x * y ∉ nonZeroDivisors R
h : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
h_1 : y ∉ nonZeroDivisors R
⊢ 0 =
    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 ℤ))
      (0 : WithZero (Multiplicative ℤ))

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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
_ : x * y ∉ nonZeroDivisors R
h : x ∉ nonZeroDivisors R
h_1 : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
⊢ 0 =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ)) (0 : 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:
simp_all [mul_mem_nonZeroDivisors]

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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
_ : x * y ∉ nonZeroDivisors R
h : x ∉ nonZeroDivisors R
h_1 : y ∉ nonZeroDivisors R
⊢ 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0

Tactic:
simp_all [mul_mem_nonZeroDivisors]

Premises used: mul_mem_nonZeroDivisors
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
y : ↥(nonZeroDivisors R)
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) = ⊤
⊢ Eq (α := WithZero (Multiplicative ℤ))
      (((ordMonoidWithZeroHom R : R →*₀ WithZero (Multiplicative ℤ)) : (a : R) → WithZero (Multiplicative ℤ)) (↑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]

Premises used: SetLike.coe_mem, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, reduceIte, Ring.ordMonoidWithZeroHom
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Nontrivial R
y : ↥(nonZeroDivisors R)
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 = ⊤
⊢ 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:
generalize ord R y = k

Premises used: Ring.ord, Subtype.val
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
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 (α := ℕ∞) ⊤ ⊤
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 : ℕ∞) ⊤
⊢ 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:
cases k