awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
M : Type u_3
inst : Mul M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
⊢ lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t)

Tactic:
subset_upperBounds_mul (M := Mᵒᵈ) _ _

Premises used: lowerBounds, Set.Mem, setOf, subset_upperBounds_mul, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
M : Type u_3
inst : Mul M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs : BddAbove s
ht : BddAbove t
⊢ BddAbove (s * t)

Tactic:
(Nonempty.mul hs ht).mono (subset_upperBounds_mul s t)

Premises used: Set.Nonempty.mul, subset_upperBounds_mul, BddAbove, Set.Nonempty.mono
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
M : Type u_3
inst : Mul M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs : BddBelow s
ht : BddBelow t
⊢ BddBelow (s * t)

Tactic:
(Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t)

Premises used: Set.Nonempty.mul, Set.Nonempty.mono, BddBelow, subset_lowerBounds_mul
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
ι : Type u_1
M : Type u_3
inst : Mul M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
f g : ι → M
hf : BddAbove (range f)
hg : BddAbove (range g)
⊢ BddAbove.{u_3} (α := M) (range fun (i : ι) ↦ f i * g i)

Tactic:
.range_comp (f := fun i ↦ (f i, g i)) (bddAbove_range_prod.2 ⟨hf, hg⟩)
    (monotone_fst.mul' monotone_snd)

Premises used: bddAbove_range_prod, Iff.mpr, monotone_fst, And.intro, Monotone.mul', monotone_snd, BddAbove.range_comp
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
ι : Type u_1
M : Type u_3
inst : Mul M
inst_1 : Preorder M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
f g : ι → M
hf : BddBelow (range f)
hg : BddBelow (range g)
⊢ BddBelow.{u_3} (α := M) (range fun (i : ι) ↦ f i * g i)

Tactic:
BddAbove.range_mul (M := Mᵒᵈ) hf hg

Premises used: lowerBounds, Set.Mem, setOf, BddBelow, OrderDual, BddAbove.range_mul
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
⊢ BddAbove s⁻¹ ↔ BddBelow s

Tactic:
(OrderIso.inv G).bddAbove_preimage

Premises used: lowerBounds, Set.Mem, OrderIso.inv, setOf, OrderIso.bddAbove_preimage, BddBelow, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
⊢ BddBelow s⁻¹ ↔ BddAbove s

Tactic:
(OrderIso.inv G).bddBelow_preimage

Premises used: Set.Mem, OrderIso.inv, setOf, OrderIso.bddBelow_preimage, upperBounds, BddAbove, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
h : BddAbove s
⊢ BddBelow s⁻¹

Tactic:
bddBelow_inv.2 h

Premises used: Iff.mpr, bddBelow_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
h : BddBelow s
⊢ BddAbove s⁻¹

Tactic:
bddAbove_inv.2 h

Premises used: Iff.mpr, bddAbove_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
a : G
⊢ IsLUB s⁻¹ a ↔ IsGLB s a⁻¹

Tactic:
(OrderIso.inv G).isLUB_preimage

Premises used: lowerBounds, Set.Mem, OrderIso.inv, setOf, upperBounds, IsGreatest, OrderIso.isLUB_preimage, IsGLB, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
a : G
⊢ IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a

Tactic:
(OrderIso.inv G).isLUB_preimage'

Premises used: lowerBounds, Set.Mem, OrderIso.inv, setOf, upperBounds, IsGreatest, IsGLB, OrderDual, OrderIso.isLUB_preimage'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
a : G
h : IsGLB s a
⊢ IsLUB s⁻¹ a⁻¹

Tactic:
isLUB_inv'.2 h

Premises used: Iff.mpr, isLUB_inv'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
a : G
⊢ IsGLB s⁻¹ a ↔ IsLUB s a⁻¹

Tactic:
(OrderIso.inv G).isGLB_preimage

Premises used: lowerBounds, Set.Mem, OrderIso.inv, setOf, OrderIso.isGLB_preimage, upperBounds, IsLeast, IsLUB, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
a : G
⊢ IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a

Tactic:
(OrderIso.inv G).isGLB_preimage'

Premises used: OrderIso.isGLB_preimage', lowerBounds, Set.Mem, OrderIso.inv, setOf, upperBounds, IsLeast, IsLUB, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s : Set G
a : G
h : IsLUB s a
⊢ IsGLB s⁻¹ a⁻¹

Tactic:
isGLB_inv'.2 h

Premises used: Iff.mpr, isGLB_inv'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
α : Type u_4
f : α → G
hf : BddBelow (range f)
⊢ BddAbove.{u_2} (α := G) (range fun (x : α) ↦ (f x)⁻¹)

Tactic:
hf.range_comp (OrderIso.inv G).monotone

Premises used: OrderIso.monotone, Set.Mem, OrderIso.inv, setOf, BddBelow.range_comp, upperBounds, BddAbove, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
α : Type u_4
f : α → G
hf : BddAbove (range f)
⊢ BddBelow.{u_2} (α := G) (range fun (x : α) ↦ (f x)⁻¹)

Tactic:
BddBelow.range_inv (G := Gᵒᵈ) hf

Premises used: lowerBounds, Set.Mem, setOf, BddBelow, BddBelow.range_inv, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsLUB t b
⊢ IsLUB (s * t) (a * b)

Tactic:
isLUB_image2_of_isLUB_isLUB (fun _ => (OrderIso.mulRight _).to_galoisConnection)
    (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs ht

Premises used: OrderIso.mulLeft, OrderIso.to_galoisConnection, OrderIso.mulRight, isLUB_image2_of_isLUB_isLUB
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s t : Set G
a b : G
hs : IsGLB s a
ht : IsGLB t b
⊢ IsGLB (s * t) (a * b)

Tactic:
IsLUB.mul (G := Gᵒᵈ) hs ht

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsLUB.mul, IsGreatest, IsGLB, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
rw : IsLUB (s * t⁻¹) (a * b⁻¹)
⊢ IsLUB (s / t) (a / b)

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s * t⁻¹) (a * b⁻¹)

Tactic:
hs.mul ht.inv

Premises used: IsLUB.mul, IsGLB.inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s * t⁻¹) (a * b⁻¹)

Tactic:
exact hs.mul ht.inv

Premises used: IsLUB.mul, IsGLB.inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds
Goal:
G : Type u_2
inst : Group G
inst_1 : Preorder G
inst_2 : MulLeftMono G
inst_3 : MulRightMono G
s t : Set G
a b : G
hs : IsGLB s a
ht : IsLUB t b
⊢ IsGLB (s / t) (a / b)

Tactic:
IsLUB.div (G := Gᵒᵈ) hs ht

Premises used: lowerBounds, Set.Mem, setOf, upperBounds, IsGreatest, IsGLB, OrderDual, IsLUB.div
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : One M
⊢ Eq.{u_1 + 1} (α := M) (sSup 1) 1

Tactic:
csSup_singleton _

Premises used: csSup_singleton
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : One M
⊢ Eq.{u_1 + 1} (α := M) (sInf 1) 1

Tactic:
csInf_singleton _

Premises used: csInf_singleton
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
rw : sSup ((fun (x : M) ↦ x⁻¹) '' s) = (sInf s)⁻¹
⊢ sSup s⁻¹ = (sInf s)⁻¹

Tactic:
rw [← image_inv_eq_inv]

Premises used: Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
⊢ sSup ((fun (x : M) ↦ x⁻¹) '' s) = (sInf s)⁻¹

Tactic:
((OrderIso.inv _).map_csInf' hs₀ hs₁).symm

Premises used: OrderIso.map_csInf', OrderDual, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
⊢ sSup ((fun (x : M) ↦ x⁻¹) '' s) = (sInf s)⁻¹

Tactic:
exact ((OrderIso.inv _).map_csInf' hs₀ hs₁).symm

Premises used: OrderIso.map_csInf', Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
rw : sInf ((fun (x : M) ↦ x⁻¹) '' s) = (sSup s)⁻¹
⊢ sInf s⁻¹ = (sSup s)⁻¹

Tactic:
rw [← image_inv_eq_inv]

Premises used: Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
⊢ sInf ((fun (x : M) ↦ x⁻¹) '' s) = (sSup s)⁻¹

Tactic:
((OrderIso.inv _).map_csSup' hs₀ hs₁).symm

Premises used: OrderIso.map_csSup', OrderDual, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
⊢ sInf ((fun (x : M) ↦ x⁻¹) '' s) = (sSup s)⁻¹

Tactic:
exact ((OrderIso.inv _).map_csSup' hs₀ hs₁).symm

Premises used: OrderIso.map_csSup', Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sSup (s * t) = sSup s * sSup t

Tactic:
csSup_image2_eq_csSup_csSup (fun _ => (OrderIso.mulRight _).to_galoisConnection)
    (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs₀ hs₁ ht₀ ht₁

Premises used: OrderIso.mulLeft, csSup_image2_eq_csSup_csSup, OrderIso.to_galoisConnection, OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sInf (s * t) = sInf s * sInf t

Tactic:
csInf_image2_eq_csInf_csInf (fun _ => (OrderIso.mulRight _).symm.to_galoisConnection)
    (fun _ => (OrderIso.mulLeft _).symm.to_galoisConnection) hs₀ hs₁ ht₀ ht₁

Premises used: OrderIso.mulLeft, OrderIso.to_galoisConnection, OrderIso.symm, OrderIso.mulRight, csInf_image2_eq_csInf_csInf
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
rw : sSup (s * t⁻¹) = sSup s / sInf t
rw₁ : sSup s * sSup t⁻¹ = sSup s / sInf t
rw₂ : sSup s * (sInf t)⁻¹ = sSup s / sInf t
rw₃ rw₄ : sSup s * (sInf t)⁻¹ = sSup s * (sInf t)⁻¹
⊢ sSup (s / t) = sSup s / sInf t

Tactic:
rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv]

Premises used: Set.Nonempty.inv, csSup_mul, div_eq_mul_inv, csSup_inv, BddBelow.inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : ConditionallyCompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
rw : sInf (s * t⁻¹) = sInf s / sSup t
rw₁ : sInf s * sInf t⁻¹ = sInf s / sSup t
rw₂ : sInf s * (sSup t)⁻¹ = sInf s / sSup t
rw₃ rw₄ : sInf s * (sSup t)⁻¹ = sInf s * (sSup t)⁻¹
⊢ sInf (s / t) = sInf s / sSup t

Tactic:
rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]

Premises used: Set.Nonempty.inv, csInf_mul, BddAbove.inv, div_eq_mul_inv, csInf_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : One M
⊢ Eq.{u_1 + 1} (α := M) (sSup 1) 1

Tactic:
sSup_singleton

Premises used: sSup_singleton
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : One M
⊢ Eq.{u_1 + 1} (α := M) (sInf 1) 1

Tactic:
sInf_singleton

Premises used: sInf_singleton
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
rw : ⨆ a ∈ s, a⁻¹ = (sInf s)⁻¹
⊢ sSup s⁻¹ = (sInf s)⁻¹

Tactic:
rw [← image_inv_eq_inv, sSup_image]

Premises used: sSup_image, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
⊢ ⨆ a ∈ s, a⁻¹ = (sInf s)⁻¹

Tactic:
((OrderIso.inv M).map_sInf _).symm

Premises used: iSup, OrderIso.inv, OrderIso.map_sInf, OrderDual, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
⊢ ⨆ a ∈ s, a⁻¹ = (sInf s)⁻¹

Tactic:
exact ((OrderIso.inv M).map_sInf _).symm

Premises used: OrderIso.inv, OrderIso.map_sInf, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
rw : ⨅ a ∈ s, a⁻¹ = (sSup s)⁻¹
⊢ sInf s⁻¹ = (sSup s)⁻¹

Tactic:
rw [← image_inv_eq_inv, sInf_image]

Premises used: sInf_image, Set.image_inv_eq_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
⊢ ⨅ a ∈ s, a⁻¹ = (sSup s)⁻¹

Tactic:
((OrderIso.inv M).map_sSup _).symm

Premises used: iInf, OrderIso.inv, OrderIso.map_sSup, OrderDual, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s : Set M
⊢ ⨅ a ∈ s, a⁻¹ = (sSup s)⁻¹

Tactic:
exact ((OrderIso.inv M).map_sSup _).symm

Premises used: OrderIso.inv, OrderIso.map_sSup, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
⊢ sSup (s * t) = sSup s * sSup t

Tactic:
(sSup_image2_eq_sSup_sSup fun _ => (OrderIso.mulRight _).to_galoisConnection) fun _ =>
    (OrderIso.mulLeft _).to_galoisConnection

Premises used: OrderIso.mulLeft, OrderIso.to_galoisConnection, sSup_image2_eq_sSup_sSup, OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
⊢ sInf (s * t) = sInf s * sInf t

Tactic:
(sInf_image2_eq_sInf_sInf fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) fun _ =>
    (OrderIso.mulLeft _).symm.to_galoisConnection

Premises used: OrderIso.mulLeft, sInf_image2_eq_sInf_sInf, OrderIso.to_galoisConnection, OrderIso.symm, OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
simp_rw : sSup (s * t⁻¹) = sSup s * (sInf t)⁻¹
simp_rw₁ : sSup s * sSup t⁻¹ = sSup s * (sInf t)⁻¹
⊢ sSup (s / t) = sSup s / sInf t

Tactic:
simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv]

Premises used: sSup_inv, sSup_mul, div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
Goal:
M : Type u_1
inst : CompleteLattice M
inst_1 : Group M
inst_2 : MulLeftMono M
inst_3 : MulRightMono M
s t : Set M
simp_rw : sInf (s * t⁻¹) = sInf s * (sSup t)⁻¹
simp_rw₁ : sInf s * sInf t⁻¹ = sInf s * (sSup t)⁻¹
⊢ sInf (s / t) = sInf s / sSup t

Tactic:
simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]

Premises used: sInf_mul, sInf_inv, div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c d y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Icc (a * c) (b * d)

Tactic:
⟨mul_le_mul' hya hzc, mul_le_mul' hyb hzd⟩

Premises used: Set.Mem, setOf, Set.Icc, And.intro, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c d y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Icc (a * c) (b * d)

Tactic:
exact ⟨mul_le_mul' hya hzc, mul_le_mul' hyb hzd⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iic b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Iic (a * b)

Tactic:
mul_le_mul' hya hzb

Premises used: Set.Mem, setOf, Set.Iic, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iic b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Iic (a * b)

Tactic:
exact mul_le_mul' hya hzb

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ici b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ici (a * b)

Tactic:
mul_le_mul' hya hzb

Premises used: Set.Ici, Set.Mem, setOf, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b y : α
hya : y ∈ Ici a
z : α
hzb : z ∈ Ici b
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ici (a * b)

Tactic:
exact mul_le_mul' hya hzb

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
⊢ MulLeftMono α

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this : MulLeftMono α
⊢ MulRightMono α

Tactic:
have := mulRightMono_of_mulRightStrictMono α
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this_1 : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ico (a * c) (b * d)

Tactic:
⟨mul_le_mul' hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩

Premises used: Set.Mem, setOf, Set.Ico, And.intro, mul_lt_mul_of_le_of_lt, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this_1 : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ico (a * c) (b * d)

Tactic:
exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this_1 : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ico (a * c) (b * d)

Tactic:
⟨mul_le_mul' hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩

Premises used: Set.Mem, setOf, Set.Ico, And.intro, mul_le_mul', mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this_1 : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c ≤ z
hzd : z ≤ d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ico (a * c) (b * d)

Tactic:
exact ⟨mul_le_mul' hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this_1 : MulLeftMono α
this : MulRightMono α
y : α
hya : a < y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ioo (a * c) (b * d)

Tactic:
⟨mul_lt_mul_of_lt_of_le hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩

Premises used: Set.Mem, setOf, And.intro, mul_lt_mul_of_le_of_lt, Set.Ioo, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this_1 : MulLeftMono α
this : MulRightMono α
y : α
hya : a < y
hyb : y ≤ b
z : α
hzc : c ≤ z
hzd : z < d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ioo (a * c) (b * d)

Tactic:
exact ⟨mul_lt_mul_of_lt_of_le hya hzc, mul_lt_mul_of_le_of_lt hyb hzd⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this_1 : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c < z
hzd : z ≤ d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ioo (a * c) (b * d)

Tactic:
⟨mul_lt_mul_of_le_of_lt hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩

Premises used: Set.Mem, setOf, And.intro, mul_lt_mul_of_le_of_lt, Set.Ioo, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c d : α
this_1 : MulLeftMono α
this : MulRightMono α
y : α
hya : a ≤ y
hyb : y < b
z : α
hzc : c < z
hzd : z ≤ d
⊢ (fun (x1 x2 : α) ↦ x1 * x2) y z ∈ Ioo (a * c) (b * d)

Tactic:
exact ⟨mul_lt_mul_of_le_of_lt hya hzc, mul_lt_mul_of_lt_of_le hyb hzd⟩
-- Module: Mathlib.Algebra.Order.Group.Pointwise.Interval
Goal:
α : Type u_1
inst : Mul α
inst_1 : PartialOrder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
⊢ MulRightMono α

Tactic:
have := mulRightMono_of_mulRightStrictMono α