Built with Alectryon, running Lean4 v4.3.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
import Mathlib

set_option trace.Meta.Tactic.simp.rewrite true

set_option maxHeartbeats 400000

/--
Definition of supremum.
-/
def up_bounds {E : Type*} [LE E] (A : Set E) := {x : E |  a  A, a  x}

def is_sup {E : Type*} [LE E] (A : Set E) (a : E) := a  (up_bounds A)  x  (up_bounds A), a  x

/-
Addition between two elements of the same set.
-/
instance [OrderedAddCommGroup E] : HAdd (Set E) (Set E) (Set E) where
  hAdd A B := {x : E | a  A, b  B,  x = a + b}

/-
Multiplication between Real and Set.
-/
instance [HMul ℝ E E] : HMul ℝ (Set E) (Set E) where
  hMul c A := {x : E | a  A, x = c * a}

variable {E : Type*} [HMul ℝ E E] [OrderedAddCommGroup E]

variable [CovariantClass E E (fun a b => a + b) fun a b => a  b] [CovariantClass E E (Function.swap fun a b => a + b) fun a b => a  b]

/-
Properties on the multiplication between elements of E and absolute value of real number. This is verified for classical finite and infinite dimension spaces.
-/
variable (c : ℝ)
variable (le_mul_pos :  (a b : E), a  b  |c| * a  |c| * b)
variable (le_div_pos :  (a b : E), a  b  (1 / |c|) * a  (1 / |c|) * b)
variable (mul_assoc :  (b : E), |c| * (1 / |c| * b) = (|c| * |c|⁻¹) * b)
variable (one_mul :  (a : E), (1 : ℝ) * a = a)

/--
sup(|c| * A) = |c| * sup(A)
-/
theorem c_sup_A_eq_sup_cA (A : Set E) (a₁ : E) (hc : |c|  0) (h1 : is_sup A a₁) : is_sup (|c| * A) (|c| * a₁) :=

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

is_sup (|c| * A) (|c| * a₁)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

is_sup (|c| * A) (|c| * a₁)

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

a A, a a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

a A, a a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

a A, a a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
a: E
ain: a A

a a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

a A, a a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
a: E
ain: a A
up: a₁ up_bounds A
right✝: x up_bounds A, a₁ x

intro
a a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

a A, a a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
a: E
ain: a A
up: a₁ {x | a A, a x}
right✝: x up_bounds A, a₁ x

intro
a a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

a A, a a₁

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

is_sup (|c| * A) (|c| * a₁)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁

is_sup (|c| * A) (|c| * a₁)

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁

|c| * A = {x | a A, x = |c| * a}

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

is_sup (|c| * A) (|c| * a₁)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

|c| * a₁ up_bounds (|c| * A) x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

is_sup (|c| * A) (|c| * a₁)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

is_sup (|c| * A) (|c| * a₁)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ {x | a |c| * A, a x}
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ {x | a |c| * A, a x}
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
a |c| * A, a |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
a |c| * A, a |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac: E
acin: ac |c| * A

left
ac |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac: E
acin: ac |c| * A

left
ac |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac: E
acin: ac {x | a A, x = |c| * a}

left
ac |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac: E
acin: ac {x | a A, x = |c| * a}

left
ac |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac: E
acin: ac {x | a A, x = |c| * a}

left
ac |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac, x: E
xin: x A
hca: ac = |c| * x

left.intro.intro
ac |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac, x: E
xin: x A
hca: ac = |c| * x

left.intro.intro
ac |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac, x: E
xin: x A
hca: ac = |c| * x

left.intro.intro
|c| * x |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac, x: E
xin: x A
hca: ac = |c| * x

left.intro.intro
|c| * x |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac, x: E
xin: x A
hca: ac = |c| * x

left.intro.intro
|c| * x |c| * a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac, x: E
xin: x A
hca: ac = |c| * x

left.intro.intro
x a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
ac, x: E
xin: x A
hca: ac = |c| * x

left.intro.intro
x a₁
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

left
|c| * a₁ up_bounds (|c| * A)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
x up_bounds (|c| * A), |c| * a₁ x

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁

is_sup (|c| * A) (|c| * a₁)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: b up_bounds (|c| * A)

right
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: b {x | a |c| * A, a x}

right
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: b {x | a |c| * A, a x}

right
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

right
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

right
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

right
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

right
|c| * a₁ b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

( a |c| * A, a b) a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

( a |c| * A, a b) a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

( a |c| * A, a b) a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin, h: a |c| * A, a b

a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

( a |c| * A, a b) a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin, h: a |c| * A, a b

a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
h: a {x | a A, x = |c| * a}, a b

a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
h: a {x | a A, x = |c| * a}, a b

a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
h: a {x | a A, x = |c| * a}, a b

a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

( a |c| * A, a b) a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
h: a {x | a A, x = |c| * a}, a b
a: E
ain: a A

|c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

( a |c| * A, a b) a A, |c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
h: a {x | a A, x = |c| * a}, a b
a: E
ain: a A

|c| * a b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
h: a {x | a A, x = |c| * a}, a b
a: E
ain: a A

|c| * a |c| * A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
h: a {x | a A, x = |c| * a}, a b
a: E
ain: a A

|c| * a |c| * A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
h: a {x | a A, x = |c| * a}, a b
a: E
ain: a A

|c| * a |c| * A

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b

( a |c| * A, a b) a A, |c| * a b

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b

right
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b

right
|c| * a₁ b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b

a A, a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b

a A, a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b

a A, a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
a: E
ain: a A

a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b

a A, a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b

a A, a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

|c| * a |c| * (1 / |c| * b)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

|c| * a |c| * |c|⁻¹ * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

|c| * a 1 * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

a 1 / |c| * b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

|c| * a b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
a: E
ain: a A
rw_up_mul_set: |c| * a b

|c| * a b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: a₁ up_bounds A x up_bounds A, a₁ x
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b

right
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: x up_bounds A, a₁ x

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: x {x | a A, a x}, a₁ x

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: a₁ 1 / |c| * b

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
h1: is_sup A a₁
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}

right
x up_bounds (|c| * A), |c| * a₁ x
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: a₁ 1 / |c| * b

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: |c| * a₁ |c| * (1 / |c| * b)

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: a₁ 1 / |c| * b

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: |c| * a₁ |c| * |c|⁻¹ * b

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: a₁ 1 / |c| * b

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: |c| * a₁ 1 * b

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: a₁ 1 / |c| * b

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: |c| * a₁ b

right.intro
|c| * a₁ b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A: Set E
a₁: E
hc: |c| 0
up_A: a A, a a₁
rfl_mul: |c| * A = {x | a A, x = |c| * a}
b: E
bin: a |c| * A, a b
rw_up_mul_set: a A, |c| * a b
up_mul_set_to_up_set: a A, a 1 / |c| * b
left✝: a₁ up_bounds A
least: |c| * a₁ b

right.intro
|c| * a₁ b

Goals accomplished! 🐙

Goals accomplished! 🐙
/-- A ⊆ B ⇒ sup A ≤ sup B -/ theorem sup_incl_le (A B : Set E) (sup_a sup_b : E) (hA : is_sup A sup_a) (hB : is_sup B sup_b) (h_incl : A B) : sup_a sup_b :=

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B

sup_a sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_a sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B

sup_a sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_a sup_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_b up_bounds A
Warning: unused variable `B_least` [linter.unusedVariables]
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
h_incl: A B
A_el: x A, x B
B_up: sup_b up_bounds B
B_least: x up_bounds B, sup_b x

intro
sup_b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
h_incl: A B
A_el: x A, x B
B_up: sup_b up_bounds B
B_least: x up_bounds B, sup_b x

intro
sup_b {x | a A, a x}
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
h_incl: A B
A_el: x A, x B
B_up: sup_b up_bounds B
B_least: x up_bounds B, sup_b x
x: E
xin: x A

intro
x sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B

sup_b up_bounds A

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B

sup_a sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B
sup_b_up_A: sup_b up_bounds A

sup_a sup_b
Warning: unused variable `A_up` [linter.unusedVariables]
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B
sup_b_up_A: sup_b up_bounds A

sup_a sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hB: is_sup B sup_b
h_incl: A B
A_el: x A, x B
sup_b_up_A: sup_b up_bounds A
A_up: sup_a up_bounds A
A_least: x up_bounds A, sup_a x

intro
sup_a sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_incl: A B

sup_a sup_b

Goals accomplished! 🐙
instance [HAdd E E E] : HAdd (Set E) (Set E) (Set E) where hAdd A B := {x : E | a A, b B, x = a + b} /-- sup(A + B) = sup(A) + sup(B) -/ theorem sup_sum_eq_sum_sup (A B : Set E) (sup_a sup_b sup_a_b : E) (hA : is_sup A sup_a) (hB : is_sup B sup_b) (h_add : is_sup (A + B) (sup_a_b)) : sup_a_b = sup_a + sup_b :=

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_add: is_sup (A + B) sup_a_b

sup_a_b = sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

intro
sup_a_b = sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_add: is_sup (A + B) sup_a_b

sup_a_b = sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

intro
sup_a_b = sup_a + sup_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

sup_a_b sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

sup_a_b sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

sup_a_b sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

sup_a_b sup_a + sup_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

A + B = {x | a A, b B, x = a + b}

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

sup_a_b sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a_b sup_a + sup_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b {x | a A + B, a x}
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x: E
xin: x A + B

x sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x: E
xin: x A + B

x sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x: E
xin: x {x | a A, b B, x = a + b}

x sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x: E
xin: x {x | a A, b B, x = a + b}

x sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x: E
xin: x {x | a A, b B, x = a + b}

x sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b

intro.intro.intro.intro
x sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b

intro.intro.intro.intro
x sup_a + sup_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b

a sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b

a sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b

a sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
upA: sup_a up_bounds A
right✝: x up_bounds A, sup_a x

intro
a sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b

a sup_a

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a

intro.intro.intro.intro
x sup_a + sup_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a

b sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a

b sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a

b sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a
upB: sup_b up_bounds B
right✝: x up_bounds B, sup_b x

intro
b sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a

b sup_b

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a
tmpB: b sup_b

intro.intro.intro.intro
x sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a
tmpB: b sup_b

intro.intro.intro.intro
a + b sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}
x, a: E
ain: a A
b: E
bin: b B
sum: x = a + b
tmpA: a sup_a
tmpB: b sup_b

intro.intro.intro.intro
a + b sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
rfl_add: A + B = {x | a A, b B, x = a + b}

sup_a + sup_b up_bounds (A + B)

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x

sup_a_b sup_a + sup_b

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
h_add: is_sup (A + B) sup_a_b

sup_a_b = sup_a + sup_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

intro
sup_a_b = sup_a + sup_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

sup_a + sup_b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

sup_a + sup_b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

sup_a + sup_b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

sup_a + sup_b sup_a_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

a A, b B, a + b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

a A, b B, a + b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

a A, b B, a + b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
a: E
ain: a A
b: E
bin: b B

a + b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

a A, b B, a + b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
a: E
ain: a A
b: E
bin: b B
membership: a + b A + B

a + b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

a A, b B, a + b sup_a_b

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b

b B, sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B

sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B

sup_a sup_a_b - b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B

sup_a_b - b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B

sup_a_b - b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B

sup_a_b - b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B

sup_a_b - b {x | a A, a x}
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B

sup_a_b - b up_bounds A
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B
a: E
ain: a A

a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B

sup_a_b - b up_bounds A

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
coe_add_set: a A, b B, a + b sup_a_b
tmp: a A, b B, a sup_a_b - b
b: E
bin: b B
up_bound: sup_a_b - b up_bounds A
left✝: sup_a up_bounds A
leastA: x up_bounds A, sup_a x

intro
sup_a sup_a_b - b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

b B, sup_a sup_a_b - b

Goals accomplished! 🐙

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b

sup_a + sup_b sup_a_b
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b

sup_a + sup_b sup_a_b

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b

sup_b sup_a_b - sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b

sup_b sup_a_b - sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b

sup_b sup_a_b - sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b

sup_b sup_a_b - sup_a

Goals accomplished! 🐙
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b

b B, b sup_a_b - sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b

b B, b sup_a_b - sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b

b B, b sup_a_b - sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c| * (1 / |c| * b) = |c| * |c|⁻¹ * b
one_mul: (a : E), 1 * a = a
A, B: Set E
sup_a, sup_b, sup_a_b: E
hA: is_sup A sup_a
hB: is_sup B sup_b
up: sup_a_b up_bounds (A + B)
least: x up_bounds (A + B), sup_a_b x
sup_sum_le_sup: sup_a_b sup_a + sup_b
tt: b B, sup_a sup_a_b - b
b: E
bin: b B

b sup_a_b - sup_a
E: Type u_1
inst✝³: HMul ℝ E E
inst✝²: OrderedAddCommGroup E
inst✝¹: CovariantClass E E (fun a b => a + b) fun a b => a b
inst✝: CovariantClass E E (Function.swap fun a b => a + b) fun a b => a b
c:
le_mul_pos: (a b : E), a b |c| * a |c| * b
le_div_pos: (a b : E), a b 1 / |c| * a 1 / |c| * b
mul_assoc: (b : E), |c|</