awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hU : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} U
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
inl : ∀ (aU : α) (haU : U = Ioi aU), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
have inr : ∀ (aU : α) (haU : U = Iio aU), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
Tactic: obtain ⟨aU, (haU | haU)⟩ := hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
have inl : ∃ (a_1 : α), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi a_1 ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio a_1
Tactic: simp only [hV, haU, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} V
have inr : ∃ (a_1 : α), (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi a_1 ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio a_1
Tactic: simp only [hV, haU, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
⊢ ∃ (a_1 : α), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi a_1 ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio a_1
have h : (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
Tactic: use a⁻¹ * aU
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
⊢ ∃ (a_1 : α), (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi a_1 ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio a_1
have h : (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
Tactic: use a⁻¹ * aU
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
have h : ∀ (hb : a < 0), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
Tactic: rcases lt_or_gt_of_ne hb with (hb | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
h :
  ∀ (hb : a < 0), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
have h₁ : ∀ (hb : 0 < a), (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
Tactic: rcases lt_or_gt_of_ne hb with (hb | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
have h : ∀ (hb : a < 0), (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
Tactic: rcases lt_or_gt_of_ne hb with (hb | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
h :
  ∀ (hb : a < 0), (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
have h₁ : ∀ (hb : 0 < a), (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
Tactic: rcases lt_or_gt_of_ne hb with (hb | hb)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
have h : (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
have h : Iio (aU / a) = Iio (a⁻¹ * aU)
Tactic: rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : a < 0
h : Iio (aU / a) = Iio (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
have h₁ : Iio (a⁻¹ * aU) = Iio (a⁻¹ * aU)
Tactic: rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : 0 < a
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)
have h : (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU)
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : 0 < a
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU)
have h : Ioi (aU / a) = Ioi (a⁻¹ * aU)
Tactic: rw [Set.preimage_const_mul_Ioi₀ _ hb, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
hb : 0 < a
h : Ioi (aU / a) = Ioi (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU)
have h₁ : Ioi (a⁻¹ * aU) = Ioi (a⁻¹ * aU)
Tactic: rw [Set.preimage_const_mul_Ioi₀ _ hb, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
have h : (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU)
Tactic: left
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU)
have h : Ioi (aU / a) = Ioi (a⁻¹ * aU)
Tactic: rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : a < 0
h : Ioi (aU / a) = Ioi (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU)
have h₁ : Ioi (a⁻¹ * aU) = Ioi (a⁻¹ * aU)
Tactic: rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : 0 < a
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
have h : (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
Tactic: right
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : 0 < a
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
have h : Iio (aU / a) = Iio (a⁻¹ * aU)
Tactic: rw [Set.preimage_const_mul_Iio₀ _ hb, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
hb_1 : a ≠ 0
U V : Set α
hV : V = (fun (x : α) ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
hb : 0 < a
h : Iio (aU / a) = Iio (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)
have h₁ : Iio (a⁻¹ * aU) = Iio (a⁻¹ * aU)
Tactic: rw [Set.preimage_const_mul_Iio₀ _ hb, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ (Ioo a 0)⁻¹ = Iio a⁻¹
have h : ∀ (x : α), x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
⊢ x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹
have h : ∀ (h : x ∈ Iio a⁻¹), x ∈ (Ioo a 0)⁻¹
Tactic: refine ⟨fun h ↦ (lt_inv_of_neg (inv_neg''.1 h.2) ha).2 h.1, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (hypothesis)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
⊢ x ∈ (Ioo a 0)⁻¹
have h' : x < 0
Tactic: have h' := (h.trans (inv_neg''.2 ha))
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
⊢ (Iio a)⁻¹ = Ioo a⁻¹ 0
have rw : Iio a = (Ioo a⁻¹ 0)⁻¹
Tactic: rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
rw : Iio a = (Ioo a⁻¹ 0)⁻¹
⊢ (Iio a)⁻¹ = Ioo a⁻¹ 0
have rw₁ : Iio a = Iio a⁻¹⁻¹
Tactic: rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
rw : Iio a = (Ioo a⁻¹ 0)⁻¹
rw₁ : Iio a = Iio a⁻¹⁻¹
⊢ (Iio a)⁻¹ = Ioo a⁻¹ 0
have rw₂ : Iio a = Iio a
Tactic: rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a b : α
⊢ Ici a * Ici b = Ici (a * b)
have refine : ∀ (c : α) (c_in : c ∈ Ici (a * b)), ∃ y ∈ Ici b, a * y = c
Tactic: refine Subset.antisymm (Ici_mul_Ici_subset' ..) (subset_def ▸ fun c c_in ↦
    mem_mul.mpr ⟨a, ⟨by simp, ?_⟩⟩)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Pointwise.Interval (goal)
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a b c : α
c_in : c ∈ Ici (a * b)
⊢ ∃ y ∈ Ici b, a * y = c
have obtain : ∀ (d : α) (hd : c = a * b * d), ∃ y ∈ Ici b, a * y = c
Tactic: obtain ⟨d, hd⟩ := exists_mul_of_le <| mem_Ici.mp c_in
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
ha : a < 1
⊢ 1 < a⁻ᵐ
have rwa : 1 < a⁻¹
Tactic: rwa [leOnePart_eq_inv.2 ha.le, one_lt_inv']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
⊢ a⁺ᵐ / a⁻ᵐ = a
have rw : a⁺ᵐ * a⁻ᵐ⁻¹ = a
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : a⁺ᵐ * a⁻ᵐ⁻¹ = a
⊢ a⁺ᵐ / a⁻ᵐ = a
have rw₁ : a⁺ᵐ = a * a⁻ᵐ
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : a⁺ᵐ * a⁻ᵐ⁻¹ = a
rw₁ : a⁺ᵐ = a * a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ = a
have rw₂ : a⁺ᵐ = a * (a⁻¹ ⊔ 1)
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : a⁺ᵐ * a⁻ᵐ⁻¹ = a
rw₁ : a⁺ᵐ = a * a⁻ᵐ
rw₂ : a⁺ᵐ = a * (a⁻¹ ⊔ 1)
⊢ a⁺ᵐ / a⁻ᵐ = a
have rw₃ : a⁺ᵐ = a * a⁻¹ ⊔ a * 1
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : a⁺ᵐ * a⁻ᵐ⁻¹ = a
rw₁ : a⁺ᵐ = a * a⁻ᵐ
rw₂ : a⁺ᵐ = a * (a⁻¹ ⊔ 1)
rw₃ : a⁺ᵐ = a * a⁻¹ ⊔ a * 1
⊢ a⁺ᵐ / a⁻ᵐ = a
have rw₄ : a⁺ᵐ = a * a⁻¹ ⊔ a
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : a⁺ᵐ * a⁻ᵐ⁻¹ = a
rw₁ : a⁺ᵐ = a * a⁻ᵐ
rw₂ : a⁺ᵐ = a * (a⁻¹ ⊔ 1)
rw₃ : a⁺ᵐ = a * a⁻¹ ⊔ a * 1
rw₄ : a⁺ᵐ = a * a⁻¹ ⊔ a
⊢ a⁺ᵐ / a⁻ᵐ = a
have rw₅ : a⁺ᵐ = 1 ⊔ a
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : a⁺ᵐ * a⁻ᵐ⁻¹ = a
rw₁ : a⁺ᵐ = a * a⁻ᵐ
rw₂ : a⁺ᵐ = a * (a⁻¹ ⊔ 1)
rw₃ : a⁺ᵐ = a * a⁻¹ ⊔ a * 1
rw₄ : a⁺ᵐ = a * a⁻¹ ⊔ a
rw₅ : a⁺ᵐ = 1 ⊔ a
⊢ a⁺ᵐ / a⁻ᵐ = a
have rw₆ : a⁺ᵐ = a ⊔ 1
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : a⁺ᵐ * a⁻ᵐ⁻¹ = a
rw₁ : a⁺ᵐ = a * a⁻ᵐ
rw₂ : a⁺ᵐ = a * (a⁻¹ ⊔ 1)
rw₃ : a⁺ᵐ = a * a⁻¹ ⊔ a * 1
rw₄ : a⁺ᵐ = a * a⁻¹ ⊔ a
rw₅ : a⁺ᵐ = 1 ⊔ a
rw₆ : a⁺ᵐ = a ⊔ 1
⊢ a⁺ᵐ / a⁻ᵐ = a
have rw₇ : a ⊔ 1 = a ⊔ 1
Tactic: rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
    sup_comm, oneLePart_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
⊢ a⁻ᵐ / a⁺ᵐ = a⁻¹
have rw : (a⁺ᵐ / a⁻ᵐ)⁻¹ = a⁻¹
Tactic: rw [← inv_div, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : (a⁺ᵐ / a⁻ᵐ)⁻¹ = a⁻¹
⊢ a⁻ᵐ / a⁺ᵐ = a⁻¹
have rw₁ : a⁻¹ = a⁻¹
Tactic: rw [← inv_div, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
⊢ Injective (β := α × α) fun (a : α) ↦ (a⁺ᵐ, a⁻ᵐ)
have simp : ∀ ⦃a₁ a₂ : α⦄, a₁⁺ᵐ = a₂⁺ᵐ → a₁⁻ᵐ = a₂⁻ᵐ → a₁ = a₂
Tactic: simp only [Injective, Prod.mk.injEq, and_imp]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
⊢ a = b
have rw : a⁺ᵐ / a⁻ᵐ = b
Tactic: rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b, hpos, hneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
rw : a⁺ᵐ / a⁻ᵐ = b
⊢ a = b
have rw₁ : a⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ
Tactic: rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b, hpos, hneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
rw : a⁺ᵐ / a⁻ᵐ = b
rw₁ : a⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ
⊢ a = b
have rw₂ : b⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ
Tactic: rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b, hpos, hneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a b : α
hpos : a⁺ᵐ = b⁺ᵐ
hneg : a⁻ᵐ = b⁻ᵐ
rw : a⁺ᵐ / a⁻ᵐ = b
rw₁ : a⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ
rw₂ : b⁺ᵐ / a⁻ᵐ = b⁺ᵐ / b⁻ᵐ
⊢ a = b
have rw₃ : b⁺ᵐ / b⁻ᵐ = b⁺ᵐ / b⁻ᵐ
Tactic: rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b, hpos, hneg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹
have rw : a⁻¹ ⊔ 1 = (a ⊓ 1)⁻¹
Tactic: rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : a⁻¹ ⊔ 1 = (a ⊓ 1)⁻¹
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹
have rw₁ : (a⁻¹ ⊔ 1)⁻¹ = (a ⊓ 1)⁻¹⁻¹
Tactic: rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : a⁻¹ ⊔ 1 = (a ⊓ 1)⁻¹
rw₁ : (a⁻¹ ⊔ 1)⁻¹ = (a ⊓ 1)⁻¹⁻¹
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹
have rw₂ : a⁻¹⁻¹ ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹
Tactic: rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : a⁻¹ ⊔ 1 = (a ⊓ 1)⁻¹
rw₁ : (a⁻¹ ⊔ 1)⁻¹ = (a ⊓ 1)⁻¹⁻¹
rw₂ : a⁻¹⁻¹ ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹
have rw₃ : a ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹
Tactic: rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : a⁻¹ ⊔ 1 = (a ⊓ 1)⁻¹
rw₁ : (a⁻¹ ⊔ 1)⁻¹ = (a ⊓ 1)⁻¹⁻¹
rw₂ : a⁻¹⁻¹ ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹
rw₃ : a ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹
have rw₄ : a ⊓ 1⁻¹ = a ⊓ 1
Tactic: rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : a⁻¹ ⊔ 1 = (a ⊓ 1)⁻¹
rw₁ : (a⁻¹ ⊔ 1)⁻¹ = (a ⊓ 1)⁻¹⁻¹
rw₂ : a⁻¹⁻¹ ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹
rw₃ : a ⊓ 1⁻¹ = (a ⊓ 1)⁻¹⁻¹
rw₄ : a ⊓ 1⁻¹ = a ⊓ 1
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹
have rw₅ : a ⊓ 1 = a ⊓ 1
Tactic: rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ a⁺ᵐ * a⁻ᵐ = |a|ₘ
have rw : a ⊔ a⁻¹ ⊔ 1 = |a|ₘ
Tactic: rw [oneLePart_def, sup_mul, one_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel, sup_assoc,
    ← sup_assoc a, sup_eq_right.2 le_sup_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ a⁻ᵐ * a⁺ᵐ = |a|ₘ
have rw : a ⊔ a⁻¹ ⊔ 1 = |a|ₘ
Tactic: rw [oneLePart_def, mul_sup, mul_one, leOnePart_def, sup_mul, one_mul, inv_mul_cancel, sup_assoc,
    ← @sup_assoc _ _ a, sup_eq_right.2 le_sup_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1
have rw : (a⁺ᵐ ⊓ a⁻ᵐ) * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
Tactic: rw [← mul_left_inj a⁻ᵐ⁻¹, inf_mul, one_mul, mul_inv_cancel, ← div_eq_mul_inv,
    oneLePart_div_leOnePart, leOnePart_eq_inv_inf_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : (a⁺ᵐ ⊓ a⁻ᵐ) * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1
have rw₁ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ a⁻ᵐ * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
Tactic: rw [← mul_left_inj a⁻ᵐ⁻¹, inf_mul, one_mul, mul_inv_cancel, ← div_eq_mul_inv,
    oneLePart_div_leOnePart, leOnePart_eq_inv_inf_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : (a⁺ᵐ ⊓ a⁻ᵐ) * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
rw₁ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ a⁻ᵐ * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1
have rw₂ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ a⁻ᵐ * a⁻ᵐ⁻¹ = a⁻ᵐ⁻¹
Tactic: rw [← mul_left_inj a⁻ᵐ⁻¹, inf_mul, one_mul, mul_inv_cancel, ← div_eq_mul_inv,
    oneLePart_div_leOnePart, leOnePart_eq_inv_inf_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : (a⁺ᵐ ⊓ a⁻ᵐ) * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
rw₁ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ a⁻ᵐ * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
rw₂ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ a⁻ᵐ * a⁻ᵐ⁻¹ = a⁻ᵐ⁻¹
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1
have rw₃ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ 1 = a⁻ᵐ⁻¹
Tactic: rw [← mul_left_inj a⁻ᵐ⁻¹, inf_mul, one_mul, mul_inv_cancel, ← div_eq_mul_inv,
    oneLePart_div_leOnePart, leOnePart_eq_inv_inf_one, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : (a⁺ᵐ ⊓ a⁻ᵐ) * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
rw₁ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ a⁻ᵐ * a⁻ᵐ⁻¹ = 1 * a⁻ᵐ⁻¹
rw₂ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ a⁻ᵐ * a⁻ᵐ⁻¹ = a⁻ᵐ⁻¹
rw₃ : a⁺ᵐ * a⁻ᵐ⁻¹ ⊓ 1 = a⁻ᵐ⁻¹
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1
have rw₄ : a⁺ᵐ / a⁻ᵐ ⊓ 1 = a⁻ᵐ⁻¹
Tactic: rw [← mul_left_inj a⁻ᵐ⁻¹, inf_mul, one_mul, mul_inv_cancel, ← div_eq_mul_inv,
    oneLePart_div_leOnePart, leOnePart_eq_inv_inf_one, inv_inv]