awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
this :
  Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a})) +
      Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b}))
lem : HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = span {b * a}
⊢ HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = HSMul.hSMul (β := Ideal R) b (span {a})

Tactic:
have : (({b} : Set R) • Ideal.span {a}) = b • Ideal.span {a} := Submodule.singleton_set_smul
    (Ideal.span {a}) b
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
this_1 :
  Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a})) +
      Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b}))
lem : HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = span {b * a}
this : HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = HSMul.hSMul (β := Ideal R) b (span {a})
⊢ HSMul.hSMul (β := Ideal R) b (span {a}) = span {b * a}

Tactic:
rw [this] at lem
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
this_1 :
  Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a})) +
      Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b}))
lem : HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = span {b * a}
this : HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = HSMul.hSMul (β := Ideal R) b (span {a})
lem₁ : HSMul.hSMul (β := Ideal R) b (span {a}) = span {b * a}
⊢ HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = HSMul.hSMul (β := Ideal R) b (span {a})

Tactic:
rw [this] at lem
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
this_1 :
  Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a})) +
      Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b}))
lem : HSMul.hSMul (β := Ideal R) b (span {a}) = span {b * a}
this : HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = HSMul.hSMul (β := Ideal R) b (span {a})
rw :
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b * a}))
rw₁ rw₂ :
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b * a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b * a}))
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
    Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a}))

Tactic:
rw [lem, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
rw : ord R (b * a) = ord R a + ord R b
rw₁ : ord R b + ord R a = ord R a + ord R b
rw₂ rw₃ : ord R a + ord R b = ord R a + ord R b
⊢ ord R (a * b) = ord R a + ord R b

Tactic:
rw [mul_comm, ord_mul R ha, add_comm]

Premises used: add_comm, mul_comm, Ring.ord_mul
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
m : HasQuotient.Quotient R (B := Submodule R R) (span {0}) ≃ₗ[R] R := Submodule.quotEquivOfEqBot (span {0}) ⋯
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {0})) = Module.length R R

Tactic:
le_antisymm (Module.length_le_of_injective m m.injective)
      (Module.length_le_of_surjective m m.surjective)

Premises used: LinearEquiv.surjective, Module.length_le_of_surjective, le_antisymm, LinearEquiv.toLinearMap, Module.length_le_of_injective, LinearEquiv.injective
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
m : HasQuotient.Quotient R (B := Submodule R R) (span {0}) ≃ₗ[R] R := Submodule.quotEquivOfEqBot (span {0}) ⋯
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {0})) = Module.length R R

Tactic:
exact le_antisymm (Module.length_le_of_injective m m.injective)
      (Module.length_le_of_surjective m m.surjective)

Premises used: Module.length_le_of_surjective, le_antisymm, Module.length_le_of_injective
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ ord R (HPow.hPow (β := ℕ) x 0) = HSMul.hSMul (α := ℕ) 0 (ord R x)

Tactic:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
n : ℕ
ih : ord R (x ^ n) = n • ord R x
succ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
⊢ ord R (x ^ (n + 1)) = (n + 1) • ord R x

Tactic:
rw [pow_succ, ord_mul, ih, succ_nsmul]

Premises used: pow_succ, Ring.ord_mul, succ_nsmul
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x

Tactic:
hx
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
n : ℕ
ih : ord R (x ^ n) = n • ord R x
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x

Tactic:
exact hx
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
n : ℕ
zero : ord R (HPow.hPow (β := ℕ) x 0) = HSMul.hSMul (α := ℕ) 0 (ord R x)
succ : ∀ (n : ℕ) (ih : ord R (x ^ n) = n • ord R x), ord R (x ^ (n + 1)) = (n + 1) • ord R x
⊢ ord R (x ^ n) = n • ord R x

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ord_mul, ih, succ_nsmul]
    exact hx

Premises used: pow_succ, Ring.ord_mul, succ_nsmul
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
h : IsUnit a
x : R
rw : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * x})) = ord R x
rw₁ :
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * x})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
rw₂ rw₃ :
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
⊢ ord R (a * x) = ord R x

Tactic:
rw [ord, ord, Ideal.span_singleton_mul_left_unit h x]

Premises used: Ring.ord, Ideal.span_singleton_mul_left_unit
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
h : IsUnit a
x : R
rw : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x * a})) = ord R x
rw₁ :
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x * a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
rw₂ rw₃ :
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
⊢ ord R (x * a) = ord R x

Tactic:
rw [ord, ord, Ideal.span_singleton_mul_right_unit h x]

Premises used: Ideal.span_singleton_mul_right_unit, Ring.ord
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : Associated x y
obtain : ∀ (a : Rˣ), ord R x = ord R (x * (↑a : R))
⊢ ord R x = ord R y

Tactic:
obtain ⟨a, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
a : Rˣ
⊢ ord R x = ord R (x * (↑a : R))

Tactic:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
⊢ Associated (-x) x

Tactic:
simp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
⊢ ord R (-x) = ord R x

Tactic:
simp [ord_eq_of_associated (x := -x) (y := x) (by simp)]

Premises used: Ring.ord_eq_of_associated
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra S R
a : S
h : IsUnit a
x : R
rw : ord R (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) a : R) x) = ord R x
⊢ ord R (a • x) = ord R x

Tactic:
rw [Algebra.smul_def a x]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) a : R) x) = ord R x

Tactic:
ord_mul_of_isUnit_left (RingHom.isUnit_map (algebraMap S R) h) x

Premises used: Algebra.algebraMap, Ring.ord_mul_of_isUnit_left, RingHom.isUnit_map
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra S R
a : S
h : IsUnit a
x : R
⊢ ord R (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) a : R) x) = ord R x

Tactic:
exact ord_mul_of_isUnit_left (RingHom.isUnit_map (algebraMap S R) h) x

Premises used: Algebra.algebraMap, Ring.ord_mul_of_isUnit_left, RingHom.isUnit_map
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a x : R
this : LE.le (α := Ideal R) (span {a * x}) (span {x})
g : HasQuotient.Quotient R (B := Ideal R) (span {a * x}) →ₗ[R] HasQuotient.Quotient R (B := Ideal R) (span {x}) :=
  Submodule.factor this
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x})) ≤
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * x}))

Tactic:
Module.length_le_of_surjective (Submodule.factor this) (Submodule.factor_surjective this)

Premises used: Module.length_le_of_surjective, Submodule.factor, Submodule.factor_surjective
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a x : R
this : LE.le (α := Ideal R) (span {a * x}) (span {x})
g : HasQuotient.Quotient R (B := Ideal R) (span {a * x}) →ₗ[R] HasQuotient.Quotient R (B := Ideal R) (span {x}) :=
  Submodule.factor this
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x})) ≤
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * x}))

Tactic:
refine Module.length_le_of_surjective (Submodule.factor this) (Submodule.factor_surjective this)

Premises used: Module.length_le_of_surjective, Submodule.factor, Submodule.factor_surjective
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a x : R
suffices : LE.le (α := Ideal R) (span {a * x}) (span {x})
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x})) ≤
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * x}))

Tactic:
suffices Ideal.span {a * x} ≤ Ideal.span {x} by
    let g : (R ⧸ Ideal.span {a * x}) →ₗ[R] (R ⧸ Ideal.span {x}) := Submodule.factor this
    refine Module.length_le_of_surjective (Submodule.factor this) (Submodule.factor_surjective this)
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a x : R
rw : x ∣ a * x
⊢ LE.le (α := Ideal R) (span {a * x}) (span {x})

Tactic:
rw [Ideal.span_singleton_le_span_singleton]

Premises used: Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a x : R
⊢ x ∣ a * x

Tactic:
Dvd.intro_left (algebraMap R R a) rfl

Premises used: Algebra.algebraMap, Dvd.intro_left, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a x : R
⊢ x ∣ a * x

Tactic:
exact Dvd.intro_left (algebraMap R R a) rfl

Premises used: Algebra.algebraMap, Dvd.intro_left, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a x : R
h : a ∣ x
obtain : ∀ (b : R), ord R a ≤ ord R (a * b)
⊢ ord R a ≤ ord R x

Tactic:
obtain ⟨b, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
rw : ord R a ≤ ord R (b * a)
⊢ ord R a ≤ ord R (a * b)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
⊢ ord R a ≤ ord R (b * a)

Tactic:
ord_le_ord_mul b a

Premises used: Ring.ord_le_ord_mul
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
⊢ ord R a ≤ ord R (b * a)

Tactic:
exact ord_le_ord_mul b a

Premises used: Ring.ord_le_ord_mul
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra S R
a : S
x : R
⊢ ord R x ≤ ord R (a • x)

Tactic:
simp [Algebra.smul_def, ord_le_ord_mul]

Premises used: Ring.ord_le_ord_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : IsUnit x
⊢ ord R x = 0

Tactic:
simpa using ord_smul_of_isUnit hx (1 : R)

Premises used: Ring.ord_smul_of_isUnit, OfNat.ofNat
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
rw : IsSimpleModule R (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
⊢ ord R ϖ = 1

Tactic:
rw [Ring.ord, Module.length_eq_one_iff]

Premises used: Ring.ord, Module.length_eq_one_iff
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ IsMaximal (α := R) (span {ϖ})

Tactic:
have : (Ideal.span {ϖ}).IsMaximal :=
    PrincipalIdealRing.isMaximal_of_irreducible hϖ
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
this : IsMaximal (α := R) (span {ϖ})
rw :
  IsSimpleModule.{u_1, u_1} (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
    (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
⊢ IsSimpleModule R (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))

Tactic:
rw [isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective (S := R ⧸ Ideal.span {ϖ})
    Ideal.Quotient.mk_surjective]

Premises used: isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
this_1 : IsMaximal (α := R) (span {ϖ})
this : Field (HasQuotient.Quotient R (B := Ideal R) (span {ϖ})) := Quotient.field (span {ϖ})
⊢ IsSimpleModule.{u_1, u_1} (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
    (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))

Tactic:
instIsSimpleModule _

Premises used: instIsSimpleModule
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
this_1 : IsMaximal (α := R) (span {ϖ})
this : Field (HasQuotient.Quotient R (B := Ideal R) (span {ϖ})) := Quotient.field (span {ϖ})
⊢ IsSimpleModule.{u_1, u_1} (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
    (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))

Tactic:
exact instIsSimpleModule _

Premises used: instIsSimpleModule
-- 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
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 0 then
        ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R 0)
      else 0 :
      WithZero (Multiplicative ℤ))
    (0 : WithZero (Multiplicative ℤ))

Tactic:
simp [nonZeroDivisors, exists_ne]

Premises used: nonZeroDivisors, exists_ne
-- 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
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1 then
        ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R 1)
      else 0 :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [nonZeroDivisors]

Premises used: 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)
_ : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
b : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
pos :
  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 ℤ))
⊢ 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 ℤ))
      (ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
          (fun (x : ℕ) ↦
            (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
          (ord R y) :
        WithZero (Multiplicative ℤ))

Tactic:
rw [ord_mul _ b]

Premises used: Ring.ord_mul
-- 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
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 ℤ))
⊢ 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 ℤ))

Tactic:
generalize ord R x = x'

Premises used: Ring.ord
-- 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' : ℕ∞
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 ℤ))
⊢ 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 y = y'

Premises used: Ring.ord