-- Mathlib/Analysis/Convex/EGauge.lean
theorem egauge_add_add_le {U V : Set E} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a b : E) :
    egauge 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b)

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
c : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
⊢ ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c

Tactic:
wlog hxy : ‖x‖ ≤ ‖y‖ generalizing a b x y U V

Result:
case intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
c : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
this :
  ∀ {U V : Set E},
    Balanced 𝕜 U →
      Balanced 𝕜 V →
        ∀ (a b : E) (x : 𝕜),
          a ∈ x • U → ‖x‖ₑ < c → ∀ (y : 𝕜), b ∈ y • V → ‖y‖ₑ < c → ‖x‖ ≤ ‖y‖ → ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c
hxy : ¬‖x‖ ≤ ‖y‖
⊢ ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c

𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : ℝ≥0∞
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
hxy : ‖x‖ ≤ ‖y‖
⊢ ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : ℝ≥0∞
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
hxy : ‖x‖ ≤ ‖y‖
⊢ a + b ∈ y • U + y • V

Tactic:
exact add_mem_add (hU.smul_mono hxy hx) hy

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : ℝ≥0∞
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
hxy : ‖x‖ ≤ ‖y‖
⊢ ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c

Tactic:
refine ⟨y, ?_, hyc⟩

Result:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : ℝ≥0∞
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
hxy : ‖x‖ ≤ ‖y‖
⊢ a + b ∈ y • (U + V)

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
c : ℝ≥0∞
hc : (∃ c_1, a ∈ c_1 • U ∧ ‖c_1‖ₑ < c) ∧ ∃ c_1, b ∈ c_1 • V ∧ ‖c_1‖ₑ < c
⊢ ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c

Tactic:
rcases hc with ⟨⟨x, hx, hxc⟩, ⟨y, hy, hyc⟩⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
c : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
⊢ ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
c : ℝ≥0∞
hc : egauge 𝕜 U a ⊔ egauge 𝕜 V b < c
⊢ egauge 𝕜 (U + V) (a + b) < c

Tactic:
simp only [max_lt_iff, egauge_lt_iff] at hc ⊢

Result:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
c : ℝ≥0∞
hc : (∃ c_1, a ∈ c_1 • U ∧ ‖c_1‖ₑ < c) ∧ ∃ c_1, b ∈ c_1 • V ∧ ‖c_1‖ₑ < c
⊢ ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c

Proof state:
case intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
c : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
this :
  ∀ {U V : Set E},
    Balanced 𝕜 U →
      Balanced 𝕜 V →
        ∀ (a b : E) (x : 𝕜),
          a ∈ x • U → ‖x‖ₑ < c → ∀ (y : 𝕜), b ∈ y • V → ‖y‖ₑ < c → ‖x‖ ≤ ‖y‖ → ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c
hxy : ¬‖x‖ ≤ ‖y‖
⊢ ∃ c_1, a + b ∈ c_1 • (U + V) ∧ ‖c_1‖ₑ < c

Tactic:
simpa only [add_comm] using this hV hU b a y hy hyc x hx hxc (le_of_not_le hxy)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : ℝ≥0∞
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
hxy : ‖x‖ ≤ ‖y‖
⊢ a + b ∈ y • (U + V)

Tactic:
rw [smul_add]

Result:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : ℝ≥0∞
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
x : 𝕜
hx : a ∈ x • U
hxc : ‖x‖ₑ < c
y : 𝕜
hy : b ∈ y • V
hyc : ‖y‖ₑ < c
hxy : ‖x‖ ≤ ‖y‖
⊢ a + b ∈ y • U + y • V

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
⊢ egauge 𝕜 (U + V) (a + b) ≤ egauge 𝕜 U a ⊔ egauge 𝕜 V b

Tactic:
refine le_of_forall_lt' fun c hc ↦ ?_

Result:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
c : ℝ≥0∞
hc : egauge 𝕜 U a ⊔ egauge 𝕜 V b < c
⊢ egauge 𝕜 (U + V) (a + b) < c