awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ ≤ (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₄ : α
rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₅ : α
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₈ : (↑d₂ : α) * ((↑a₂ : α) * b₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
Tactic: rw [← mul_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_le_mul_iff_right, ← mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ ≤ (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₄ : α
rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₅ : α
rw₈ : (↑d₂ : α) * ((↑a₂ : α) * b₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₉ : (↑a₂ : α) * ((↑d₂ : α) * b₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
Tactic: rw [← mul_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_le_mul_iff_right, ← mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ ≤ (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₄ : α
rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₅ : α
rw₈ : (↑d₂ : α) * ((↑a₂ : α) * b₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₉ : (↑a₂ : α) * ((↑d₂ : α) * b₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₁₀ : (↑a₂ : α) * ((↑d₂ : α) * b₁) ≤ (↑a₂ : α) * ((↑b₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
Tactic: rw [← mul_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_le_mul_iff_right, ← mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ ≤ (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₄ : α
rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
a₅ : α
rw₈ : (↑d₂ : α) * ((↑a₂ : α) * b₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₉ : (↑a₂ : α) * ((↑d₂ : α) * b₁) ≤ (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
rw₁₀ : (↑a₂ : α) * ((↑d₂ : α) * b₁) ≤ (↑a₂ : α) * ((↑b₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₁₁ : (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
Tactic: rw [← mul_le_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_le_mul_iff_right, ← mul_le_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_le_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
⊢ (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂
have obtain : ∀ (e : ↥s) (he : (↑e : α) * ((↑(b₁, b₂).2 : α) * (a₁, a₂).1) = (↑e : α) * ((↑(a₁, a₂).2 : α) * (b₁, b₂).1)),
  (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂
Tactic: obtain ⟨e, he⟩ := r_iff_exists.1 hab
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e : ↥s
he : (↑e : α) * ((↑(b₁, b₂).2 : α) * (a₁, a₂).1) = (↑e : α) * ((↑(a₁, a₂).2 : α) * (b₁, b₂).1)
⊢ (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂
have obtain : ∀ (f : ↥s) (hf : (↑f : α) * ((↑(d₁, d₂).2 : α) * (c₁, c₂).1) = (↑f : α) * ((↑(c₁, c₂).2 : α) * (d₁, d₂).1)),
  (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂
Tactic: obtain ⟨f, hf⟩ := r_iff_exists.1 hcd
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (hypothesis)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e : ↥s
he : (↑e : α) * ((↑(b₁, b₂).2 : α) * (a₁, a₂).1) = (↑e : α) * ((↑(a₁, a₂).2 : α) * (b₁, b₂).1)
f : ↥s
hf : (↑f : α) * ((↑(d₁, d₂).2 : α) * (c₁, c₂).1) = (↑f : α) * ((↑(c₁, c₂).2 : α) * (d₁, d₂).1)
⊢ (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂
have he₁ : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
Tactic: simp only [mul_right_inj] at he hf
Cleared hypotheses: he, hf
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (hypothesis)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e : ↥s
he : (↑e : α) * ((↑(b₁, b₂).2 : α) * (a₁, a₂).1) = (↑e : α) * ((↑(a₁, a₂).2 : α) * (b₁, b₂).1)
f : ↥s
hf : (↑f : α) * ((↑(d₁, d₂).2 : α) * (c₁, c₂).1) = (↑f : α) * ((↑(c₁, c₂).2 : α) * (d₁, d₂).1)
he₁ : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
⊢ (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) a₁ a₂ c₁ c₂ ↔
    (fun (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s) ↦ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁) b₁ b₂ d₁ d₂
have hf₁ : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
Tactic: simp only [mul_right_inj] at he hf
Cleared hypotheses: he, hf
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₄ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₅ : (↑d₂ : α) * a₁ < (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ < (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ < (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₄ : α
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ < (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₄ : α
rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₅ : α
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₈ : (↑d₂ : α) * ((↑a₂ : α) * b₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Order (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁_1 b₁_1 : α
a₂_1 b₂_1 : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s : (a : α × ↥s) → α × ↥s → Prop) (a₁, a₂) (b₁, b₂)
hcd : (r s : (a : α × ↥s) → α × ↥s → Prop) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁
hf : (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁
rw : (↑c₂ : α) * a₁ * d₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₃ : α
rw₁ : (↑c₂ : α) * d₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
c : α
rw₂ : (↑d₂ : α) * c₁ * a₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₃ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * c₁ * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₄ : (↑d₂ : α) * a₁ * c₁ < (↑a₂ : α) * d₁ * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₅ : (↑d₂ : α) * a₁ < (↑a₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₄ : α
rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
a₅ : α
rw₈ : (↑d₂ : α) * ((↑a₂ : α) * b₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
have rw₉ : (↑a₂ : α) * ((↑d₂ : α) * b₁) < (↑b₂ : α) * ((↑a₂ : α) * d₁) ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
Tactic: rw [← mul_lt_mul_iff_right, mul_right_comm, ← hf, mul_right_comm, mul_right_comm (a₂ : α),
          mul_lt_mul_iff_right, ← mul_lt_mul_iff_left, mul_left_comm, he, mul_left_comm,
          mul_left_comm (b₂ : α), mul_lt_mul_iff_left]