awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⁻ᵐ⁻¹
rw₄ : a⁺ᵐ / a⁻ᵐ ⊓ 1 = a⁻ᵐ⁻¹
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1
have rw₅ : 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⁻ᵐ⁻¹
rw₄ : a⁺ᵐ / a⁻ᵐ ⊓ 1 = a⁻ᵐ⁻¹
rw₅ : a ⊓ 1 = a⁻ᵐ⁻¹
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1
have rw₆ : a ⊓ 1 = (a ⊓ 1)⁻¹⁻¹
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⁻ᵐ⁻¹
rw₄ : a⁺ᵐ / a⁻ᵐ ⊓ 1 = a⁻ᵐ⁻¹
rw₅ : a ⊓ 1 = a⁻ᵐ⁻¹
rw₆ : a ⊓ 1 = (a ⊓ 1)⁻¹⁻¹
⊢ a⁺ᵐ ⊓ a⁻ᵐ = 1
have rw₇ : a ⊓ 1 = a ⊓ 1
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 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
have refine : ∀ (h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ), a ≤ b
Tactic: refine ⟨fun h ↦ ⟨oneLePart_mono h, leOnePart_anti h⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a ≤ b
have rw : a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ
Tactic: rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
⊢ |a|ₘ * a = HPow.hPow (β := ℕ) a⁺ᵐ 2
have rw : |a|ₘ * a = a⁺ᵐ * a⁺ᵐ
Tactic: rw [sq, ← mul_mul_div_cancel a⁺ᵐ, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : |a|ₘ * a = a⁺ᵐ * a⁺ᵐ
⊢ |a|ₘ * a = HPow.hPow (β := ℕ) a⁺ᵐ 2
have rw₁ : |a|ₘ * a = a⁺ᵐ * a⁻ᵐ * (a⁺ᵐ / a⁻ᵐ)
Tactic: rw [sq, ← mul_mul_div_cancel a⁺ᵐ, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : |a|ₘ * a = a⁺ᵐ * a⁺ᵐ
rw₁ : |a|ₘ * a = a⁺ᵐ * a⁻ᵐ * (a⁺ᵐ / a⁻ᵐ)
c : α
⊢ |a|ₘ * a = HPow.hPow (β := ℕ) a⁺ᵐ 2
have rw₂ : |a|ₘ * a = |a|ₘ * (a⁺ᵐ / a⁻ᵐ)
Tactic: rw [sq, ← mul_mul_div_cancel a⁺ᵐ, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : |a|ₘ * a = a⁺ᵐ * a⁺ᵐ
rw₁ : |a|ₘ * a = a⁺ᵐ * a⁻ᵐ * (a⁺ᵐ / a⁻ᵐ)
c : α
rw₂ : |a|ₘ * a = |a|ₘ * (a⁺ᵐ / a⁻ᵐ)
⊢ |a|ₘ * a = HPow.hPow (β := ℕ) a⁺ᵐ 2
have rw₃ : |a|ₘ * a = |a|ₘ * a
Tactic: rw [sq, ← mul_mul_div_cancel a⁺ᵐ, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
⊢ a * |a|ₘ = HPow.hPow (β := ℕ) a⁺ᵐ 2
have rw : |a|ₘ * a = HPow.hPow (β := ℕ) a⁺ᵐ 2
Tactic: rw [mul_comm, mabs_mul_eq_oneLePart_sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : |a|ₘ * a = HPow.hPow (β := ℕ) a⁺ᵐ 2
⊢ a * |a|ₘ = HPow.hPow (β := ℕ) a⁺ᵐ 2
have rw₁ : HPow.hPow (β := ℕ) a⁺ᵐ 2 = HPow.hPow (β := ℕ) a⁺ᵐ 2
Tactic: rw [mul_comm, mabs_mul_eq_oneLePart_sq]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
⊢ |a|ₘ / a = HPow.hPow (β := ℕ) a⁻ᵐ 2
have rw : |a|ₘ / a = a⁻ᵐ * a⁻ᵐ
Tactic: rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : |a|ₘ / a = a⁻ᵐ * a⁻ᵐ
⊢ |a|ₘ / a = HPow.hPow (β := ℕ) a⁻ᵐ 2
have rw₁ : |a|ₘ / a = a⁺ᵐ * a⁻ᵐ / (a⁺ᵐ / a⁻ᵐ)
Tactic: rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : |a|ₘ / a = a⁻ᵐ * a⁻ᵐ
rw₁ : |a|ₘ / a = a⁺ᵐ * a⁻ᵐ / (a⁺ᵐ / a⁻ᵐ)
a₁ : α
⊢ |a|ₘ / a = HPow.hPow (β := ℕ) a⁻ᵐ 2
have rw₂ : |a|ₘ / a = |a|ₘ / (a⁺ᵐ / a⁻ᵐ)
Tactic: rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : |a|ₘ / a = a⁻ᵐ * a⁻ᵐ
rw₁ : |a|ₘ / a = a⁺ᵐ * a⁻ᵐ / (a⁺ᵐ / a⁻ᵐ)
a₁ : α
rw₂ : |a|ₘ / a = |a|ₘ / (a⁺ᵐ / a⁻ᵐ)
⊢ |a|ₘ / a = HPow.hPow (β := ℕ) a⁻ᵐ 2
have rw₃ : |a|ₘ / a = |a|ₘ / a
Tactic: rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
⊢ a / |a|ₘ = (HPow.hPow (β := ℕ) a⁻ᵐ 2)⁻¹
have rw : a / |a|ₘ = (|a|ₘ / a)⁻¹
Tactic: rw [← mabs_div_eq_leOnePart_sq, inv_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : a / |a|ₘ = (|a|ₘ / a)⁻¹
⊢ a / |a|ₘ = (HPow.hPow (β := ℕ) a⁻ᵐ 2)⁻¹
have rw₁ : a / |a|ₘ = a / |a|ₘ
Tactic: rw [← mabs_div_eq_leOnePart_sq, inv_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
⊢ a⁺ᵐ = if 1 ≤ a then a else 1
have rw : max a 1 = (fun (x1 x2 : α) ↦ max x1 x2) 1 a
Tactic: rw [oneLePart_def, ← maxDefault, ← sup_eq_maxDefault]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
ha : 1 < a⁺ᵐ
⊢ a⁺ᵐ = a
have ha₁ : 1 < a
Tactic: rw [oneLePart_def, right_lt_sup, not_le] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
⊢ a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1
have simp_rw : a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1
Tactic: simp_rw [← one_le_inv']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
⊢ a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1
have rw : max a⁻¹ 1 = (fun (x1 x2 : α) ↦ max x1 x2) 1 a⁻¹
Tactic: rw [leOnePart_def, ← maxDefault, ← sup_eq_maxDefault]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.PosPart (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : Group α
a b : α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
⊢ a⁻¹ < b ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b
have rw : b⁻¹ < a ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b
Tactic: rw [inv_lt']
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
⊢ |a / b|ₘ = |b / a|ₘ
have rw : |(a / b)⁻¹|ₘ = |b / a|ₘ
Tactic: rw [← mabs_inv, inv_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
rw : |(a / b)⁻¹|ₘ = |b / a|ₘ
⊢ |a / b|ₘ = |b / a|ₘ
have rw₁ : |b / a|ₘ = |b / a|ₘ
Tactic: rw [← mabs_inv, inv_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
inst_2 : MulLeftMono α
ha : 1 ≤ a
hab : a ≤ b
⊢ |a|ₘ ≤ |b|ₘ
have rwa : a ≤ |b|ₘ
Tactic: rwa [mabs_of_one_le ha, mabs_of_one_le (ha.trans hab)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ 1 ≤ |a|ₘ
have apply : 1 ≤ HPow.hPow (β := ℕ) |a|ₘ 2
Tactic: apply pow_two_semiclosed _
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ 1 ≤ HPow.hPow (β := ℕ) |a|ₘ 2
have rw : 1 ≤ (a ⊔ a⁻¹) * a⁻¹ ⊔ HPow.hPow (β := ℕ) a 2 ⊔ 1
Tactic: rw [mabs, pow_two, mul_sup, sup_mul, ← pow_two, inv_mul_cancel, sup_comm, ← sup_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ |a * b|ₘ ≤ |a|ₘ * |b|ₘ
have a₁ : a * b ≤ |a|ₘ * |b|ₘ
Tactic: apply sup_le
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
a₁ : a * b ≤ |a|ₘ * |b|ₘ
⊢ |a * b|ₘ ≤ |a|ₘ * |b|ₘ
have a₂ : (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ
Tactic: apply sup_le
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ
have a₁ : a⁻¹ * b⁻¹ ≤ |a|ₘ * |b|ₘ
Tactic: rw [mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ ||a|ₘ / |b|ₘ|ₘ ≤ |a / b|ₘ
have rw : |a|ₘ / |b|ₘ ≤ |a / b|ₘ ∧ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
Tactic: rw [mabs, sup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ ∧ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
have left : |a|ₘ / |b|ₘ ≤ |a / b|ₘ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
left : |a|ₘ / |b|ₘ ≤ |a / b|ₘ
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ ∧ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
have right : (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ
have left : |a|ₘ ≤ |a / b|ₘ * |b|ₘ
Tactic: apply div_le_iff_le_mul.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ |a|ₘ ≤ |a / b|ₘ * |b|ₘ
have h : a = a / b * b
Tactic: convert! mabs_mul_le (a / b) b
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a = a / b * b
have h : a = a
Tactic: rw [div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ (|a|ₘ / |b|ₘ)⁻¹ ≤ |a / b|ₘ
have right : |b|ₘ ≤ |b / a|ₘ * |a|ₘ
Tactic: rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, mabs_div_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ |b|ₘ ≤ |b / a|ₘ * |a|ₘ
have h : b = b / a * a
Tactic: convert! mabs_mul_le (b / a) a
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ b = b / a * a
have h : b = b
Tactic: rw [div_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ (a ⊔ b) / (a ⊓ b) = |b / a|ₘ
have simp_rw : a / b ⊔ b / a ⊔ 1 = |b / a|ₘ
Tactic: simp_rw [sup_div, div_inf, div_self', sup_comm, sup_sup_sup_comm, sup_idem]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a / b ⊔ b / a ⊔ 1 = |b / a|ₘ
have rw : 1 ≤ |b / a|ₘ
Tactic: rw [← inv_div, sup_comm (b := _ / _), ← mabs, sup_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ
have rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ
have rw₁ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ
have rw₂ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ
have rw₃ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * (a ⊔ b) * (a ⊓ b)⁻¹
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)
rw₃ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * (a ⊔ b) * (a ⊓ b)⁻¹
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ
have rw₄ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * (a ⊔ b) * (a ⊔ b))
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)
rw₃ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * (a ⊔ b) * (a ⊓ b)⁻¹
rw₄ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * (a ⊔ b) * (a ⊔ b))
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ
have rw₅ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * ((a ⊔ b) * (a ⊔ b)))
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)
rw₃ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * (a ⊔ b) * (a ⊓ b)⁻¹
rw₄ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * (a ⊔ b) * (a ⊔ b))
rw₅ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * ((a ⊔ b) * (a ⊔ b)))
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ
have rw₆ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * HPow.hPow (β := ℕ) (a ⊔ b) 2)
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)
rw₃ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b) * (a ⊔ b) * (a ⊔ b) * (a ⊓ b)⁻¹
rw₄ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * (a ⊔ b) * (a ⊔ b))
rw₅ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * ((a ⊔ b) * (a ⊔ b)))
rw₆ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = (a ⊓ b)⁻¹ * ((a ⊓ b) * HPow.hPow (β := ℕ) (a ⊔ b) 2)
⊢ HPow.hPow (β := ℕ) (a ⊔ b) 2 = a * b * |b / a|ₘ
have rw₇ : HPow.hPow (β := ℕ) (a ⊔ b) 2 = HPow.hPow (β := ℕ) (a ⊔ b) 2
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw₁ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw₂ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))⁻¹
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))⁻¹
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw₃ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)⁻¹
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))⁻¹
rw₃ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)⁻¹
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw₄ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b)⁻¹⁻¹ * (a ⊔ b)⁻¹)
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))⁻¹
rw₃ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)⁻¹
rw₄ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b)⁻¹⁻¹ * (a ⊔ b)⁻¹)
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw₅ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b) * (a ⊔ b)⁻¹)
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))⁻¹
rw₃ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)⁻¹
rw₄ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b)⁻¹⁻¹ * (a ⊔ b)⁻¹)
rw₅ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b) * (a ⊔ b)⁻¹)
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw₆ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * ((a ⊔ b) * ((a ⊓ b) * (a ⊔ b)⁻¹))
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Unbundled.Abs (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / |b / a|ₘ
rw₁ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) / ((a ⊔ b) / (a ⊓ b))
rw₂ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) / (a ⊓ b))⁻¹
rw₃ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊔ b) * (a ⊓ b)⁻¹)⁻¹
rw₄ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b)⁻¹⁻¹ * (a ⊔ b)⁻¹)
rw₅ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊔ b) * ((a ⊓ b) * (a ⊔ b)⁻¹)
rw₆ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * ((a ⊔ b) * ((a ⊓ b) * (a ⊔ b)⁻¹))
⊢ HPow.hPow (β := ℕ) (a ⊓ b) 2 = a * b / |b / a|ₘ
have rw₇ : HPow.hPow (β := ℕ) (a ⊓ b) 2 = (a ⊓ b) * (a ⊓ b)
Tactic: rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]