awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi
-- 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
hc0 : ∀ (i : ι) (hi : i ∈ I), c i = 0
⊢ ∀ (i : ι) (hi : i ∈ I), x i = 0

Tactic:
have heg0 (i : ι) (hi : i ∈ I) : x i = 0 :=
          zero_smul_set_subset (α := 𝕜) (U i) (hc0 i hi ▸ hc i hi)
-- 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
hc0 : ∀ (i : ι) (hi : i ∈ I), c i = 0
heg0 : ∀ (i : ι) (hi : i ∈ I), x i = 0
⊢ ¬∃ i ∈ I, x i ≠ 0

Tactic:
simpa
-- 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
hc0 : ∀ (i : ι) (hi : i ∈ I), c i = 0
heg0 : ∀ (i : ι) (hi : i ∈ I), x i = 0
⊢ NeBot (α := 𝕜) (𝓝[≠] 0)

Tactic:
have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)
-- 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
hc0 : ∀ (i : ι) (hi : i ∈ I), c i = 0
heg0 : ∀ (i : ι) (hi : i ∈ I), x i = 0
this : NeBot (α := 𝕜) (𝓝[≠] 0)
neg :
  ∀ (c₁ : 𝕜) (hc₁ : c₁ ≠ 0) (hc₁r : ‖c₁‖ₑ < r), ∃ (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 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)
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
hc0 : ∀ (i : ι) (hi : i ∈ I), c i = 0
heg0 : ∀ (i : ι) (hi : i ∈ I), x i = 0
this : NeBot (α := 𝕜) (𝓝[≠] 0)
c₁ : 𝕜
hc₁ : c₁ ≠ 0
hc₁r : ‖c₁‖ₑ < r
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
⟨c₁, .inl hc₁, fun i hi ↦ ?_, hc₁r⟩

Premises used: And.intro, Exists.intro, Or.inl
-- 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
hc0 : ∀ (i : ι) (hi : i ∈ I), c i = 0
heg0 : ∀ (i : ι) (hi : i ∈ I), x i = 0
this : NeBot (α := 𝕜) (𝓝[≠] 0)
c₁ : 𝕜
hc₁ : c₁ ≠ 0
hc₁r : ‖c₁‖ₑ < r
neg : ∀ (i : ι) (hi : i ∈ I), ‖c i‖ ≤ ‖c₁‖
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
refine ⟨c₁, .inl hc₁, fun i hi ↦ ?_, 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₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (β := ℝ≥0∞) (fun (x : ι) ↦ ‖c x‖ₑ) I i₀
H : c i₀ = 0 ∧ I ≠ univ
hc0 : ∀ (i : ι) (hi : i ∈ I), c i = 0
heg0 : ∀ (i : ι) (hi : i ∈ I), x i = 0
this : NeBot (α := 𝕜) (𝓝[≠] 0)
c₁ : 𝕜
hc₁ : c₁ ≠ 0
hc₁r : ‖c₁‖ₑ < r
i : ι
hi : i ∈ I
⊢ ‖c i‖ ≤ ‖c₁‖

Tactic:
simp [hc0 i hi]
-- 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
obtain :
  ∀ (c₀ : 𝕜) (hc₀ : c₀ ≠ 0 ∨ I = univ) (hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) (hc₀r : ‖c₀‖ₑ < r),
    egauge 𝕜 (I.pi (α := E) U) x < r
⊢ egauge 𝕜 (I.pi (α := E) U) x < r

Tactic:
obtain ⟨c₀, hc₀, hc₀I, hc₀r⟩ :
      ∃ c₀ : 𝕜, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r := by
    have hr₀ : 0 < r := hr.bot_lt
    rcases I.eq_empty_or_nonempty with rfl | hIne
    · obtain hι | hbot : IsEmpty ι ∨ (𝓝[≠] (0 : 𝕜)).NeBot := by simpa [@eq_comm _ ∅] using hI₀
      · use 0
        simp [@eq_comm _ ∅, hι, hr₀]
      · rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₀, hc₀, hc₀r⟩
        exact ⟨c₀, .inl hc₀, by simp, hc₀r⟩
    · obtain ⟨i₀, hi₀I, hc_max⟩ : ∃ i₀ ∈ I, IsMaxOn (‖c ·‖ₑ) I i₀ :=
        exists_max_image _ (‖c ·‖ₑ) hI hIne
      by_cases! H : c i₀ ≠ 0 ∨ I = univ
      · exact ⟨c i₀, H, fun i hi ↦ by simpa [enorm] using hc_max hi, hcr _ hi₀I⟩
      · have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi
        have heg0 (i : ι) (hi : i ∈ I) : x i = 0 :=
          zero_smul_set_subset (α := 𝕜) (U i) (hc0 i hi ▸ hc i hi)
        have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)
        rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₁, hc₁, hc₁r⟩
        refine ⟨c₁, .inl hc₁, fun i hi ↦ ?_, hc₁r⟩
        simp [hc0 i hi]
-- 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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
⊢ egauge 𝕜 (I.pi (α := E) U) x < r

Tactic:
egauge_lt_iff.2 ⟨c₀, ?_, hc₀r⟩

Premises used: Iff.mpr, And.intro, Exists.intro, egauge_lt_iff
-- 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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
refine : x ∈ c₀ • I.pi (α := E) U
⊢ egauge 𝕜 (I.pi (α := E) U) x < r

Tactic:
refine egauge_lt_iff.2 ⟨c₀, ?_, hc₀r⟩

Premises used: Iff.mpr, And.intro, Exists.intro, egauge_lt_iff
-- 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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
rw : x ∈ I.pi (α := E) (c₀ • U)
⊢ x ∈ c₀ • I.pi (α := E) U

Tactic:
rw [smul_set_pi₀' hc₀]

Premises used: Set.smul_set_pi₀'
-- 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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
i : ι
hi : i ∈ I
⊢ x i ∈ (c₀ • U) i

Tactic:
(hU i hi).smul_mono (hc₀I i hi) (hc i hi)

Premises used: Set.Mem, Balanced.smul_mono
-- 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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
i : ι
hi : i ∈ I
⊢ x i ∈ (c₀ • U) i

Tactic:
exact (hU i hi).smul_mono (hc₀I i hi) (hc i hi)

Premises used: Balanced.smul_mono
-- 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)
inst_3 : Finite ι
U : (i : ι) → Set (E i)
hU : ∀ (i : ι), Balanced 𝕜 (U i)
x : (i : ι) → E i
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) univ i), egauge 𝕜 (U i) (x i))
    (⨆ (i : ι), egauge 𝕜 (U i) (x i))

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)
inst_3 : NeBot (α := 𝕜) (𝓝[≠] 0)
I : Set ι
U : (i : ι) → Set (E i)
hI : I.Finite
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
⊢ egauge 𝕜 (I.pi (α := E) U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i)

Tactic:
egauge_pi' hI hU x <| .inr <| .inr inferInstance

Premises used: inferInstance, Or.inr, egauge_pi'
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ≥0
x : E
rw : ∀ (c : 𝕜), x ∈ HSMul.hSMul (β := Set E) c (closedBall 0 (↑r : ℝ)) → ‖x‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ
⊢ ‖x‖ₑ / (↑r : ℝ≥0∞) ≤ egauge 𝕜 (closedBall 0 (↑r : ℝ)) x

Tactic:
rw [le_egauge_iff]

Premises used: le_egauge_iff
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : Membership.mem (γ := Set E) (closedBall 0 (↑r : ℝ)) y
⊢ ‖y‖₊ ≤ r

Tactic:
rw [mem_closedBall_zero_iff, ← coe_nnnorm, NNReal.coe_le_coe] at hy

Premises used: coe_nnnorm, mem_closedBall_zero_iff, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
rw : ‖c‖ₑ * ‖y‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ
⊢ enorm.{u_2} (E := E) ((fun (x : E) ↦ c • x) y) / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ

Tactic:
rw [enorm_smul]

Premises used: enorm_smul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
h : ‖c‖ₑ * ‖y‖ₑ ≤ ‖c‖ₑ * (↑r : ℝ≥0∞)
⊢ ‖c‖ₑ * ‖y‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ

Tactic:
apply ENNReal.div_le_of_le_mul

Premises used: ENNReal.div_le_of_le_mul
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
h : ‖y‖ₑ ≤ (↑r : ℝ≥0∞)
⊢ ‖c‖ₑ * ‖y‖ₑ ≤ ‖c‖ₑ * (↑r : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy h h₁ h₂ h₃ : ‖y‖₊ ≤ r
⊢ ‖y‖ₑ ≤ (↑r : ℝ≥0∞)

Tactic:
rwa [enorm_le_coe]

Premises used: enorm_le_coe
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ ‖x‖ₑ ≤ egauge 𝕜 (closedBall 0 1) x

Tactic:
simpa using div_le_egauge_closedBall 𝕜 1 x

Premises used: div_le_egauge_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ≥0
x : E
⊢ ‖x‖ₑ / (↑r : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) x

Tactic:
(div_le_egauge_closedBall 𝕜 r x).trans <| egauge_anti _ ball_subset_closedBall _

Premises used: Metric.ball_subset_closedBall, div_le_egauge_closedBall, LE.le.trans, egauge_anti
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ ‖x‖ₑ ≤ egauge 𝕜 (ball 0 1) x

Tactic:
simpa using div_le_egauge_ball 𝕜 1 x

Premises used: div_le_egauge_ball, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
inl : ∀ (h₀ : Ne (α := ℝ≥0) 0 0 ∨ ‖x‖ ≠ 0), egauge 𝕜 (ball 0 (↑0 : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑0 : ℝ≥0∞)
inr : ∀ (hr : 0 < r), egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)

Tactic:
rcases eq_zero_or_pos r with rfl | hr

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
hc : 1 < ‖c‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
h₀ : Ne (α := ℝ≥0) 0 0 ∨ ‖x‖ ≠ 0
inl : egauge 𝕜 (ball 0 (↑0 : ℝ)) x ≤ ∞
rw : ‖c‖ₑ ≠ 0
rw₁ : ‖x‖ₑ ≠ 0
⊢ egauge 𝕜 (ball 0 (↑0 : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑0 : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_zero, ENNReal.div_zero (mul_ne_zero _ _)]

Premises used: ENNReal.coe_zero, ENNReal.div_zero, mul_ne_zero
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
hc : 1 < ‖c‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
h₀ : Ne (α := ℝ≥0) 0 0 ∨ ‖x‖ ≠ 0
⊢ egauge 𝕜 (ball 0 (↑0 : ℝ)) x ≤ ∞

Tactic:
apply le_top

Premises used: le_top
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
hc : 1 < ‖c‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
h₀ : Ne (α := ℝ≥0) 0 0 ∨ ‖x‖ ≠ 0
⊢ ‖c‖ₑ ≠ 0

Tactic:
simpa using one_pos.trans hc

Premises used: LT.lt.trans, one_pos
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
hc : 1 < ‖c‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
h₀ : Ne (α := ℝ≥0) 0 0 ∨ ‖x‖ ≠ 0
⊢ ‖x‖ₑ ≠ 0

Tactic:
simpa [enorm, ← NNReal.coe_eq_zero] using h₀

Premises used: NNReal.coe_eq_zero, ENorm.enorm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
inr : ∀ (hx : ‖x‖ = 0), egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
inr₁ : ∀ (hx : ‖x‖ ≠ 0), egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)

Tactic:
rcases eq_or_ne ‖x‖ 0 with hx | hx

Premises used: Norm.norm, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
⊢ ‖x‖ₑ = 0

Tactic:
simpa [enorm, ← coe_nnnorm, NNReal.coe_eq_zero] using hx

Premises used: NNReal.coe_eq_zero, ENorm.enorm, coe_nnnorm
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
⊢ ‖x‖ₑ = 0

Tactic:
have hx' : ‖x‖ₑ = 0 := by simpa [enorm, ← coe_nnnorm, NNReal.coe_eq_zero] using hx
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
hx' : ‖x‖ₑ = 0
inr : ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c (ball 0 (↑r : ℝ))
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)

Tactic:
simp only [hx', mul_zero, ENNReal.zero_div, nonpos_iff_eq_zero, egauge_eq_zero_iff]

Premises used: ENNReal.zero_div, MulZeroClass.mul_zero, egauge_eq_zero_iff, nonpos_iff_eq_zero
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
hx' : ‖x‖ₑ = 0
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c (ball 0 (↑r : ℝ))

Tactic:
(frequently_iff_neBot.2 (inferInstance : NeBot (𝓝[≠] (0 : 𝕜)))).mono fun c hc ↦ ?_

Premises used: Iff.mpr, inferInstance, Filter.Frequently.mono, Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
hx' : ‖x‖ₑ = 0
inr : ∀ (c : 𝕜) (hc : c ∉ {0}), x ∈ HSMul.hSMul (β := Set E) c (ball 0 (↑r : ℝ))
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c (ball 0 (↑r : ℝ))

Tactic:
refine (frequently_iff_neBot.2 (inferInstance : NeBot (𝓝[≠] (0 : 𝕜)))).mono fun c hc ↦ ?_

Premises used: Iff.mpr, inferInstance, Filter.Frequently.mono, Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c_1 : 𝕜
x : E
r : ℝ≥0
hc_1 : 1 < ‖c_1‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ = 0
hx' : ‖x‖ₑ = 0
c : 𝕜
hc : c ∉ {0}
⊢ x ∈ HSMul.hSMul (β := Set E) c (ball 0 (↑r : ℝ))

Tactic:
simp [mem_smul_set_iff_inv_smul_mem₀ hc, norm_smul, hx, hr]

Premises used: norm_smul, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ ≠ 0
inr :
  ∀ (a : 𝕜) (ha₀ : a ≠ 0) (har : ‖a • x‖ < (↑r : ℝ)) (hainv : ‖a‖⁻¹ ≤ (↑r : ℝ)⁻¹ * ‖c‖ * ‖x‖),
    egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)

Tactic:
rcases rescale_to_shell_semi_normed hc hr hx with ⟨a, ha₀, har, -, hainv⟩

Premises used: rescale_to_shell_semi_normed
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ ≠ 0
a : 𝕜
ha₀ : a ≠ 0
har : ‖a • x‖ < (↑r : ℝ)
hainv : ‖a‖⁻¹ ≤ (↑r : ℝ)⁻¹ * ‖c‖ * ‖x‖
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ (↑‖a‖₊⁻¹ : ℝ≥0∞)

Tactic:
egauge_le_of_smul_mem_of_ne (mem_ball_zero_iff.2 har) ha₀

Premises used: Iff.mpr, mem_ball_zero_iff, egauge_le_of_smul_mem_of_ne
-- Module: Mathlib.Analysis.Convex.EGauge
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst, non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ ≠ 0
a : 𝕜
ha₀ : a ≠ 0
har : ‖a • x‖ < (↑r : ℝ)
hainv : ‖a‖⁻¹ ≤ (↑r : ℝ)⁻¹ * ‖c‖ * ‖x‖
rwa : ‖a‖₊⁻¹ ≤ ‖c‖₊ * ‖x‖₊ / r
rwa₁ : ‖a‖₊⁻¹ ≤ r⁻¹ * (‖c‖₊ * ‖x‖₊)
rwa₂ rwa₃ rwa₄ rwa₅ : ‖a‖₊⁻¹ ≤ r⁻¹ * ‖c‖₊ * ‖x‖₊
⊢ (↑‖a‖₊⁻¹ : ℝ≥0∞) ≤ (↑(‖c‖₊ * ‖x‖₊ / r) : ℝ≥0∞)

Tactic:
rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]

Premises used: mul_assoc, ENNReal.coe_le_coe, div_eq_inv_mul