[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (a • s)
[PROOFSTEP]
rintro _ y hxy ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
y x : α
hx : x ∈ s
hxy : (fun x => a • x) x ≤ y
⊢ y ∈ a • s
[PROOFSTEP]
exact mem_smul_set_iff_inv_smul_mem.2 (hs (le_inv_mul_iff_mul_le.2 hxy) hx)
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : OrdConnected s
⊢ OrdConnected (a • s)
[PROOFSTEP]
rw [← hs.upperClosure_inter_lowerClosure, smul_set_inter]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : OrdConnected s
⊢ OrdConnected (a • ↑(upperClosure s) ∩ a • ↑(lowerClosure s))
[PROOFSTEP]
exact (upperClosure _).upper.smul.ordConnected.inter (lowerClosure _).lower.smul.ordConnected
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsUpperSet (s * t)
[PROOFSTEP]
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsUpperSet (⋃ (a : α) (_ : a ∈ s), a • t)
[PROOFSTEP]
exact isUpperSet_iUnion₂ fun x _ ↦ ht.smul
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (s * t)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)
[PROOFSTEP]
exact hs.mul_left
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsLowerSet (s / t)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsLowerSet (s * t⁻¹)
[PROOFSTEP]
exact ht.inv.mul_left
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (s / t)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (s * t⁻¹)
[PROOFSTEP]
exact hs.mul_right
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : UpperSet α
⊢ Set.Ici 1 * ↑s ⊆ ↑s
[PROOFSTEP]
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : UpperSet α
⊢ ⋃ (a : α) (_ : a ∈ Set.Ici 1), a • ↑s ⊆ ↑s
[PROOFSTEP]
exact Set.iUnion₂_subset fun _ ↦ s.upper.smul_subset
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
src✝ : CommSemigroup (UpperSet α) := commSemigroup
s : UpperSet α
⊢ s * 1 = s
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
src✝ : CommSemigroup (UpperSet α) := commSemigroup
s : UpperSet α
⊢ 1 * s = s
[PROOFSTEP]
exact one_mul _
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : LowerSet α
⊢ Set.Iic 1 * ↑s ⊆ ↑s
[PROOFSTEP]
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : LowerSet α
⊢ ⋃ (a : α) (_ : a ∈ Set.Iic 1), a • ↑s ⊆ ↑s
[PROOFSTEP]
exact Set.iUnion₂_subset fun _ ↦ s.lower.smul_subset
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
src✝ : CommSemigroup (LowerSet α) := commSemigroup
s : LowerSet α
⊢ s * 1 = s
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
src✝ : CommSemigroup (LowerSet α) := commSemigroup
s : LowerSet α
⊢ 1 * s = s
[PROOFSTEP]
exact one_mul _
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ s * ↑(upperClosure t) = ↑(upperClosure (s * t))
[PROOFSTEP]
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, upperClosure_iUnion, upperClosure_smul, UpperSet.coe_iInf₂]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ⋃ (a : α) (_ : a ∈ s), a • ↑(upperClosure t) = ⋃ (i : α) (_ : i ∈ s), ↑(i • upperClosure t)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))
[PROOFSTEP]
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul, LowerSet.coe_iSup₂]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ⋃ (a : α) (_ : a ∈ s), a • ↑(lowerClosure t) = ⋃ (i : α) (_ : i ∈ s), ↑(i • lowerClosure t)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(upperClosure s) * t = ↑(upperClosure (s * t))
[PROOFSTEP]
simp_rw [mul_comm _ t]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ t * ↑(upperClosure s) = ↑(upperClosure (t * s))
[PROOFSTEP]
exact mul_upperClosure _ _
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(lowerClosure s) * t = ↑(lowerClosure (s * t))
[PROOFSTEP]
simp_rw [mul_comm _ t]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ t * ↑(lowerClosure s) = ↑(lowerClosure (t * s))
[PROOFSTEP]
exact mul_lowerClosure _ _
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(upperClosure (s * t)) = ↑(upperClosure s * upperClosure t)
[PROOFSTEP]
rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(lowerClosure (s * t)) = ↑(lowerClosure s * lowerClosure t)
[PROOFSTEP]
rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]
