awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
this : Submodule.map (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) I = a • I
h : Eq (α := Submodule R (R ⧸ a • I)) (Submodule.map (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) I) ⊥
h₁ :
  Eq (α := Submodule R (R ⧸ a • I))
    (Submodule.map (Submodule.mkQ (a • I)) (Submodule.map (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) I))
    ⊥
h₂ : Eq.{u_1 + 1} (α := Submodule R (R ⧸ a • I)) (Submodule.map (Submodule.mkQ (a • I)) (a • I)) ⊥
⊢ I ≤ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
have h₃ : Eq.{u_1 + 1} (α := Submodule R (R ⧸ a • I)) ⊥ ⊥
Tactic: rw [le_ker_iff_map, Submodule.map_comp, this, Submodule.mkQ_map_self]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ I = Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I)
have h : ∀ (b : R),
  b ∈ I ↔
    Membership.mem (γ := Ideal R) (Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I)) b
Tactic: ext b
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) ≤ I
have m : I = Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I)
Tactic: have m : I = Submodule.comap (mul R R a) (a • I) := by
      ext b
      exact (Submodule.mul_mem_smul_iff ha).symm
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
⊢ Function.Exact (M := R ⧸ I) (N := R ⧸ a • I) (P := HasQuotient.Quotient R (B := Ideal R) (span {a}))
    (⇑(mulQuot a I) : (a_1 : R ⧸ I) → R ⧸ a • I) (⇑(quotOfMul a I) : (a_1 : R ⧸ a • I) → R ⧸ span {a})
have simp : (quotOfMul a I).ker = (mulQuot a I).range
Tactic: simp only [exact_iff]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
⊢ (quotOfMul a I).ker = (mulQuot a I).range
have this : (quotOfMul a I).ker = HSMul.hSMul (β := Submodule R (R ⧸ a • I)) a ⊤
Tactic: have : ker (Ideal.quotOfMul a I) = a • ⊤ := by
    simp only [← submodule_span_eq, quotOfMul, Submodule.factor, Submodule.mapQ, comp_id,
      Submodule.ker_liftQ, Submodule.ker_mkQ, Submodule.map_span, Submodule.mkQ_apply,
      Quotient.mk_eq_mk, Set.image_singleton, Quotient.smul_top]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
⊢ ord R (a * b) = ord R a + ord R b
have 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}))
Tactic: have := Module.length_eq_add_of_exact (Ideal.mulQuot b (Ideal.span {a}))
          (Ideal.quotOfMul b (Ideal.span {a})) (Ideal.mulQuot_injective (Ideal.span {a}) hb)
          (Ideal.quotOfMul_surjective (Ideal.span {a}))
          (Ideal.exact_mulQuot_quotOfMul (Ideal.span {a}))
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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}))
⊢ ord R (a * b) = ord R a + ord R b
have simp : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
  Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a}))
Tactic: simp only [Ring.ord, ← this]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
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}))
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
    Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a}))
have lem : HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = span {b * a}
Tactic: have lem : (({b} : Set R) • Ideal.span {a}) = Ideal.span {b * a} := by
    simp [← Ideal.submodule_span_eq, Submodule.set_smul_span]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
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}
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
    Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a}))
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
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})
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
    Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a}))
have lem₁ : HSMul.hSMul (β := Ideal R) b (span {a}) = span {b * a}
Tactic: rw [this] at lem
Cleared hypotheses: lem, this
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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})
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
    Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a}))
have 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}))
Tactic: rw [lem, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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}))
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
    Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a}))
have 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}))
Tactic: rw [lem, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ ord R (a * b) = ord R a + ord R b
have rw : ord R (b * a) = ord R a + ord R b
Tactic: rw [mul_comm, ord_mul R ha, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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
⊢ ord R (a * b) = ord R a + ord R b
have rw₁ : ord R b + ord R a = ord R a + ord R b
Tactic: rw [mul_comm, ord_mul R ha, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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
⊢ ord R (a * b) = ord R a + ord R b
have rw₂ : ord R a + ord R b = ord R a + ord R b
Tactic: rw [mul_comm, ord_mul R ha, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x : R
hx : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x
n : ℕ
⊢ ord R (x ^ n) = n • ord R x
have zero : ord R (HPow.hPow (β := ℕ) x 0) = HSMul.hSMul (α := ℕ) 0 (ord R x)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ord_mul, ih, succ_nsmul]
    exact hx
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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)
⊢ ord R (x ^ n) = n • ord R x
have succ : ∀ (n : ℕ) (ih : ord R (x ^ n) = n • ord R x), ord R (x ^ (n + 1)) = (n + 1) • ord R x
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, ord_mul, ih, succ_nsmul]
    exact hx
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
h : IsUnit a
x : R
⊢ ord R (a * x) = ord R x
have rw : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * x})) = ord R x
Tactic: rw [ord, ord, Ideal.span_singleton_mul_left_unit h x]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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
⊢ ord R (a * x) = ord R x
have rw₁ : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * x})) =
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
Tactic: rw [ord, ord, Ideal.span_singleton_mul_left_unit h x]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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}))
⊢ ord R (a * x) = ord R x
have rw₂ : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x})) =
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
Tactic: rw [ord, ord, Ideal.span_singleton_mul_left_unit h x]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
h : IsUnit a
x : R
⊢ ord R (x * a) = ord R x
have rw : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x * a})) = ord R x
Tactic: rw [ord, ord, Ideal.span_singleton_mul_right_unit h x]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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
⊢ ord R (x * a) = ord R x
have rw₁ : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x * a})) =
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
Tactic: rw [ord, ord, Ideal.span_singleton_mul_right_unit h x]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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}))
⊢ ord R (x * a) = ord R x
have rw₂ : Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x})) =
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x}))
Tactic: rw [ord, ord, Ideal.span_singleton_mul_right_unit h x]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : Associated x y
⊢ ord R x = ord R y
have obtain : ∀ (a : Rˣ), ord R x = ord R (x * (↑a : R))
Tactic: obtain ⟨a, rfl⟩ := h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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 (a • x) = ord R x
have rw : ord R (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) a : R) x) = ord R x
Tactic: rw [Algebra.smul_def a x]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a x : R
⊢ Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {x})) ≤
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * x}))
have suffices : LE.le (α := Ideal R) (span {a * x}) (span {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)
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a x : R
⊢ LE.le (α := Ideal R) (span {a * x}) (span {x})
have rw : x ∣ a * x
Tactic: rw [Ideal.span_singleton_le_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a x : R
h : a ∣ x
⊢ ord R a ≤ ord R x
have obtain : ∀ (b : R), ord R a ≤ ord R (a * b)
Tactic: obtain ⟨b, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
⊢ ord R a ≤ ord R (a * b)
have rw : ord R a ≤ ord R (b * a)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ ord R ϖ = 1
have rw : IsSimpleModule R (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
Tactic: rw [Ring.ord, Module.length_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ IsSimpleModule R (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
have this : IsMaximal (α := R) (span {ϖ})
Tactic: have : (Ideal.span {ϖ}).IsMaximal :=
    PrincipalIdealRing.isMaximal_of_irreducible hϖ
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
this : IsMaximal (α := R) (span {ϖ})
⊢ IsSimpleModule R (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
have rw : IsSimpleModule.{u_1, u_1} (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
  (HasQuotient.Quotient R (B := Ideal R) (span {ϖ}))
Tactic: rw [isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective (S := R ⧸ Ideal.span {ϖ})
    Ideal.Quotient.mk_surjective]
-- 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
⊢ (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y) then
      ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R (x * y))
    else 0) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x then
          ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R x)
        else 0 :
        WithZero (Multiplicative ℤ))
      (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y then
          ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R y)
        else 0 :
        WithZero (Multiplicative ℤ))
have pos : ∀ (_ : 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 * 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: split_ifs with _ _ b
-- 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
pos :
  ∀ (_ : 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 * 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 ℤ))
⊢ (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (x * y) then
      ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
        (fun (x : ℕ) ↦ (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
        (ord R (x * y))
    else 0) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) x then
          ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R x)
        else 0 :
        WithZero (Multiplicative ℤ))
      (if Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y then
          ENat.recTopCoe (C := fun (x : ℕ∞) ↦ WithZero (Multiplicative ℤ)) 0
            (fun (x : ℕ) ↦
              (↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) (↑x : ℤ)) : WithZero (Multiplicative ℤ)))
            (ord R y)
        else 0 :
        WithZero (Multiplicative ℤ))
have neg : ∀ (_ : 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: split_ifs with _ _ b
-- 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 * 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 : 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: rw [ord_mul _ b]