awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (min (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) x)
        (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) y) :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) (x + y) :
      WithZero (Multiplicative ℤ))
have simp : LE.le (α := WithZero (Multiplicative ℤ))
  (min
      (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          x)⁻¹
      (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          y)⁻¹ :
    WithZero (Multiplicative ℤ))
  ((((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
          (a : K) → WithZero (Multiplicative ℤ))
        (x + y))⁻¹ :
    WithZero (Multiplicative ℤ))
Tactic: simp only [ordFrac_eq_valuation_inv]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h1 : x + y ≠ 0
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (min
        (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            x)⁻¹
        (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
              (a : K) → WithZero (Multiplicative ℤ))
            y)⁻¹ :
      WithZero (Multiplicative ℤ))
    ((((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
            (a : K) → WithZero (Multiplicative ℤ))
          (x + y))⁻¹ :
      WithZero (Multiplicative ℤ))
have h₂ : LT.lt (α := WithZero (Multiplicative ℤ)) 0
  (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
      (a : K) → WithZero (Multiplicative ℤ))
    (x + y))
Tactic: grw [Valuation.map_add, min_inv_inv_le]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
K : Type u_2
inst_3 : Field K
inst_4 : Algebra R K
inst_5 : IsFractionRing R K
x y : K
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (((ordFrac R : K →*₀ WithZero (Multiplicative ℤ)) : (a : K) → WithZero (Multiplicative ℤ)) y :
      WithZero (Multiplicative ℤ))
⊢ ∃ (u : Rˣ), u • x = y
have h₁ : Eq (α := WithZero (Multiplicative ℤ))
  (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      x :
    WithZero (Multiplicative ℤ))
  (((valuation K (IsDiscreteValuationRing.maximalIdeal R) : Valuation K (WithZero (Multiplicative ℤ))) :
        (a : K) → WithZero (Multiplicative ℤ))
      y :
    WithZero (Multiplicative ℤ))
Tactic: rw [ordFrac_eq_valuation_inv, ordFrac_eq_valuation_inv, inv_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
s : ↥S
⊢ Eq (α := OreLocalization S R) (0 /ₒ s) 0
have rw : ∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := R) u 0 = HSMul.hSMul (β := R) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑s : R)
Tactic: rw [OreLocalization.zero_def, oreDiv_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
x : OreLocalization S R
⊢ 0 * x = 0
have c : ∀ (r : R) (s : ↥S), HMul.hMul (α := OreLocalization S R) 0 (r /ₒ s) = 0
Tactic: induction x using OreLocalization.ind with | _ r s
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
⊢ HMul.hMul (α := OreLocalization S R) 0 (r /ₒ s) = 0
have c : HMul.hMul (α := OreLocalization S R) (0 /ₒ 1) (r /ₒ s) = 0 /ₒ 1
Tactic: rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (0 /ₒ 1) (r /ₒ s) = 0 /ₒ 1
⊢ HMul.hMul (α := OreLocalization S R) 0 (r /ₒ s) = 0
have c₁ : Eq (α := OreLocalization S R) (0 * r /ₒ HMul.hMul (α := ↥S) 1 1) (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (0 /ₒ 1) (r /ₒ s) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S R) (0 * r /ₒ HMul.hMul (α := ↥S) 1 1) (0 /ₒ 1)
⊢ HMul.hMul (α := OreLocalization S R) 0 (r /ₒ s) = 0
have c₂ : Eq (α := OreLocalization S R) (0 /ₒ HMul.hMul (α := ↥S) 1 1) (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (0 /ₒ 1) (r /ₒ s) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S R) (0 * r /ₒ HMul.hMul (α := ↥S) 1 1) (0 /ₒ 1)
c₂ : Eq (α := OreLocalization S R) (0 /ₒ HMul.hMul (α := ↥S) 1 1) (0 /ₒ 1)
⊢ HMul.hMul (α := OreLocalization S R) 0 (r /ₒ s) = 0
have c₃ : Eq.{u_1 + 1} (α := OreLocalization S R) (0 /ₒ 1) (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
x : OreLocalization S R
⊢ x * 0 = 0
have c : ∀ (r : R) (s : ↥S), HMul.hMul (α := OreLocalization S R) (r /ₒ s) 0 = 0
Tactic: induction x using OreLocalization.ind with | _ r s
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
⊢ HMul.hMul (α := OreLocalization S R) (r /ₒ s) 0 = 0
have c : HMul.hMul (α := OreLocalization S R) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
Tactic: rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
⊢ HMul.hMul (α := OreLocalization S R) (r /ₒ s) 0 = 0
have c₁ : Eq (α := OreLocalization S R) (r * 0 /ₒ s) (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S R) (r * 0 /ₒ s) (0 /ₒ 1)
⊢ HMul.hMul (α := OreLocalization S R) (r /ₒ s) 0 = 0
have c₂ : Eq (α := OreLocalization S R) (0 /ₒ s) (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S R) (r * 0 /ₒ s) (0 /ₒ 1)
c₂ : Eq (α := OreLocalization S R) (0 /ₒ s) (0 /ₒ 1)
⊢ HMul.hMul (α := OreLocalization S R) (r /ₒ s) 0 = 0
have c₃ : Eq.{u_1 + 1} (α := OreLocalization S R) 0 (0 /ₒ 1)
Tactic: rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
c : HMul.hMul (α := OreLocalization S R) (r /ₒ s) (0 /ₒ 1) = 0 /ₒ 1
c₁ : Eq (α := OreLocalization S R) (r * 0 /ₒ s) (0 /ₒ 1)
c₂ : Eq (α := OreLocalization S R) (0 /ₒ s) (0 /ₒ 1)
c₃ : Eq.{u_1 + 1} (α := OreLocalization S R) 0 (0 /ₒ 1)
⊢ HMul.hMul (α := OreLocalization S R) (r /ₒ s) 0 = 0
have c₄ : Eq.{u_1 + 1} (α := OreLocalization S R) 0 0
Tactic: rw [OreLocalization.zero_def, mul_div_one, mul_zero, zero_oreDiv', zero_oreDiv']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
⊢ Subsingleton.{u_1 + 1} (OreLocalization S R) ↔ 0 ∈ S
have rw : (∃ (u : ↥S), ∃ (v : R), HSMul.hSMul (β := R) u 1 = HSMul.hSMul (β := R) v 0 ∧ (↑u : R) * (↑1 : R) = v * (↑1 : R)) ↔
  0 ∈ S
Tactic: rw [← subsingleton_iff_zero_eq_one, OreLocalization.one_def,
    OreLocalization.zero_def, oreDiv_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
⊢ Nontrivial.{u_1} (OreLocalization S R) ↔ ¬0 ∈ S
have rw : ¬Subsingleton.{u_1 + 1} (OreLocalization S R) ↔ ¬0 ∈ S
Tactic: rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
S : Submonoid R
inst_1 : OreSet S
rw : ¬Subsingleton.{u_1 + 1} (OreLocalization S R) ↔ ¬0 ∈ S
⊢ Nontrivial.{u_1} (OreLocalization S R) ↔ ¬0 ∈ S
have rw₁ : ¬0 ∈ S ↔ ¬0 ∈ S
Tactic: rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
⊢ Eq (α := OreLocalization S X)
    ((oreDenom (↑s₁ : R) s₂ • r₁ + oreNum (↑s₁ : R) s₂ • r₂) /ₒ (oreDenom (↑s₁ : R) s₂ * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)
have ha : (↑(oreDenom (↑s₁ : R) s₂) : R) * (↑s₁ : R) = oreNum (↑s₁ : R) s₂ * (↑s₂ : R)
Tactic: have ha := ore_eq (s₁ : R) s₂
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ha : (↑(oreDenom (↑s₁ : R) s₂) : R) * (↑s₁ : R) = oreNum (↑s₁ : R) s₂ * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X)
    ((oreDenom (↑s₁ : R) s₂ • r₁ + oreNum (↑s₁ : R) s₂ • r₂) /ₒ (oreDenom (↑s₁ : R) s₂ * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)
have generalize : ∀ (ra : R) (ha : (↑(oreDenom (↑s₁ : R) s₂) : R) * (↑s₁ : R) = ra * (↑s₂ : R)),
  Eq (α := OreLocalization S X) ((oreDenom (↑s₁ : R) s₂ • r₁ + ra • r₂) /ₒ (oreDenom (↑s₁ : R) s₂ * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)
Tactic: generalize oreNum (s₁ : R) s₂ = ra at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
ha : (↑(oreDenom (↑s₁ : R) s₂) : R) * (↑s₁ : R) = ra * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) ((oreDenom (↑s₁ : R) s₂ • r₁ + ra • r₂) /ₒ (oreDenom (↑s₁ : R) s₂ * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)
have generalize : ∀ (sa : ↥S) (ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)),
  Eq (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)
Tactic: generalize oreDenom (s₁ : R) s₂ = sa at *
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
⊢ Eq (α := OreLocalization S X) ((sa • r₁ + ra • r₂) /ₒ (sa * s₁))
    ((sb • r₁ + rb • r₂) /ₒ Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h)
have rw : ∃ (u : ↥S),
  ∃ (v : R),
    u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
      (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
Tactic: rw [oreDiv_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
have rcases : ∀ (rc : R) (sc : ↥S) (hc : (↑sc : R) * sb = rc * (↑sa : R)),
  ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
Tactic: rcases oreCondition sb sa with ⟨rc, sc, hc⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
have rw : (↑sc : R) * rb * (↑s₂ : R) = rc * (ra * (↑s₂ : R))
Tactic: rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
rw : (↑sc : R) * rb * (↑s₂ : R) = rc * (ra * (↑s₂ : R))
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
have rw₁ : (↑sc : R) * rb * (↑s₂ : R) = rc * ((↑sa : R) * (↑s₁ : R))
Tactic: rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
rw : (↑sc : R) * rb * (↑s₂ : R) = rc * (ra * (↑s₂ : R))
rw₁ : (↑sc : R) * rb * (↑s₂ : R) = rc * ((↑sa : R) * (↑s₁ : R))
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
have rw₂ : (↑sc : R) * rb * (↑s₂ : R) = rc * (↑sa : R) * (↑s₁ : R)
Tactic: rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
rw : (↑sc : R) * rb * (↑s₂ : R) = rc * (ra * (↑s₂ : R))
rw₁ : (↑sc : R) * rb * (↑s₂ : R) = rc * ((↑sa : R) * (↑s₁ : R))
rw₂ : (↑sc : R) * rb * (↑s₂ : R) = rc * (↑sa : R) * (↑s₁ : R)
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
have rw₃ : (↑sc : R) * rb * (↑s₂ : R) = (↑sc : R) * sb * (↑s₁ : R)
Tactic: rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
rw : (↑sc : R) * rb * (↑s₂ : R) = rc * (ra * (↑s₂ : R))
rw₁ : (↑sc : R) * rb * (↑s₂ : R) = rc * ((↑sa : R) * (↑s₁ : R))
rw₂ : (↑sc : R) * rb * (↑s₂ : R) = rc * (↑sa : R) * (↑s₁ : R)
rw₃ : (↑sc : R) * rb * (↑s₂ : R) = (↑sc : R) * sb * (↑s₁ : R)
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
have rw₄ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * sb * (↑s₁ : R)
Tactic: rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
rw : (↑sc : R) * rb * (↑s₂ : R) = rc * (ra * (↑s₂ : R))
rw₁ : (↑sc : R) * rb * (↑s₂ : R) = rc * ((↑sa : R) * (↑s₁ : R))
rw₂ : (↑sc : R) * rb * (↑s₂ : R) = rc * (↑sa : R) * (↑s₁ : R)
rw₃ : (↑sc : R) * rb * (↑s₂ : R) = (↑sc : R) * sb * (↑s₁ : R)
rw₄ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * sb * (↑s₁ : R)
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
have rw₅ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * (sb * (↑s₁ : R))
Tactic: rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
rw : (↑sc : R) * rb * (↑s₂ : R) = rc * (ra * (↑s₂ : R))
rw₁ : (↑sc : R) * rb * (↑s₂ : R) = rc * ((↑sa : R) * (↑s₁ : R))
rw₂ : (↑sc : R) * rb * (↑s₂ : R) = rc * (↑sa : R) * (↑s₁ : R)
rw₃ : (↑sc : R) * rb * (↑s₂ : R) = (↑sc : R) * sb * (↑s₁ : R)
rw₄ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * sb * (↑s₁ : R)
rw₅ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * (sb * (↑s₁ : R))
⊢ (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
have rw₆ : (↑sc : R) * (rb * (↑s₂ : R)) = (↑sc : R) * (rb * (↑s₂ : R))
Tactic: rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
have this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
Tactic: have : sc * rb * s₂ = rc * ra * s₂ := by
    rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
have rcases : ∀ (sd : ↥S) (hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)),
  ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
Tactic: rcases ore_right_cancel _ _ s₂ this with ⟨sd, hd⟩
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
⊢ ∃ (u : ↥S),
    ∃ (v : R),
      u • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
        (↑u : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
have h₁ : ∃ (v : R),
  (sd * sc) • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
    (↑(sd * sc) : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
Tactic: use sd * sc
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddMonoid X
inst_3 : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * (↑s₁ : R) = rb * (↑s₂ : R)
h : sb * (↑s₁ : R) ∈ S
ra : R
sa : ↥S
ha : (↑sa : R) * (↑s₁ : R) = ra * (↑s₂ : R)
rc : R
sc : ↥S
hc : (↑sc : R) * sb = rc * (↑sa : R)
this : (↑sc : R) * rb * (↑s₂ : R) = rc * ra * (↑s₂ : R)
sd : ↥S
hd : (↑sd : R) * ((↑sc : R) * rb) = (↑sd : R) * (rc * ra)
⊢ ∃ (v : R),
    (sd * sc) • (sb • r₁ + rb • r₂) = v • (sa • r₁ + ra • r₂) ∧
      (↑(sd * sc) : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) = v * (↑(sa * s₁) : R)
have h₁ : (sd * sc) • (sb • r₁ + rb • r₂) = ((↑sd : R) * rc) • (sa • r₁ + ra • r₂) ∧
  (↑(sd * sc) : R) * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ S) (sb * (↑s₁ : R)) h) : R) =
    (↑sd : R) * rc * (↑(sa * s₁) : R)
Tactic: use sd * rc