awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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)
h₁ :
  ∀ (hb : 0 < a), (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)

Tactic:
rcases lt_or_gt_of_ne hb with (hb | hb)

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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 : (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)

Tactic:
right
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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)
h₁ h₂ : Iio (a⁻¹ * aU) = Iio (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Ioi_of_neg _ hb, div_eq_inv_mul]

Premises used: Set.preimage_const_mul_Ioi_of_neg, div_eq_inv_mul
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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 : (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Iio (a⁻¹ * aU)

Tactic:
left
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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)
h₁ h₂ : Ioi (a⁻¹ * aU) = Ioi (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Ioi aU = Ioi (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Ioi₀ _ hb, div_eq_inv_mul]

Premises used: Set.preimage_const_mul_Ioi₀, div_eq_inv_mul
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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 : (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU) ∨ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Tactic:
left
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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)
h₁ h₂ : Ioi (a⁻¹ * aU) = Ioi (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Ioi (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Iio_of_neg _ hb, div_eq_inv_mul]

Premises used: Set.preimage_const_mul_Iio_of_neg, div_eq_inv_mul
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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 : (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)

Tactic:
right
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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)
h₁ h₂ : Iio (a⁻¹ * aU) = Iio (a⁻¹ * aU)
⊢ (fun (x : α) ↦ a * x) ⁻¹' Iio aU = Iio (a⁻¹ * aU)

Tactic:
rw [Set.preimage_const_mul_Iio₀ _ hb, div_eq_inv_mul]

Premises used: Set.preimage_const_mul_Iio₀, div_eq_inv_mul
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : a = 0
⊢ (fun (x : α) ↦ x * a) '' [[b, c]] = [[b * a, c * a]]

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : ¬a = 0
⊢ Eq (α := Set α) ((fun (x : α) ↦ x * a⁻¹) ⁻¹' [[b, c]]) ((fun (x : α) ↦ x / a) ⁻¹' [[b, c]])

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
⊢ (fun (x : α) ↦ a * x) '' [[b, c]] = [[a * b, a * c]]

Tactic:
simpa only [mul_comm] using image_mul_const_uIcc a b c

Premises used: Set.image_mul_const_uIcc, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
⊢ (fun (x : α) ↦ x / a) '' [[b, c]] = [[b / a, c / a]]

Tactic:
simp only [div_eq_mul_inv, image_mul_const_uIcc]

Premises used: Set.image_mul_const_uIcc, div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
h : ∀ (x : α), x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹
⊢ (Ioo a 0)⁻¹ = Iio a⁻¹

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
⊢ x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹

Tactic:
⟨fun h ↦ (lt_inv_of_neg (inv_neg''.1 h.2) ha).2 h.1, fun h ↦ ?_⟩

Premises used: Iff.mpr, inv_neg'', And.right, And.left, Iff.intro, Iff.mp, lt_inv_of_neg
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
h : ∀ (h : x ∈ Iio a⁻¹), x ∈ (Ioo a 0)⁻¹
⊢ x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹

Tactic:
refine ⟨fun h ↦ (lt_inv_of_neg (inv_neg''.1 h.2) ha).2 h.1, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
⊢ x < 0

Tactic:
have h' := (h.trans (inv_neg''.2 ha))
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
h' : x < 0
⊢ x ∈ (Ioo a 0)⁻¹

Tactic:
⟨(lt_inv_of_neg ha h').2 h, inv_neg''.2 h'⟩

Premises used: Iff.mpr, Set.Mem, setOf, inv_neg'', Set.preimage, And.intro, lt_inv_of_neg, Set.Ioo
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
h' : x < 0
⊢ x ∈ (Ioo a 0)⁻¹

Tactic:
exact ⟨(lt_inv_of_neg ha h').2 h, inv_neg''.2 h'⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
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⁻¹⁻¹
rw₂ rw₃ : Iio a = Iio a
⊢ (Iio a)⁻¹ = Ioo a⁻¹ 0

Tactic:
rw [inv_eq_iff_eq_inv, inv_Ioo_0_right (inv_neg''.2 ha), inv_inv]

Premises used: Iff.mpr, Set.inv_Ioo_0_right, inv_neg'', inv_inv, inv_eq_iff_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a b c : α
c_in : c ∈ Ici (a * b)
⊢ a ∈ Ici a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a b : α
refine : ∀ (c : α) (c_in : c ∈ Ici (a * b)), ∃ y ∈ Ici b, a * y = c
⊢ Ici a * Ici b = Ici (a * b)

Tactic:
refine Subset.antisymm (Ici_mul_Ici_subset' ..) (subset_def ▸ fun c c_in ↦
    mem_mul.mpr ⟨a, ⟨by simp, ?_⟩⟩)

Premises used: Set.Subset.antisymm, Set.Ici_mul_Ici_subset'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a b c : α
c_in : c ∈ Ici (a * b)
obtain : ∀ (d : α) (hd : c = a * b * d), ∃ y ∈ Ici b, a * y = c
⊢ ∃ y ∈ Ici b, a * y = c

Tactic:
obtain ⟨d, hd⟩ := exists_mul_of_le <| mem_Ici.mp c_in

Premises used: Set.mem_Ici, Iff.mp, ExistsMulOfLE.exists_mul_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a b c : α
c_in : c ∈ Ici (a * b)
d : α
hd : c = a * b * d
⊢ b * d ∈ Ici b ∧ a * (b * d) = c

Tactic:
simp [← mul_assoc, hd]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a b c : α
c_in : c ∈ Ici (a * b)
d : α
hd : c = a * b * d
⊢ ∃ y ∈ Ici b, a * y = c

Tactic:
exact ⟨b * d, by simp [← mul_assoc, hd]⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a : α
h : Ne (α := ℕ) 1 0
⊢ HPow.hPow (β := ℕ) (Ici a) 1 = Ici (HPow.hPow (β := ℕ) a 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
inst_3 : MulRightMono α
a : α
n : ℕ
h : n + 2 ≠ 0
⊢ Ici a ^ (n + 2) = Ici (a ^ (n + 2))

Tactic:
simp [pow_succ _ n.succ, Ici_pow_eq, Ici_mul_Ici_eq]

Premises used: pow_succ, Set.Ici_mul_Ici_eq, Nat.succ
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_2
inst : Monoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
⊢ Eq.{u_2 + 1} (α := Set α) (Ici 1) univ

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁻ᵐ = a⁻¹ ⊔ 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁺ᵐ = a ⊔ 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
⊢ Monotone (β := α) fun (x : α) ↦ x⁺ᵐ

Tactic:
fun _a _b hab ↦ sup_le_sup_right hab _

Premises used: sup_le_sup_right, Monotone, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
⊢ Eq.{u_1 + 1} (α := α) 1⁺ᵐ 1

Tactic:
sup_idem _

Premises used: sup_idem
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
⊢ Eq.{u_1 + 1} (α := α) 1⁻ᵐ 1

Tactic:
simp [leOnePart]

Premises used: LeOnePart.leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ 1 ≤ a⁺ᵐ

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ 1 ≤ a⁻ᵐ

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a ≤ a⁺ᵐ

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁻¹ ≤ a⁻ᵐ

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁺ᵐ = a ↔ 1 ≤ a

Tactic:
sup_eq_left

Premises used: sup_eq_left
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁺ᵐ = 1 ↔ a ≤ 1

Tactic:
sup_eq_right

Premises used: sup_eq_right
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁻ᵐ = a⁻¹ ↔ 1 ≤ a⁻¹

Tactic:
sup_eq_left

Premises used: sup_eq_left
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁻ᵐ = 1 ↔ a⁻¹ ≤ 1

Tactic:
sup_eq_right

Premises used: sup_eq_right
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁺ᵐ ≤ 1 ↔ a ≤ 1

Tactic:
simp [oneLePart]

Premises used: OneLePart.oneLePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

Tactic:
simp [leOnePart]

Premises used: LeOnePart.leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
ha rwa rwa₁ rwa₂ rwa₃ : 1 < a
⊢ 1 < a⁺ᵐ

Tactic:
rwa [oneLePart_eq_self.2 ha.le]

Premises used: Iff.mpr, LT.lt.le, oneLePart_eq_self
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁻¹⁺ᵐ = a⁻ᵐ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
⊢ a⁻¹⁻ᵐ = a⁺ᵐ

Tactic:
simp [oneLePart, leOnePart]

Premises used: LeOnePart.leOnePart, OneLePart.oneLePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
⊢ (a ⊔ b)⁺ᵐ = a⁺ᵐ ⊔ b⁺ᵐ

Tactic:
simp [oneLePart, sup_sup_distrib_right]

Premises used: OneLePart.oneLePart, sup_sup_distrib_right
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
⊢ a⁻ᵐ = a⁻¹ ↔ a ≤ 1

Tactic:
simp [leOnePart]

Premises used: LeOnePart.leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
⊢ a⁻ᵐ = 1 ↔ 1 ≤ a

Tactic:
simp [leOnePart_eq_one']

Premises used: leOnePart_eq_one'
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
⊢ a⁻ᵐ ≤ 1 ↔ 1 ≤ a

Tactic:
simp [leOnePart]

Premises used: LeOnePart.leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a : α
inst_2 : MulLeftMono α
ha : a < 1
rwa : 1 < a⁻¹
rwa₁ rwa₂ rwa₃ rwa₄ : a < 1
⊢ 1 < a⁻ᵐ

Tactic:
rwa [leOnePart_eq_inv.2 ha.le, one_lt_inv']

Premises used: Iff.mpr, one_lt_inv', LT.lt.le, leOnePart_eq_inv
-- Module: Mathlib.Algebra.Order.Group.PosPart
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
rw₇ rw₈ : a ⊔ 1 = a ⊔ 1
⊢ 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]

Premises used: div_eq_mul_inv, mul_sup, sup_comm, oneLePart_def, leOnePart_def, mul_inv_cancel, mul_one, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a : α
rw : (a⁺ᵐ / a⁻ᵐ)⁻¹ = a⁻¹
rw₁ rw₂ : a⁻¹ = a⁻¹
⊢ a⁻ᵐ / a⁺ᵐ = a⁻¹

Tactic:
rw [← inv_div, oneLePart_div_leOnePart]

Premises used: inv_div, oneLePart_div_leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
simp : ∀ ⦃a₁ a₂ : α⦄, a₁⁺ᵐ = a₂⁺ᵐ → a₁⁻ᵐ = a₂⁻ᵐ → a₁ = a₂
⊢ Injective (β := α × α) fun (a : α) ↦ (a⁺ᵐ, a⁻ᵐ)

Tactic:
simp only [Injective, Prod.mk.injEq, and_imp]

Premises used: and_imp, Prod.mk.injEq, Function.Injective
-- Module: Mathlib.Algebra.Order.Group.PosPart
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⁻ᵐ
rw₃ rw₄ : b⁺ᵐ / b⁻ᵐ = b⁺ᵐ / b⁻ᵐ
⊢ a = b

Tactic:
rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b, hpos, hneg]

Premises used: oneLePart_div_leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
a b : α
inst_2 : MulLeftMono α
⊢ a⁺ᵐ = b⁺ᵐ ∧ a⁻ᵐ = b⁻ᵐ ↔ a = b

Tactic:
Prod.mk_inj.symm.trans oneLePart_leOnePart_injective.eq_iff

Premises used: oneLePart_leOnePart_injective, Function.Injective.eq_iff, Prod.mk_inj, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
⊢ Antitone.{u_1, u_1} (α := α) leOnePart

Tactic:
fun _a _b hab ↦ sup_le_sup_right (inv_le_inv_iff.2 hab) _

Premises used: Iff.mpr, sup_le_sup_right, inv_le_inv_iff, Antitone, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.PosPart
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
rw₅ rw₆ : a ⊓ 1 = a ⊓ 1
⊢ a⁻ᵐ = (a ⊓ 1)⁻¹

Tactic:
rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]

Premises used: inv_one, inv_sup, inv_inj, inv_inv, leOnePart_def
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : a ⊔ a⁻¹ ⊔ 1 = |a|ₘ
⊢ a⁺ᵐ * a⁻ᵐ = |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]

Premises used: Iff.mpr, le_sup_right, sup_assoc, sup_mul, mul_sup, sup_eq_right, oneLePart_def, leOnePart_def, mul_inv_cancel, mul_one, one_mul
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ a ⊔ a⁻¹ ⊔ 1 = |a|ₘ

Tactic:
sup_eq_left.2 <| one_le_mabs a

Premises used: Iff.mpr, sup_eq_left, one_le_mabs, mabs
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
⊢ a ⊔ a⁻¹ ⊔ 1 = |a|ₘ

Tactic:
exact sup_eq_left.2 <| one_le_mabs a

Premises used: Iff.mpr, sup_eq_left, one_le_mabs
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
rw : a ⊔ a⁻¹ ⊔ 1 = |a|ₘ
⊢ a⁻ᵐ * a⁺ᵐ = |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]

Premises used: Iff.mpr, inv_mul_cancel, le_sup_right, sup_assoc, sup_mul, mul_sup, sup_eq_right, oneLePart_def, leOnePart_def, mul_one, one_mul
-- Module: Mathlib.Algebra.Order.Group.PosPart
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)⁻¹⁻¹
rw₇ rw₈ : a ⊓ 1 = a ⊓ 1
⊢ a⁺ᵐ ⊓ 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]

Premises used: inf_mul, leOnePart_eq_inv_inf_one, mul_left_inj, div_eq_mul_inv, LeOnePart.leOnePart, Inv.inv, inv_inv, mul_inv_cancel, oneLePart_div_leOnePart, one_mul
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ (a ⊓ b)⁻ᵐ = a⁻ᵐ ⊔ b⁻ᵐ

Tactic:
simp [leOnePart, inv_inf, sup_sup_distrib_right]

Premises used: LeOnePart.leOnePart, inv_inf, sup_sup_distrib_right
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a ⊔ b = b * (a / b)⁺ᵐ

Tactic:
simp [oneLePart, mul_sup]

Premises used: mul_sup, OneLePart.oneLePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a ⊓ b = a / (a / b)⁺ᵐ

Tactic:
simp [oneLePart, div_sup, inf_comm]

Premises used: inf_comm, div_sup, OneLePart.oneLePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

Tactic:
⟨fun h ↦ ⟨oneLePart_mono h, leOnePart_anti h⟩, fun h ↦ ?_⟩

Premises used: oneLePart_mono, And.intro, Iff.intro, leOnePart_anti
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
refine : ∀ (h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ), a ≤ b
⊢ a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

Tactic:
refine ⟨fun h ↦ ⟨oneLePart_mono h, leOnePart_anti h⟩, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
rw : a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ
⊢ a ≤ b

Tactic:
rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b]

Premises used: oneLePart_div_leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ

Tactic:
div_le_div'' h.1 h.2

Premises used: div_le_div'', And.right, And.left
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ

Tactic:
exact div_le_div'' h.1 h.2

Premises used: div_le_div'', And.right, And.left
-- Module: Mathlib.Algebra.Order.Group.PosPart
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⁻ᵐ)
rw₃ rw₄ : |a|ₘ * a = |a|ₘ * a
⊢ |a|ₘ * a = HPow.hPow (β := ℕ) a⁺ᵐ 2

Tactic:
rw [sq, ← mul_mul_div_cancel a⁺ᵐ, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]

Premises used: mul_mul_div_cancel, sq, oneLePart_mul_leOnePart, OneLePart.oneLePart, oneLePart_div_leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : |a|ₘ * a = HPow.hPow (β := ℕ) a⁺ᵐ 2
rw₁ rw₂ : HPow.hPow (β := ℕ) a⁺ᵐ 2 = HPow.hPow (β := ℕ) a⁺ᵐ 2
⊢ a * |a|ₘ = HPow.hPow (β := ℕ) a⁺ᵐ 2

Tactic:
rw [mul_comm, mabs_mul_eq_oneLePart_sq]

Premises used: mabs_mul_eq_oneLePart_sq, mul_comm
-- Module: Mathlib.Algebra.Order.Group.PosPart
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⁻ᵐ)
rw₃ rw₄ : |a|ₘ / a = |a|ₘ / a
⊢ |a|ₘ / a = HPow.hPow (β := ℕ) a⁻ᵐ 2

Tactic:
rw [sq, ← mul_div_div_cancel, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]

Premises used: sq, oneLePart_mul_leOnePart, mul_div_div_cancel, oneLePart_div_leOnePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a : α
rw : a / |a|ₘ = (|a|ₘ / a)⁻¹
rw₁ rw₂ : a / |a|ₘ = a / |a|ₘ
⊢ a / |a|ₘ = (HPow.hPow (β := ℕ) a⁻ᵐ 2)⁻¹

Tactic:
rw [← mabs_div_eq_leOnePart_sq, inv_div]

Premises used: inv_div, mabs_div_eq_leOnePart_sq
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Group α
a b : α
⊢ (a ⊓ b)⁺ᵐ = a⁺ᵐ ⊓ b⁺ᵐ

Tactic:
simp [oneLePart, sup_inf_right]

Premises used: sup_inf_right, OneLePart.oneLePart
-- Module: Mathlib.Algebra.Order.Group.PosPart
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ (a ⊔ b)⁻ᵐ = a⁻ᵐ ⊓ b⁻ᵐ

Tactic:
simp [leOnePart, inv_sup, sup_inf_right]

Premises used: inv_sup, sup_inf_right, LeOnePart.leOnePart