awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
simp : b + (↑⌊(a + p - b) / p⌋ : α) * p = a + p - (a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p)
⊢ b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - (↑⌊(a + p - b) / p⌋ : α)) * p

Tactic:
simp [field, -Int.self_sub_floor]

Premises used: Int.self_sub_floor
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b + (↑⌊(a + p - b) / p⌋ : α) * p = a + p - (a + p - b - (↑⌊(a + p - b) / p⌋ : α) * p)

Tactic:
ring
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
b : α
⊢ toIcoMod (p := 1) ⋯ 0 b = Int.fract b

Tactic:
simp [toIcoMod_eq_add_fract_mul]

Premises used: toIcoMod_eq_add_fract_mul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ioc (a + n • p) (a + (n + 1) • p)) univ

Tactic:
eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall, Set.mem_iUnion
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a : α
refine : ∀ (b : α), ∃ (i : ℤ), b ∈ Ioc (a + i • p) (a + (i + 1) • p)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ioc (a + n • p) (a + (n + 1) • p)) univ

Tactic:
refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall, Set.mem_iUnion
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ a < b - toIocDiv hp a b • p

Tactic:
rcases sub_toIocDiv_zsmul_mem_Ioc hp a b with ⟨hl, hr⟩

Premises used: sub_toIocDiv_zsmul_mem_Ioc
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
⊢ b - toIocDiv hp a b • p ≤ a + p

Tactic:
rcases sub_toIocDiv_zsmul_mem_Ioc hp a b with ⟨hl, hr⟩

Premises used: sub_toIocDiv_zsmul_mem_Ioc
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ ∃ (i : ℤ), b ∈ Ioc (a + i • p) (a + (i + 1) • p)

Tactic:
⟨toIocDiv hp a b, ⟨lt_sub_iff_add_lt.mp hl, ?_⟩⟩

Premises used: And.intro, Exists.intro, Iff.mp, lt_sub_iff_add_lt, toIocDiv
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
refine : b ≤ a + (toIocDiv hp a b + 1) • p
⊢ ∃ (i : ℤ), b ∈ Ioc (a + i • p) (a + (i + 1) • p)

Tactic:
refine ⟨toIocDiv hp a b, ⟨lt_sub_iff_add_lt.mp hl, ?_⟩⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
rw : b ≤ a + toIocDiv hp a b • p + p
⊢ b ≤ a + (toIocDiv hp a b + 1) • p

Tactic:
rw [add_smul, one_smul, ← add_assoc]

Premises used: add_assoc, one_smul, add_smul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + p + toIocDiv hp a b • p

Tactic:
sub_le_iff_le_add.mp hr

Premises used: sub_le_iff_le_add, Iff.mp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
h : a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p
⊢ b ≤ a + toIocDiv hp a b • p + p

Tactic:
convert! sub_le_iff_le_add.mp hr using 1

Premises used: sub_le_iff_le_add, Iff.mp
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ a + toIocDiv hp a b • p + p = a + p + toIocDiv hp a b • p

Tactic:
abel
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ico (a + n • p) (a + (n + 1) • p)) univ

Tactic:
eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall, Set.mem_iUnion
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a : α
refine : ∀ (b : α), ∃ (i : ℤ), b ∈ Ico (a + i • p) (a + (i + 1) • p)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ico (a + n • p) (a + (n + 1) • p)) univ

Tactic:
refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall, Set.mem_iUnion
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ a ≤ b - toIcoDiv hp a b • p

Tactic:
rcases sub_toIcoDiv_zsmul_mem_Ico hp a b with ⟨hl, hr⟩

Premises used: sub_toIcoDiv_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
⊢ b - toIcoDiv hp a b • p < a + p

Tactic:
rcases sub_toIcoDiv_zsmul_mem_Ico hp a b with ⟨hl, hr⟩

Premises used: sub_toIcoDiv_zsmul_mem_Ico
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ ∃ (i : ℤ), b ∈ Ico (a + i • p) (a + (i + 1) • p)

Tactic:
⟨toIcoDiv hp a b, ⟨le_sub_iff_add_le.mp hl, ?_⟩⟩

Premises used: toIcoDiv, And.intro, Exists.intro, Iff.mp, le_sub_iff_add_le
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
refine : b < a + (toIcoDiv hp a b + 1) • p
⊢ ∃ (i : ℤ), b ∈ Ico (a + i • p) (a + (i + 1) • p)

Tactic:
refine ⟨toIcoDiv hp a b, ⟨le_sub_iff_add_le.mp hl, ?_⟩⟩
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
rw : b < a + toIcoDiv hp a b • p + p
⊢ b < a + (toIcoDiv hp a b + 1) • p

Tactic:
rw [add_smul, one_smul, ← add_assoc]

Premises used: add_assoc, one_smul, add_smul
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + p + toIcoDiv hp a b • p

Tactic:
sub_lt_iff_lt_add.mp hr

Premises used: Iff.mp, sub_lt_iff_lt_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
h : a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p
⊢ b < a + toIcoDiv hp a b • p + p

Tactic:
convert! sub_lt_iff_lt_add.mp hr using 1

Premises used: Iff.mp, sub_lt_iff_lt_add
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p

Tactic:
abel
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Icc (a + n • p) (a + (n + 1) • p)) univ

Tactic:
simpa only [iUnion_Ioc_add_zsmul hp a, univ_subset_iff] using
    iUnion_mono fun n : ℤ => (Ioc_subset_Icc_self : Ioc (a + n • p) (a + (n + 1) • p) ⊆ Icc _ _)

Premises used: Set.univ_subset_iff, Set.Ioc_subset_Icc_self, iUnion_Ioc_add_zsmul, Set.iUnion_mono
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ioc (n • p) ((n + 1) • p)) univ

Tactic:
simpa only [zero_add] using iUnion_Ioc_add_zsmul hp 0

Premises used: iUnion_Ioc_add_zsmul, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ico (n • p) ((n + 1) • p)) univ

Tactic:
simpa only [zero_add] using iUnion_Ico_add_zsmul hp 0

Premises used: iUnion_Ico_add_zsmul, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
p : α
hp : 0 < p
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Icc (n • p) ((n + 1) • p)) univ

Tactic:
simpa only [zero_add] using iUnion_Icc_add_zsmul hp 0

Premises used: iUnion_Icc_add_zsmul, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ioc (a + (↑n : α)) (a + (↑n : α) + 1)) univ

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    iUnion_Ioc_add_zsmul zero_lt_one a

Premises used: add_assoc, iUnion_Ioc_add_zsmul, Int.cast_add, zero_lt_one, zsmul_one, Int.cast_one
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ico (a + (↑n : α)) (a + (↑n : α) + 1)) univ

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    iUnion_Ico_add_zsmul zero_lt_one a

Premises used: add_assoc, Int.cast_add, iUnion_Ico_add_zsmul, zero_lt_one, zsmul_one, Int.cast_one
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
a : α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Icc (a + (↑n : α)) (a + (↑n : α) + 1)) univ

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    iUnion_Icc_add_zsmul zero_lt_one a

Premises used: add_assoc, Int.cast_add, iUnion_Icc_add_zsmul, zero_lt_one, zsmul_one, Int.cast_one
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ioc (↑n : α) (HAdd.hAdd (α := α) (↑n : α) 1)) univ

Tactic:
simpa only [zero_add] using iUnion_Ioc_add_intCast (0 : α)

Premises used: iUnion_Ioc_add_intCast, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Ico (↑n : α) (HAdd.hAdd (α := α) (↑n : α) 1)) univ

Tactic:
simpa only [zero_add] using iUnion_Ico_add_intCast (0 : α)

Premises used: iUnion_Ico_add_intCast, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ToIntervalMod
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℤ), Icc (↑n : α) (HAdd.hAdd (α := α) (↑n : α) 1)) univ

Tactic:
simpa only [zero_add] using iUnion_Icc_add_intCast (0 : α)

Premises used: iUnion_Icc_add_intCast, zero_add, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
x : α
hs : IsUpperSet s
hx : 1 ≤ x
⊢ x • s ⊆ s

Tactic:
smul_set_subset_iff.2 fun _ ↦ hs <| le_mul_of_one_le_left' hx

Premises used: Iff.mpr, le_mul_of_one_le_left', Set.smul_set_subset_iff
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
x : α
hs : IsLowerSet s
hx : x ≤ 1
⊢ x • s ⊆ s

Tactic:
smul_set_subset_iff.2 fun _ ↦ hs <| mul_le_of_le_one_left' hx

Premises used: Iff.mpr, mul_le_of_le_one_left', Set.smul_set_subset_iff
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (a • s)

Tactic:
hs.image <| OrderIso.mulLeft _

Premises used: OrderIso.mulLeft, IsUpperSet.image
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
a : α
hs : IsLowerSet s
⊢ IsLowerSet (a • s)

Tactic:
hs.image <| OrderIso.mulLeft _

Premises used: OrderIso.mulLeft, IsLowerSet.image
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
a : α
hs : s.OrdConnected
rw : (a • (↑(upperClosure s) : Set α) ∩ a • (↑(lowerClosure s) : Set α)).OrdConnected
⊢ (a • s).OrdConnected

Tactic:
rw [← hs.upperClosure_inter_lowerClosure, smul_set_inter]

Premises used: Set.smul_set_inter, Set.OrdConnected.upperClosure_inter_lowerClosure
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
a : α
hs : s.OrdConnected
⊢ (a • (↑(upperClosure s) : Set α) ∩ a • (↑(lowerClosure s) : Set α)).OrdConnected

Tactic:
(upperClosure _).upper.smul.ordConnected.inter (lowerClosure _).lower.smul.ordConnected

Premises used: IsLowerSet.smul, IsLowerSet.ordConnected, upperClosure, IsUpperSet.smul, IsUpperSet.ordConnected, Set.OrdConnected.inter, UpperSet.upper, LowerSet.lower, lowerClosure
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
a : α
hs : s.OrdConnected
⊢ (a • (↑(upperClosure s) : Set α) ∩ a • (↑(lowerClosure s) : Set α)).OrdConnected

Tactic:
exact (upperClosure _).upper.smul.ordConnected.inter (lowerClosure _).lower.smul.ordConnected

Premises used: IsLowerSet.smul, IsLowerSet.ordConnected, upperClosure, IsUpperSet.smul, IsUpperSet.ordConnected, Set.OrdConnected.inter, UpperSet.upper, LowerSet.lower, lowerClosure
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
rw : IsUpperSet.{u_1} (α := α) (⋃ a ∈ s, a • t)
⊢ IsUpperSet (s * t)

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]

Premises used: Set.iUnion_smul_set, smul_eq_mul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsUpperSet.{u_1} (α := α) (⋃ a ∈ s, a • t)

Tactic:
isUpperSet_iUnion₂ fun x _ ↦ ht.smul

Premises used: isUpperSet_iUnion₂, IsUpperSet.smul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsUpperSet.{u_1} (α := α) (⋃ a ∈ s, a • t)

Tactic:
exact isUpperSet_iUnion₂ fun x _ ↦ ht.smul

Premises used: isUpperSet_iUnion₂, IsUpperSet.smul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
rw : IsUpperSet (t * s)
⊢ IsUpperSet (s * t)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)

Tactic:
hs.mul_left

Premises used: IsUpperSet.mul_left
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)

Tactic:
exact hs.mul_left

Premises used: IsUpperSet.mul_left
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsLowerSet t
⊢ IsLowerSet (s * t)

Tactic:
ht.toDual.mul_left

Premises used: Set.Mem, setOf, IsUpperSet.mul_left, Set.preimage, IsLowerSet, IsLowerSet.toDual, OrderDual
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsLowerSet s
⊢ IsLowerSet (s * t)

Tactic:
hs.toDual.mul_right

Premises used: Set.Mem, IsUpperSet.mul_right, setOf, Set.preimage, IsLowerSet, IsLowerSet.toDual, OrderDual
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsUpperSet s
⊢ IsLowerSet s⁻¹

Tactic:
fun _ _ h ↦ hs <| inv_le_inv' h

Premises used: Set.Mem, setOf, Set.preimage, IsLowerSet, inv_le_inv'
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s : Set α
hs : IsLowerSet s
⊢ IsUpperSet s⁻¹

Tactic:
fun _ _ h ↦ hs <| inv_le_inv' h

Premises used: Set.Mem, setOf, IsUpperSet, Set.preimage, inv_le_inv'
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
rw : IsLowerSet (s * t⁻¹)
⊢ IsLowerSet (s / t)

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsLowerSet (s * t⁻¹)

Tactic:
ht.inv.mul_left

Premises used: IsUpperSet.inv, IsLowerSet.mul_left
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsUpperSet t
⊢ IsLowerSet (s * t⁻¹)

Tactic:
exact ht.inv.mul_left

Premises used: IsUpperSet.inv, IsLowerSet.mul_left
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
rw : IsUpperSet (s * t⁻¹)
⊢ IsUpperSet (s / t)

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s * t⁻¹)

Tactic:
hs.mul_right

Premises used: IsUpperSet.mul_right
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s * t⁻¹)

Tactic:
exact hs.mul_right

Premises used: IsUpperSet.mul_right
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_2
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
s t : Set α
ht : IsLowerSet t
⊢ IsUpperSet (s / t)

Tactic:
ht.toDual.div_left

Premises used: Set.Mem, setOf, IsUpperSet, Set.preimage, IsUpperSet.div_left, IsLowerSet.toDual, OrderDual
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
hs : IsLowerSet s
⊢ IsLowerSet (s / t)

Tactic:
hs.toDual.div_right

Premises used: Set.Mem, setOf, IsUpperSet.div_right, Set.preimage, IsLowerSet, IsLowerSet.toDual, OrderDual
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
⊢ (↑1 : Set α) = Set.Ici 1

Tactic:
rfl

Premises used: Set.Ici, setOf, rfl
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : UpperSet α
⊢ (↑(s * t) : Set α) = (↑s : Set α) * (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : UpperSet α
⊢ (↑(s / t) : Set α) = (↑s : Set α) / (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
⊢ Eq.{u_1 + 1} (α := UpperSet α) (Ici 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : UpperSet α
rw : ⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) (Set.Ici 1) a), a • (↑s : Set α) ⊆ (↑s : Set α)
⊢ Set.Ici 1 * (↑s : Set α) ⊆ (↑s : Set α)

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]

Premises used: Set.iUnion_smul_set, smul_eq_mul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : UpperSet α
⊢ ⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) (Set.Ici 1) a), a • (↑s : Set α) ⊆ (↑s : Set α)

Tactic:
Set.iUnion₂_subset fun _ ↦ s.upper.smul_subset

Premises used: Set.iUnion₂_subset, UpperSet.upper, IsUpperSet.smul_subset
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : UpperSet α
⊢ ⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) (Set.Ici 1) a), a • (↑s : Set α) ⊆ (↑s : Set α)

Tactic:
exact Set.iUnion₂_subset fun _ ↦ s.upper.smul_subset

Premises used: Set.iUnion₂_subset, UpperSet.upper, IsUpperSet.smul_subset
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s_1 t : Set α
a : α
s : UpperSet α
rw : 1 * s = s
⊢ s * 1 = s

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s_1 t : Set α
a : α
s : UpperSet α
⊢ 1 * s = s

Tactic:
one_mul _

Premises used: _private.0.UpperSet.one_mul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s_1 t : Set α
a : α
s : UpperSet α
⊢ 1 * s = s

Tactic:
exact one_mul _

Premises used: _private.0.UpperSet.one_mul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : LowerSet α
⊢ (↑(s * t) : Set α) = (↑s : Set α) * (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : LowerSet α
⊢ (↑(s / t) : Set α) = (↑s : Set α) / (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
⊢ Eq.{u_1 + 1} (α := LowerSet α) (Iic 1) 1

Tactic:
rfl

Premises used: rfl