awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
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)
⊢ (↑b₂ : α) * a₁ = (↑a₂ : α) * b₁

Tactic:
simp only [mul_right_inj] at he hf

Premises used: mul_right_inj
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
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₁
⊢ (↑d₂ : α) * c₁ = (↑c₂ : α) * d₁

Tactic:
simp only [mul_right_inj] at he hf

Premises used: mul_right_inj
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
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₁
rw₁₁ rw₁₂ : (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ ≤ (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ ≤ (↑a₂ : α) * 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]

Premises used: mul_le_mul_iff_right, mul_left_comm, mul_le_mul_iff_left, mul_right_comm, Subtype.val
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
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₂)
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₂
⊢ (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

Premises used: Localization.r_iff_exists, Iff.mp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
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)
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₂
⊢ (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

Premises used: Localization.r_iff_exists, Iff.mp
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
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₁
rw₁₁ rw₁₂ : (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁ ↔ (↑d₂ : α) * b₁ < (↑b₂ : α) * d₁
⊢ (↑c₂ : α) * a₁ < (↑a₂ : α) * 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]

Premises used: mul_lt_mul_iff_left, mul_left_comm, mul_right_comm, mul_lt_mul_iff_right, Subtype.val
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ mk a₁ a₂ ≤ mk b₁ b₂ ↔ (↑b₂ : α) * a₁ ≤ (↑a₂ : α) * b₁

Tactic:
Iff.rfl

Premises used: Localization.mk, Iff.rfl, Localization.rec, Localization.liftOn₂, Quotient.mk', Localization.liftOn, OreLocalization.oreDiv
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ mk a₁ a₂ < mk b₁ b₂ ↔ (↑b₂ : α) * a₁ < (↑a₂ : α) * b₁

Tactic:
Iff.rfl

Premises used: Localization.mk, Iff.rfl, Localization.rec, Localization.liftOn₂, Quotient.mk', Localization.liftOn, OreLocalization.oreDiv
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : mk a.1 a.2 ≤ mk b.1 b.2
hbc : mk b.1 b.2 ≤ mk c.1 c.2
simp :
  ∀ (hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1) (hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1),
    (↑c.2 : α) * a.1 ≤ (↑a.2 : α) * c.1
⊢ mk a.1 a.2 ≤ mk c.1 c.2

Tactic:
simp only [mk_le_mk] at hab hbc ⊢

Premises used: Localization.mk_le_mk
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
apply : α
apply₁ : (↑b.2 : α) * ((↑c.2 : α) * a.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
⊢ (↑c.2 : α) * a.1 ≤ (↑a.2 : α) * c.1

Tactic:
apply le_of_mul_le_mul_left' _

Premises used: le_of_mul_le_mul_left'
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
⊢ α

Tactic:
exact ↑b.2

Premises used: Prod.snd
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
grw : (↑c.2 : α) * ((↑a.2 : α) * b.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
⊢ (↑b.2 : α) * ((↑c.2 : α) * a.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)

Tactic:
grw [mul_left_comm, hab]

Premises used: mul_left_comm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
hbc : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
rwa : (↑a.2 : α) * ((↑c.2 : α) * b.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)
rwa₁ : (↑a.2 : α) * ((↑c.2 : α) * b.1) ≤ (↑a.2 : α) * ((↑b.2 : α) * c.1)
rwa₂ rwa₃ rwa₄ rwa₅ : (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
⊢ (↑c.2 : α) * ((↑a.2 : α) * b.1) ≤ (↑b.2 : α) * ((↑a.2 : α) * c.1)

Tactic:
rwa [mul_left_comm, mul_left_comm (b.2 : α), mul_le_mul_iff_left]

Premises used: mul_left_comm, mul_le_mul_iff_left, Subtype.val, Prod.snd
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a b : Localization s
f : ∀ (a : α) (b_1 : ↥s), mk a b_1 ≤ b → b ≤ mk a b_1 → mk a b_1 = b
H :
  ∀ {a c : α} {b_1 d : ↥s} (h : (r s : (a : α × ↥s) → α × ↥s → Prop) (a, b_1) (c, d)),
    Eq (α := mk c d ≤ b → b ≤ mk c d → mk c d = b) ⋯ ⋯
⊢ a ≤ b → b ≤ a → a = b

Tactic:
induction a using Localization.rec
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a : α
b_1 : ↥s
f : ∀ (a_1 : α) (b : ↥s), mk a b_1 ≤ mk a_1 b → mk a_1 b ≤ mk a b_1 → mk a b_1 = mk a_1 b
f₁ :
  ∀ {a_1 c : α} {b d : ↥s} (h : (r s : (a : α × ↥s) → α × ↥s → Prop) (a_1, b) (c, d)),
    Eq (α := mk a b_1 ≤ mk c d → mk c d ≤ mk a b_1 → mk a b_1 = mk c d) ⋯ ⋯
⊢ mk a b_1 ≤ b → b ≤ mk a b_1 → mk a b_1 = b

Tactic:
induction b using Localization.rec
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a : α
b : ↥s
a_1 : α
b_1 : ↥s
f :
  (↑b_1 : α) * a ≤ (↑b : α) * a_1 →
    (↑b : α) * a_1 ≤ (↑b_1 : α) * a → ∃ (c : ↥s), (↑c : α) * ((↑b_1 : α) * a) = (↑c : α) * ((↑b : α) * a_1)
⊢ mk a b ≤ mk a_1 b_1 → mk a_1 b_1 ≤ mk a b → mk a b = mk a_1 b_1

Tactic:
simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]

Premises used: Localization.mk_le_mk, Localization.r_iff_exists, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a : α
b : ↥s
a_1 : α
b_1 : ↥s
hab : (↑b_1 : α) * a ≤ (↑b : α) * a_1
hba : (↑b : α) * a_1 ≤ (↑b_1 : α) * a
rw rw₁ : (↑1 : α) * ((↑b : α) * a_1) = (↑1 : α) * ((↑b : α) * a_1)
⊢ (↑1 : α) * ((↑b_1 : α) * a) = (↑1 : α) * ((↑b : α) * a_1)

Tactic:
rw [hab.antisymm hba]

Premises used: LE.le.antisymm
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a : α
b : ↥s
a_1 : α
b_1 : ↥s
⊢ (↑b_1 : α) * a ≤ (↑b : α) * a_1 →
    (↑b : α) * a_1 ≤ (↑b_1 : α) * a → ∃ (c : ↥s), (↑c : α) * ((↑b_1 : α) * a) = (↑c : α) * ((↑b : α) * a_1)

Tactic:
exact fun hab hba => ⟨1, by rw [hab.antisymm hba]⟩
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a : α
b_1 : ↥s
f :
  ∀ {a_1 c : α} {b d : ↥s} (h : (r s : (a : α × ↥s) → α × ↥s → Prop) (a_1, b) (c, d)),
    Eq (α := mk a b_1 ≤ mk c d → mk c d ≤ mk a b_1 → mk a b_1 = mk c d) ⋯ ⋯
⊢ mk a b_1 ≤ b → b ≤ mk a b_1 → mk a b_1 = b

Tactic:
on_goal 1 =>
      induction b using Localization.rec
      · simp_rw [mk_le_mk, mk_eq_mk_iff, r_iff_exists]
        exact fun hab hba => ⟨1, by rw [hab.antisymm hba]⟩

Premises used: Localization.mk_le_mk, Localization.r_iff_exists, Localization.mk_eq_mk_iff
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
b : Localization s
a : α
b_1 : ↥s
a_1 c : α
b_2 d : ↥s
h : (r s : (a : α × ↥s) → α × ↥s → Prop) (a_1, b_2) (c, d)
⊢ Eq (α := mk a b_1 ≤ mk c d → mk c d ≤ mk a b_1 → mk a b_1 = mk c d) ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a b : Localization s
a_1 c : α
b_1 d : ↥s
h : (r s : (a : α × ↥s) → α × ↥s → Prop) (a_1, b_1) (c, d)
⊢ Eq (α := mk c d ≤ b → b ≤ mk c d → mk c d = b) ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 : Localization s
a b : α × ↥s
hab : mk a.1 a.2 ≤ mk b.1 b.2
c_1 : Localization s
c : α × ↥s
simp :
  ∀ (hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1),
    (↑b.2 : α) * a.1 * ((↑c.2 : α) * c.1) ≤ (↑a.2 : α) * b.1 * ((↑c.2 : α) * c.1)
⊢ mk a.1 a.2 * mk c.1 c.2 ≤ mk b.1 b.2 * mk c.1 c.2

Tactic:
simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ (c.2 : α)] at hab ⊢

Premises used: Localization.mk_le_mk, mul_mul_mul_comm, Localization.mk_mul, Subtype.val, Prod.snd, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 : Localization s
a b : α × ↥s
c_1 : Localization s
c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
⊢ (↑b.2 : α) * a.1 * ((↑c.2 : α) * c.1) ≤ (↑a.2 : α) * b.1 * ((↑c.2 : α) * c.1)

Tactic:
mul_le_mul_left hab _

Premises used: mul_le_mul_left
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 : Localization s
a b : α × ↥s
c_1 : Localization s
c : α × ↥s
hab : (↑b.2 : α) * a.1 ≤ (↑a.2 : α) * b.1
⊢ (↑b.2 : α) * a.1 * ((↑c.2 : α) * c.1) ≤ (↑a.2 : α) * b.1 * ((↑c.2 : α) * c.1)

Tactic:
exact mul_le_mul_left hab _

Premises used: mul_le_mul_left
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : mk a.1 a.2 * mk b.1 b.2 ≤ mk a.1 a.2 * mk c.1 c.2
simp :
  ∀ (hab : (↑a.2 : α) * a.1 * ((↑c.2 : α) * b.1) ≤ (↑a.2 : α) * a.1 * ((↑b.2 : α) * c.1)),
    (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1
⊢ mk b.1 b.2 ≤ mk c.1 c.2

Tactic:
simp only [mk_mul, mk_le_mk, Submonoid.coe_mul, mul_mul_mul_comm _ _ a.1] at hab ⊢

Premises used: Localization.mk_le_mk, mul_mul_mul_comm, Prod.fst, Localization.mk_mul, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑a.2 : α) * a.1 * ((↑c.2 : α) * b.1) ≤ (↑a.2 : α) * a.1 * ((↑b.2 : α) * c.1)
⊢ (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1

Tactic:
le_of_mul_le_mul_left' hab

Premises used: le_of_mul_le_mul_left'
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a_1 b_1 c_1 : Localization s
a b c : α × ↥s
hab : (↑a.2 : α) * a.1 * ((↑c.2 : α) * b.1) ≤ (↑a.2 : α) * a.1 * ((↑b.2 : α) * c.1)
⊢ (↑c.2 : α) * b.1 ≤ (↑b.2 : α) * c.1

Tactic:
exact le_of_mul_le_mul_left' hab

Premises used: le_of_mul_le_mul_left'
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ b_1 : ↥s
a b : α
⊢ LE.le (α := Localization s)
      (({ toFun := fun (a : α) ↦ mk a b_1, inj' := ⋯ : α ↪ Localization s } : (a : α) → Localization s) a :
        Localization s)
      (({ toFun := fun (a : α) ↦ mk a b_1, inj' := ⋯ : α ↪ Localization s } : (a : α) → Localization s) b :
        Localization s) ↔
    a ≤ b

Tactic:
simp [mk_le_mk]

Premises used: Localization.mk_le_mk
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a b : Localization s
x x_1 : α × ↥s
simp_rw : (↑x_1.2 : α) * x.1 ≤ (↑x.2 : α) * x_1.1 ∨ (↑x.2 : α) * x_1.1 ≤ (↑x_1.2 : α) * x.1
⊢ mk x.1 x.2 ≤ mk x_1.1 x_1.2 ∨ mk x_1.1 x_1.2 ≤ mk x.1 x.2

Tactic:
simp_rw [mk_le_mk]

Premises used: Localization.mk_le_mk
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a b : Localization s
x x_1 : α × ↥s
⊢ (↑x_1.2 : α) * x.1 ≤ (↑x.2 : α) * x_1.1 ∨ (↑x.2 : α) * x_1.1 ≤ (↑x_1.2 : α) * x.1

Tactic:
le_total _ _

Premises used: le_total
-- Module: Mathlib.GroupTheory.MonoidLocalization.Order
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedCancelMonoid α
s : Submonoid α
a b : Localization s
x x_1 : α × ↥s
⊢ (↑x_1.2 : α) * x.1 ≤ (↑x.2 : α) * x_1.1 ∨ (↑x.2 : α) * x_1.1 ≤ (↑x_1.2 : α) * x.1

Tactic:
exact le_total _ _

Premises used: le_total
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
a b : G
ha : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} a
hb : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} b
y : G
⊢ ⁅a, b * y * b⁻¹⁆ * ⁅b, y⁆ ∈ H

Tactic:
Subgroup.mul_mem _ (ha (b * y * b⁻¹)) (hb y)

Premises used: HMul.hMul, Inv.inv, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
a b : G
ha : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} a
hb : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} b
y : G
h : ⁅a * b, y⁆ = ⁅a, b * y * b⁻¹⁆ * ⁅b, y⁆
⊢ ⁅a * b, y⁆ ∈ H

Tactic:
convert! Subgroup.mul_mem _ (ha (b * y * b⁻¹)) (hb y) using 1

Premises used: HMul.hMul, Inv.inv, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
a b : G
ha : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} a
hb : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} b
y : G
⊢ ⁅a * b, y⁆ = ⁅a, b * y * b⁻¹⁆ * ⁅b, y⁆

Tactic:
group
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
y : G
⊢ Bracket.bracket (L := G) 1 y ∈ H

Tactic:
simp
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
hx : Membership.mem (γ := Set G) {x : G | ∀ (y : G), ⁅x, y⁆ ∈ H} x
y : G
⊢ ⁅x, y⁻¹⁆ ∈ H

Tactic:
specialize hx y⁻¹

Premises used: Inv.inv
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x y : G
hx : ⁅x, y⁻¹⁆ ∈ H
rw : ∀ (hx : x * y⁻¹ * (x⁻¹ * y) ∈ H), x⁻¹ * y * (x * y⁻¹) ∈ H
⊢ ⁅x⁻¹, y⁆ ∈ H

Tactic:
rw [commutatorElement_def, mul_assoc, inv_inv] at hx ⊢

Premises used: commutatorElement_def, mul_assoc, inv_inv
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x y : G
hx : x * y⁻¹ * (x⁻¹ * y) ∈ H
⊢ x⁻¹ * y * (x * y⁻¹) ∈ H

Tactic:
Subgroup.Normal.mem_comm inferInstance hx

Premises used: Set.Mem, inferInstance, Subgroup.Normal.mem_comm
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x y : G
hx : x * y⁻¹ * (x⁻¹ * y) ∈ H
⊢ x⁻¹ * y * (x * y⁻¹) ∈ H

Tactic:
exact Subgroup.Normal.mem_comm inferInstance hx

Premises used: inferInstance, Subgroup.Normal.mem_comm
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
⊢ x ∈ H.upperCentralSeriesStep ↔ ∀ (y : G), ⁅x, y⁆ ∈ H

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : ∀ (x : G), x ∈ H.upperCentralSeriesStep ↔ x ∈ comap (mk' H) (center (G ⧸ H))
⊢ H.upperCentralSeriesStep = comap (mk' H) (center (G ⧸ H))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
h :
  x ∈ H.upperCentralSeriesStep ↔
    ∀ (x_1 : G),
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑x_1 : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
        HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑x_1 : G ⧸ H)
⊢ x ∈ H.upperCentralSeriesStep ↔ x ∈ comap (mk' H) (center (G ⧸ H))

Tactic:
rw [mem_comap, mem_center_iff, forall_mk]

Premises used: Subgroup.mem_center_iff, Subgroup.mem_comap, QuotientGroup.forall_mk
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
⊢ x ∈ H.upperCentralSeriesStep ↔
    ∀ (x_1 : G),
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑x_1 : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
        HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑x_1 : G ⧸ H)

Tactic:
forall_congr' fun y => ?_

Premises used: Set.Mem, setOf, forall_congr'
-- Module: Mathlib.GroupTheory.Nilpotent
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
h :
  ∀ (y : G),
    ⁅x, y⁆ ∈ H ↔
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑y : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
        HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑y : G ⧸ H)
⊢ x ∈ H.upperCentralSeriesStep ↔
    ∀ (x_1 : G),
      HMul.hMul (α := G ⧸ H) (β := G ⧸ H) (↑x_1 : G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) =
        HMul.hMul (α := G ⧸ H) (β := G ⧸ H) ((mk' H : (a : G) → G ⧸ H) x : G ⧸ H) (↑x_1 : G ⧸ H)

Tactic:
refine forall_congr' fun y => ?_

Premises used: forall_congr'