awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
⊢ egauge 𝕜 (U ×ˢ V) (a, b) = max (egauge 𝕜 U a) (egauge 𝕜 V b)

Tactic:
le_antisymm (le_of_forall_gt fun r hr ↦ ?_) (le_egauge_prod _ _ _ _)

Premises used: le_egauge_prod, le_antisymm, le_of_forall_gt
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
refine : ∀ (r : ℝ≥0∞) (hr : max (egauge 𝕜 U a) (egauge 𝕜 V b) < r), egauge 𝕜 (U ×ˢ V) (a, b) < r
⊢ egauge 𝕜 (U ×ˢ V) (a, b) = max (egauge 𝕜 U a) (egauge 𝕜 V b)

Tactic:
refine le_antisymm (le_of_forall_gt fun r hr ↦ ?_) (le_egauge_prod _ _ _ _)

Premises used: le_egauge_prod, le_antisymm, le_of_forall_gt
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
hr : max (egauge 𝕜 U a) (egauge 𝕜 V b) < r
simp :
  ∀ (hr : (∃ (c : 𝕜), a ∈ c • U ∧ ‖c‖ₑ < r) ∧ ∃ (c : 𝕜), b ∈ c • V ∧ ‖c‖ₑ < r),
    ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r
⊢ egauge 𝕜 (U ×ˢ V) (a, b) < r

Tactic:
simp only [max_lt_iff, egauge_lt_iff, smul_set_prod] at hr ⊢

Premises used: max_lt_iff, Set.smul_set_prod, egauge_lt_iff
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
hr : (∃ (c : 𝕜), a ∈ c • U ∧ ‖c‖ₑ < r) ∧ ∃ (c : 𝕜), b ∈ c • V ∧ ‖c‖ₑ < r
rcases :
  ∀ (x : 𝕜) (hx : a ∈ x • U) (hxr : ‖x‖ₑ < r) (y : 𝕜) (hy : b ∈ y • V) (hyr : ‖y‖ₑ < r),
    ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r
⊢ ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r

Tactic:
rcases hr with ⟨⟨x, hx, hxr⟩, ⟨y, hy, hyr⟩⟩
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxr : ‖x‖ₑ < r
y : 𝕜
hy : b ∈ y • V
hyr : ‖y‖ₑ < r
hle : ‖x‖ ≤ ‖y‖
⊢ ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r

Tactic:
⟨y, ⟨hU.smul_mono hle hx, hy⟩, hyr⟩

Premises used: And.intro, Exists.intro, Balanced.smul_mono
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxr : ‖x‖ₑ < r
y : 𝕜
hy : b ∈ y • V
hyr : ‖y‖ₑ < r
hle : ‖x‖ ≤ ‖y‖
⊢ ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r

Tactic:
exact ⟨y, ⟨hU.smul_mono hle hx, hy⟩, hyr⟩
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxr : ‖x‖ₑ < r
y : 𝕜
hy : b ∈ y • V
hyr : ‖y‖ₑ < r
hle : ‖y‖ ≤ ‖x‖
⊢ ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r

Tactic:
⟨x, ⟨hx, hV.smul_mono hle hy⟩, hxr⟩

Premises used: And.intro, Exists.intro, Balanced.smul_mono
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxr : ‖x‖ₑ < r
y : 𝕜
hy : b ∈ y • V
hyr : ‖y‖ₑ < r
hle : ‖y‖ ≤ ‖x‖
⊢ ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r

Tactic:
exact ⟨x, ⟨hx, hV.smul_mono hle hy⟩, hxr⟩
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
F : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 F
U : Set E
V : Set F
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a : E
b : F
r : ℝ≥0∞
x : 𝕜
hx : a ∈ x • U
hxr : ‖x‖ₑ < r
y : 𝕜
hy : b ∈ y • V
hyr : ‖y‖ₑ < r
⊢ ‖x‖ ≤ ‖y‖ ∨ ‖y‖ ≤ ‖x‖

Tactic:
cases le_total ‖x‖ ‖y‖ with
  | inl hle => exact ⟨y, ⟨hU.smul_mono hle hx, hy⟩, hyr⟩
  | inr hle => exact ⟨x, ⟨hx, hV.smul_mono hle hy⟩, hxr⟩

Premises used: Norm.norm, le_total
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
rw : egauge 𝕜 ((fun (x : E × E) ↦ x.1 + x.2) '' U ×ˢ V) (a + b) ≤ egauge 𝕜 (U ×ˢ V) (a, b)
⊢ egauge 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b)

Tactic:
rw [← egauge_prod_mk hU hV a b, ← add_image_prod]

Premises used: egauge_prod_mk, Set.add_image_prod
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
⊢ egauge 𝕜 ((fun (x : E × E) ↦ x.1 + x.2) '' U ×ˢ V) (a + b) ≤ egauge 𝕜 (U ×ˢ V) (a, b)

Tactic:
MapsTo.egauge_le 𝕜 (LinearMap.fst 𝕜 E E + LinearMap.snd 𝕜 E E) (mapsTo_image _ _) (a, b)

Premises used: LinearMap.fst, LinearMap.snd, Set.mapsTo_image, Prod.mk, HAdd.hAdd, Set.MapsTo.egauge_le
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
⊢ egauge 𝕜 ((fun (x : E × E) ↦ x.1 + x.2) '' U ×ˢ V) (a + b) ≤ egauge 𝕜 (U ×ˢ V) (a, b)

Tactic:
exact MapsTo.egauge_le 𝕜 (LinearMap.fst 𝕜 E E + LinearMap.snd 𝕜 E E) (mapsTo_image _ _) (a, b)

Premises used: LinearMap.fst, LinearMap.snd, Set.mapsTo_image, Prod.mk, HAdd.hAdd, Set.MapsTo.egauge_le
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
⊢ egauge 𝕜 (I.pi (α := E) U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

Tactic:
le_antisymm ?_ (iSup₂_le fun i hi ↦ le_egauge_pi hi _ _)

Premises used: iSup₂_le, le_egauge_pi, le_antisymm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
refine : egauge 𝕜 (I.pi (α := E) U) x ≤ ⨆ i ∈ I, egauge 𝕜 (U i) (x i)
⊢ egauge 𝕜 (I.pi (α := E) U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

Tactic:
refine le_antisymm ?_ (iSup₂_le fun i hi ↦ le_egauge_pi hi _ _)

Premises used: iSup₂_le, le_antisymm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
⊢ egauge 𝕜 (I.pi (α := E) U) x ≤ ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

Tactic:
le_of_forall_gt fun r hr ↦ ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
refine : ∀ (r : ℝ≥0∞) (hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r), egauge 𝕜 (I.pi (α := E) U) x < r
⊢ egauge 𝕜 (I.pi (α := E) U) x ≤ ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

Tactic:
refine le_of_forall_gt fun r hr ↦ ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
⊢ ∀ i ∈ I, ∃ (c : 𝕜), x i ∈ c • U i ∧ ‖c‖ₑ < r

Tactic:
have : ∀ i ∈ I, ∃ c : 𝕜, x i ∈ c • U i ∧ ‖c‖ₑ < r := fun i hi ↦
    egauge_lt_iff.mp <| (le_iSup₂ i hi).trans_lt hr
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
this : ∀ i ∈ I, ∃ (c : 𝕜), x i ∈ c • U i ∧ ‖c‖ₑ < r
choose! :
  ∀ (c : (i : ι) → 𝕜) (hc : ∀ i ∈ I, x i ∈ c i • U i) (hcr : ∀ i ∈ I, ‖c i‖ₑ < r), egauge 𝕜 (I.pi (α := E) U) x < r
⊢ egauge 𝕜 (I.pi (α := E) U) x < r

Tactic:
choose! c hc hcr using this
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : (i : ι) → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
⊢ 0 < r

Tactic:
have hr₀ : 0 < r := hr.bot_lt
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : (i : ι) → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
inl :
  ∀ (hI : Set.Finite.{u_2} (α := ι) ∅) (hU : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Balanced 𝕜 (U i))
    (hI₀ :
      Eq.{u_2 + 1} (α := Set ι) ∅ univ ∨
        (∃ (i : ι), Membership.mem (γ := Set ι) ∅ i ∧ x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0))
    (hr : ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), egauge 𝕜 (U i) (x i) < r)
    (hc : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i ∈ c i • U i)
    (hcr : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ₑ < r),
    ∃ (c₀ : 𝕜),
      (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
        (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
inr : ∀ (hIne : I.Nonempty), ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
rcases I.eq_empty_or_nonempty with rfl | hIne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : (i : ι) → 𝕜
hr₀ : 0 < r
hI : Set.Finite.{u_2} (α := ι) ∅
hU : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Balanced 𝕜 (U i)
hI₀ :
  Eq.{u_2 + 1} (α := Set ι) ∅ univ ∨ (∃ (i : ι), Membership.mem (γ := Set ι) ∅ i ∧ x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
hr : ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), egauge 𝕜 (U i) (x i) < r
hc : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i ∈ c i • U i
hcr : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ₑ < r
⊢ IsEmpty ι ∨ NeBot (α := 𝕜) (𝓝[≠] 0)

Tactic:
simpa [@eq_comm _ ∅] using hI₀

Premises used: eq_comm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : (i : ι) → 𝕜
hr₀ : 0 < r
hI : Set.Finite.{u_2} (α := ι) ∅
hU : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Balanced 𝕜 (U i)
hI₀ :
  Eq.{u_2 + 1} (α := Set ι) ∅ univ ∨ (∃ (i : ι), Membership.mem (γ := Set ι) ∅ i ∧ x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
hr : ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), egauge 𝕜 (U i) (x i) < r
hc : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i ∈ c i • U i
hcr : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ₑ < r
inl :
  ∀ (hι : IsEmpty ι),
    ∃ (c₀ : 𝕜),
      (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
        (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
inl₁ :
  ∀ (hbot : NeBot (α := 𝕜) (𝓝[≠] 0)),
    ∃ (c₀ : 𝕜),
      (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
        (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
⊢ ∃ (c₀ : 𝕜),
    (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
      (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
obtain hι | hbot : IsEmpty ι ∨ (𝓝[≠] (0 : 𝕜)).NeBot := by simpa [@eq_comm _ ∅] using hI₀

Premises used: Compl.compl, Filter.NeBot, nhdsWithin, IsEmpty, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : (i : ι) → 𝕜
hr₀ : 0 < r
hI : Set.Finite.{u_2} (α := ι) ∅
hU : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Balanced 𝕜 (U i)
hI₀ :
  Eq.{u_2 + 1} (α := Set ι) ∅ univ ∨ (∃ (i : ι), Membership.mem (γ := Set ι) ∅ i ∧ x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
hr : ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), egauge 𝕜 (U i) (x i) < r
hc : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i ∈ c i • U i
hcr : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ₑ < r
hι : IsEmpty ι
h :
  (Ne.{u_1 + 1} (α := 𝕜) 0 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
    (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ norm.{u_1} (E := 𝕜) 0) ∧ enorm.{u_1} (E := 𝕜) 0 < r
⊢ ∃ (c₀ : 𝕜),
    (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
      (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
use 0
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : (i : ι) → 𝕜
hr₀ : 0 < r
hI : Set.Finite.{u_2} (α := ι) ∅
hU : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Balanced 𝕜 (U i)
hI₀ :
  Eq.{u_2 + 1} (α := Set ι) ∅ univ ∨ (∃ (i : ι), Membership.mem (γ := Set ι) ∅ i ∧ x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
hr : ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), egauge 𝕜 (U i) (x i) < r
hc : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i ∈ c i • U i
hcr : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ₑ < r
hι : IsEmpty ι
⊢ (Ne.{u_1 + 1} (α := 𝕜) 0 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
    (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ norm.{u_1} (E := 𝕜) 0) ∧ enorm.{u_1} (E := 𝕜) 0 < r

Tactic:
simp [@eq_comm _ ∅, hι, hr₀]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : (i : ι) → 𝕜
hr₀ : 0 < r
hI : Set.Finite.{u_2} (α := ι) ∅
hU : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Balanced 𝕜 (U i)
hI₀ :
  Eq.{u_2 + 1} (α := Set ι) ∅ univ ∨ (∃ (i : ι), Membership.mem (γ := Set ι) ∅ i ∧ x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
hr : ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), egauge 𝕜 (U i) (x i) < r
hc : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i ∈ c i • U i
hcr : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ₑ < r
hbot : NeBot (α := 𝕜) (𝓝[≠] 0)
inl :
  ∀ (c₀ : 𝕜) (hc₀ : c₀ ≠ 0) (hc₀r : ‖c₀‖ₑ < r),
    ∃ (c₀ : 𝕜),
      (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
        (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
⊢ ∃ (c₀ : 𝕜),
    (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
      (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₀, hc₀, hc₀r⟩

Premises used: exists_enorm_lt, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : (i : ι) → 𝕜
hr₀ : 0 < r
hI : Set.Finite.{u_2} (α := ι) ∅
hU : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Balanced 𝕜 (U i)
hI₀ :
  Eq.{u_2 + 1} (α := Set ι) ∅ univ ∨ (∃ (i : ι), Membership.mem (γ := Set ι) ∅ i ∧ x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
hr : ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), egauge 𝕜 (U i) (x i) < r
hc : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i ∈ c i • U i
hcr : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ₑ < r
hbot : NeBot (α := 𝕜) (𝓝[≠] 0)
c₀ : 𝕜
hc₀ : c₀ ≠ 0
hc₀r : ‖c₀‖ₑ < r
⊢ ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
U : (i : ι) → Set (E i)
x : (i : ι) → E i
r : ℝ≥0∞
c : (i : ι) → 𝕜
hr₀ : 0 < r
hI : Set.Finite.{u_2} (α := ι) ∅
hU : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → Balanced 𝕜 (U i)
hI₀ :
  Eq.{u_2 + 1} (α := Set ι) ∅ univ ∨ (∃ (i : ι), Membership.mem (γ := Set ι) ∅ i ∧ x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
hr : ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), egauge 𝕜 (U i) (x i) < r
hc : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → x i ∈ c i • U i
hcr : ∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ₑ < r
hbot : NeBot (α := 𝕜) (𝓝[≠] 0)
c₀ : 𝕜
hc₀ : c₀ ≠ 0
hc₀r : ‖c₀‖ₑ < r
⊢ ∃ (c₀ : 𝕜),
    (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
      (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
exact ⟨c₀, .inl hc₀, by simp, hc₀r⟩
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : (i : ι) → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
⊢ ∃ i₀ ∈ I, IsMaxOn (β := ℝ≥0∞) (fun (x : ι) ↦ ‖c x‖ₑ) I i₀

Tactic:
exists_max_image _ (‖c ·‖ₑ) hI hIne

Premises used: Set.Mem, IsMaxOn, Filter.Eventually, setOf, Set.exists_max_image, Set.Subset, ENorm.enorm, IsMaxFilter
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : (i : ι) → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
inr :
  ∀ (i₀ : ι) (hi₀I : i₀ ∈ I) (hc_max : IsMaxOn (β := ℝ≥0∞) (fun (x : ι) ↦ ‖c x‖ₑ) I i₀),
    ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
obtain ⟨i₀, hi₀I, hc_max⟩ : ∃ i₀ ∈ I, IsMaxOn (‖c ·‖ₑ) I i₀ :=
        exists_max_image _ (‖c ·‖ₑ) hI hIne

Premises used: Set.exists_max_image, ENorm.enorm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : (i : ι) → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
i₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (β := ℝ≥0∞) (fun (x : ι) ↦ ‖c x‖ₑ) I i₀
pos : ∀ (H : c i₀ ≠ 0 ∨ I = univ), ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
neg : ∀ (H : c i₀ = 0 ∧ I ≠ univ), ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
by_cases! H : c i₀ ≠ 0 ∨ I = univ

Premises used: Set.univ
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : (i : ι) → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
i₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (β := ℝ≥0∞) (fun (x : ι) ↦ ‖c x‖ₑ) I i₀
H : c i₀ ≠ 0 ∨ I = univ
i : ι
hi : i ∈ I
⊢ ‖c i‖ ≤ ‖c i₀‖

Tactic:
simpa [enorm] using hc_max hi

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : (i : ι) → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
i₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (β := ℝ≥0∞) (fun (x : ι) ↦ ‖c x‖ₑ) I i₀
H : c i₀ ≠ 0 ∨ I = univ
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
exact ⟨c i₀, H, fun i hi ↦ by simpa [enorm] using hc_max hi, hcr _ hi₀I⟩
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ NeBot (α := 𝕜) (𝓝[≠] 0)
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : (i : ι) → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
i₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (β := ℝ≥0∞) (fun (x : ι) ↦ ‖c x‖ₑ) I i₀
H : c i₀ = 0 ∧ I ≠ univ
i : ι
hi : i ∈ I
⊢ c i = 0

Tactic:
simpa [H] using hc_max hi