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
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
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|