awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
inl :
  ∀ (h : Eq.{u_1 + 1} (α := 𝕜) 0 0 → s.Nonempty),
    egauge 𝕜 s (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) ≤ enorm.{u_1} (E := 𝕜) 0 * egauge 𝕜 s x
⊢ egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x
have inr : ∀ (hc : c ≠ 0), egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ egauge 𝕜 s (c • x) ≤ ‖c‖ₑ * egauge 𝕜 s x
have inr : ‖c⁻¹‖ₑ * egauge 𝕜 s (c • x) ≤ egauge 𝕜 s x
Tactic: rw [mul_comm, ← ENNReal.div_le_iff_le_mul (.inl <| by simpa) (.inl enorm_ne_top),
      ENNReal.div_eq_inv_mul, ← enorm_inv (by simpa)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ ‖c⁻¹‖ₑ * egauge 𝕜 s (c • x) ≤ egauge 𝕜 s x
have inr : egauge 𝕜 s (c⁻¹ • c • x) = egauge 𝕜 s x
Tactic: refine (le_egauge_smul_right _ _ _).trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
c : 𝕜
s : Set E
h : c = 0 → s.Nonempty
x : E
hc : c ≠ 0
⊢ egauge 𝕜 s (c⁻¹ • c • x) = egauge 𝕜 s x
have inr : egauge 𝕜 s x = egauge 𝕜 s x
Tactic: rw [inv_smul_smul₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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)
have refine : ∀ (r : ℝ≥0∞) (hr : max (egauge 𝕜 U a) (egauge 𝕜 V b) < r), egauge 𝕜 (U ×ˢ V) (a, b) < r
Tactic: refine le_antisymm (le_of_forall_gt fun r hr ↦ ?_) (le_egauge_prod _ _ _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ egauge 𝕜 (U ×ˢ V) (a, b) < r
have simp : ∀ (hr : (∃ (c : 𝕜), a ∈ c • U ∧ ‖c‖ₑ < r) ∧ ∃ (c : 𝕜), b ∈ c • V ∧ ‖c‖ₑ < r),
  ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r
Tactic: simp only [max_lt_iff, egauge_lt_iff, smul_set_prod] at hr ⊢
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r
have 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
Tactic: rcases hr with ⟨⟨x, hx, hxr⟩, ⟨y, hy, hyr⟩⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
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
⊢ ∃ (c : 𝕜), (a, b) ∈ (c • U) ×ˢ (c • V) ∧ ‖c‖ₑ < r
have x₁ : ‖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⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b)
have rw : egauge 𝕜 ((fun (x : E × E) ↦ x.1 + x.2) '' U ×ˢ V) (a + b) ≤ egauge 𝕜 (U ×ˢ V) (a, b)
Tactic: rw [← egauge_prod_mk hU hV a b, ← add_image_prod]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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)
have refine : 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 _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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)
have refine : ∀ (r : ℝ≥0∞) (hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r), egauge 𝕜 (I.pi (α := E) U) x < r
Tactic: refine le_of_forall_gt fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
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
⊢ egauge 𝕜 (I.pi (α := E) U) x < r
have this : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ egauge 𝕜 (I.pi (α := E) U) x < r
have 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
Tactic: choose! c hc hcr using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
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₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have hr₀ : 0 < r
Tactic: have hr₀ : 0 < r := hr.bot_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have 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
Tactic: rcases I.eq_empty_or_nonempty with rfl | hIne
Cleared hypotheses: I, hI, hU, hI₀, hr, hc, hcr
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have inr : ∀ (hIne : I.Nonempty), ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
Tactic: rcases I.eq_empty_or_nonempty with rfl | hIne
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ∃ (c₀ : 𝕜),
    (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
      (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have inl : ∀ (hι : IsEmpty ι),
  ∃ (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₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ∃ (c₀ : 𝕜),
    (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
      (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have inl₁ : ∀ (hbot : NeBot (α := 𝕜) (𝓝[≠] 0)),
  ∃ (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₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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 ι
⊢ ∃ (c₀ : 𝕜),
    (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
      (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have 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
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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₀ : 𝕜),
    (c₀ ≠ 0 ∨ Eq.{u_2 + 1} (α := Set ι) ∅ univ) ∧
      (∀ (i : ι), Membership.mem (γ := Set ι) ∅ i → ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have 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
Tactic: rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₀, hc₀, hc₀r⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have 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
Tactic: obtain ⟨i₀, hi₀I, hc_max⟩ : ∃ i₀ ∈ I, IsMaxOn (‖c ·‖ₑ) I i₀ :=
        exists_max_image _ (‖c ·‖ₑ) hI hIne
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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₀
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have pos : ∀ (H : c i₀ ≠ 0 ∨ I = univ), ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
Tactic: by_cases! H : c i₀ ≠ 0 ∨ I = univ
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have neg : ∀ (H : c i₀ = 0 ∧ I ≠ univ), ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
Tactic: by_cases! H : c i₀ ≠ 0 ∨ I = univ
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
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
have hc0 : ∀ (i : ι) (hi : i ∈ I), c i = 0
Tactic: have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
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
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have heg0 : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
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
⊢ ∃ (c₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have this : NeBot (α := 𝕜) (𝓝[≠] 0)
Tactic: have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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₀ : 𝕜), (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r
have neg : ∀ (c₁ : 𝕜) (hc₁ : c₁ ≠ 0) (hc₁r : ‖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⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
have neg : ∀ (i : ι) (hi : i ∈ I), ‖c i‖ ≤ ‖c₁‖
Tactic: refine ⟨c₁, .inl hc₁, fun i hi ↦ ?_, hc₁r⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ egauge 𝕜 (I.pi (α := E) U) x < r
have 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
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]