awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
s : ↥S
rw :
  HMul.hMul (β := N) (f.mk' m s) ((f : (a : M) → N) (↑s : M) : N) =
      HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) ↔
    ∃ (s : ↥S), (↑s : M) * m = 0
rw₁ :
  (f : (a : M) → N) m = HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) ↔
    ∃ (s : ↥S), (↑s : M) * m = 0
⊢ f.mk' m s = 0 ↔ ∃ (s : ↥S), (↑s : M) * m = 0
have rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) (0 : N) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
Tactic: rw [← (f.map_units s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
s : ↥S
rw :
  HMul.hMul (β := N) (f.mk' m s) ((f : (a : M) → N) (↑s : M) : N) =
      HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) ↔
    ∃ (s : ↥S), (↑s : M) * m = 0
rw₁ :
  (f : (a : M) → N) m = HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) ↔
    ∃ (s : ↥S), (↑s : M) * m = 0
rw₂ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) m : N) (0 : N) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
⊢ f.mk' m s = 0 ↔ ∃ (s : ↥S), (↑s : M) * m = 0
have rw₃ : (∃ (s : ↥S), (↑s : M) * m = 0) ↔ ∃ (s : ↥S), (↑s : M) * m = 0
Tactic: rw [← (f.map_units s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
s : ↥S
⊢ f.mk' 0 s = 0
have rw : 0 = f.mk' 0 s
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, zero_mul, f.map_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
s : ↥S
rw : 0 = f.mk' 0 s
⊢ f.mk' 0 s = 0
have rw₁ : HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) 0
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, zero_mul, f.map_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
s : ↥S
rw : 0 = f.mk' 0 s
rw₁ : HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) 0
⊢ f.mk' 0 s = 0
have rw₂ : Eq.{u_2 + 1} (α := N) (0 : N) ((f : (a : M) → N) 0 : N)
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, zero_mul, f.map_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
s : ↥S
rw : 0 = f.mk' 0 s
rw₁ : HMul.hMul (α := N) (β := N) (0 : N) ((f : (a : M) → N) (↑s : M) : N) = (f : (a : M) → N) 0
rw₂ : Eq.{u_2 + 1} (α := N) (0 : N) ((f : (a : M) → N) 0 : N)
⊢ f.mk' 0 s = 0
have rw₃ : Eq.{u_2 + 1} (α := N) 0 0
Tactic: rw [eq_comm, eq_mk'_iff_mul_eq, zero_mul, f.map_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
⊢ LE.le (α := Submonoid M) (nonZeroDivisors M) (comap f (nonZeroDivisors N))
have refine : ∀ (m : M) (hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m) (n : N)
  (h0 : HMul.hMul (β := N) n ((f : (a : M) → N) m : N) = 0), n = 0
Tactic: refine fun m hm ↦ nonZeroDivisorsRight_eq_nonZeroDivisors (M₀ := N) ▸ fun n h0 ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
h0 : HMul.hMul (β := N) n ((f : (a : M) → N) m : N) = 0
⊢ n = 0
have have : ∀ (ms : M × ↥S) (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1), n = 0
Tactic: have ⟨ms, eq⟩ := f.surj n
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
h0 : HMul.hMul (β := N) n ((f : (a : M) → N) m : N) = 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
⊢ n = 0
have h0₁ : ∃ (s : ↥S), (↑s : M) * (ms.1 * m) = 0
Tactic: rw [← (f.map_units ms.2).mul_left_eq_zero, mul_right_comm, eq, ← map_mul, map_eq_zero_iff] at h0
Cleared hypotheses: h0, eq
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
ms : M × ↥S
h0 : ∃ (s : ↥S), (↑s : M) * (ms.1 * m) = 0
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
⊢ n = 0
have h0₁ : ∃ (s : ↥S), (↑s : M) * ms.1 = 0
Tactic: simp_rw [← mul_assoc, mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hm.2] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h0 : ∃ (s : ↥S), (↑s : M) * ms.1 = 0
⊢ n = 0
have rwa : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = 0
Tactic: rwa [← (f.map_units ms.2).mul_left_eq_zero, eq, map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : Membership.mem (γ := Submonoid M) (nonZeroDivisors M) m
n : N
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h0 : ∃ (s : ↥S), (↑s : M) * ms.1 = 0
rwa : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = 0
⊢ n = 0
have rwa₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) ms.1 : N) (0 : N)
Tactic: rwa [← (f.map_units ms.2).mul_left_eq_zero, eq, map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
inst_2 : NoZeroDivisors M
⊢ NoZeroDivisors N
have refine : ∀ (n : N) (hn : n ≠ 0), Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n
Tactic: refine noZeroDivisors_iff_forall_mem_nonZeroDivisors.mpr fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
⊢ Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n
have have : ∀ (ms : M × ↥S) (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1),
  Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n
Tactic: have ⟨ms, eq⟩ := f.surj n
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h : ms.1 = 0
⊢ n = 0
have rwa : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) 0) (h : ms.1 = 0), n = 0
Tactic: rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at eq
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h : ms.1 = 0
rwa : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) 0) (h : ms.1 = 0), n = 0
⊢ n = 0
have rwa₁ : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = 0) (h : ms.1 = 0), n = 0
Tactic: rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at eq
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (goal)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
h : ms.1 = 0
rwa : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) 0) (h : ms.1 = 0), n = 0
rwa₁ : ∀ (eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = 0) (h : ms.1 = 0), n = 0
⊢ n = 0
have rwa₂ : ∀ (eq : n = 0) (h : ms.1 = 0), n = 0
Tactic: rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at eq
Cleared hypotheses: eq, h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero (hypothesis)
Goal:
M : Type u_1
inst : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoidWithZero N
f : S.LocalizationMap N
inst_2 : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : HMul.hMul (β := N) n ((f : (a : M) → N) (↑ms.2 : M) : N) = (f : (a : M) → N) ms.1
⊢ Membership.mem (γ := Submonoid N) (nonZeroDivisors N) n
have hs : ms.1 ≠ 0
Tactic: have hs : ms.1 ≠ 0 := fun h ↦ hn (by rwa [h, f.map_zero, (f.map_units _).mul_left_eq_zero] at eq)
-- 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_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₃ : α
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₁ : (↑c₂ : α) * d₁ * a₁ ≤ (↑a₂ : α) * c₁ * 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 : α
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₂ : (↑d₂ : α) * c₁ * a₁ ≤ (↑a₂ : α) * c₁ * 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₁
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₃ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * c₁ * 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₁
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₄ : (↑d₂ : α) * a₁ * c₁ ≤ (↑a₂ : α) * d₁ * c₁ ↔ (↑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₁
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₅ : (↑d₂ : α) * a₁ ≤ (↑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₁
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₆ : (↑b₂ : α) * ((↑d₂ : α) * a₁) ≤ (↑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₄ : α
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * c₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
have rw₇ : (↑d₂ : α) * ((↑b₂ : α) * a₁) ≤ (↑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]