awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
⊢ egauge 𝕜 (I.pi (α := E) U) x < r
have refine : x ∈ c₀ • I.pi (α := E) U
Tactic: refine egauge_lt_iff.2 ⟨c₀, ?_, 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
c₀ : 𝕜
hc₀ : c₀ ≠ 0 ∨ I = univ
hc₀I : ∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖
hc₀r : ‖c₀‖ₑ < r
⊢ x ∈ c₀ • I.pi (α := E) U
have rw : x ∈ I.pi (α := E) (c₀ • U)
Tactic: rw [smul_set_pi₀' hc₀]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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 𝕜 (closedBall 0 (↑r : ℝ)) x
have rw : ∀ (c : 𝕜), x ∈ HSMul.hSMul (β := Set E) c (closedBall 0 (↑r : ℝ)) → ‖x‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ
Tactic: rw [le_egauge_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
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
⊢ enorm.{u_2} (E := E) ((fun (x : E) ↦ c • x) y) / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ
have hy₁ : ‖y‖₊ ≤ r
Tactic: rw [mem_closedBall_zero_iff, ← coe_nnnorm, NNReal.coe_le_coe] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ enorm.{u_2} (E := E) ((fun (x : E) ↦ c • x) y) / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ
have rw : ‖c‖ₑ * ‖y‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ
Tactic: rw [enorm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ‖c‖ₑ * ‖y‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ
have h : ‖c‖ₑ * ‖y‖ₑ ≤ ‖c‖ₑ * (↑r : ℝ≥0∞)
Tactic: apply ENNReal.div_le_of_le_mul
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ ‖c‖ₑ * ‖y‖ₑ ≤ ‖c‖ₑ * (↑r : ℝ≥0∞)
have h : ‖y‖ₑ ≤ (↑r : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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 := ⋯ }
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
have inl : ∀ (h₀ : Ne (α := ℝ≥0) 0 0 ∨ ‖x‖ ≠ 0), egauge 𝕜 (ball 0 (↑0 : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑0 : ℝ≥0∞)
Tactic: rcases eq_zero_or_pos r with rfl | hr
Cleared hypotheses: r, h₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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∞)
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
have inr : ∀ (hr : 0 < r), egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
Tactic: rcases eq_zero_or_pos r with rfl | hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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 ≤ ‖c‖ₑ * ‖x‖ₑ / (↑0 : ℝ≥0∞)
have inl : egauge 𝕜 (ball 0 (↑0 : ℝ)) x ≤ ∞
Tactic: rw [ENNReal.coe_zero, ENNReal.div_zero (mul_ne_zero _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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 ≤ ∞
⊢ egauge 𝕜 (ball 0 (↑0 : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑0 : ℝ≥0∞)
have rw : ‖c‖ₑ ≠ 0
Tactic: rw [ENNReal.coe_zero, ENNReal.div_zero (mul_ne_zero _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ egauge 𝕜 (ball 0 (↑0 : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑0 : ℝ≥0∞)
have rw₁ : ‖x‖ₑ ≠ 0
Tactic: rw [ENNReal.coe_zero, ENNReal.div_zero (mul_ne_zero _ _)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
have inr : ∀ (hx : ‖x‖ = 0), egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
Tactic: rcases eq_or_ne ‖x‖ 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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∞)
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
have inr₁ : ∀ (hx : ‖x‖ ≠ 0), egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
Tactic: rcases eq_or_ne ‖x‖ 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (hypothesis)
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
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
have hx' : ‖x‖ₑ = 0
Tactic: have hx' : ‖x‖ₑ = 0 := by simpa [enorm, ← coe_nnnorm, NNReal.coe_eq_zero] using hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
have inr : ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ HSMul.hSMul (β := Set E) c (ball 0 (↑r : ℝ))
Tactic: simp only [hx', mul_zero, ENNReal.zero_div, nonpos_iff_eq_zero, egauge_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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 : ℝ))
have inr : ∀ (c : 𝕜) (hc : c ∉ {0}), x ∈ HSMul.hSMul (β := Set E) c (ball 0 (↑r : ℝ))
Tactic: refine (frequently_iff_neBot.2 (inferInstance : NeBot (𝓝[≠] (0 : 𝕜)))).mono fun c hc ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
have inr : ∀ (a : 𝕜) (ha₀ : a ≠ 0) (har : ‖a • x‖ < (↑r : ℝ)) (hainv : ‖a‖⁻¹ ≤ (↑r : ℝ)⁻¹ * ‖c‖ * ‖x‖),
  egauge 𝕜 (ball 0 (↑r : ℝ)) x ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
Tactic: rcases rescale_to_shell_semi_normed hc hr hx with ⟨a, ha₀, har, -, hainv⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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‖
⊢ (↑‖a‖₊⁻¹ : ℝ≥0∞) ≤ (↑(‖c‖₊ * ‖x‖₊ / r) : ℝ≥0∞)
have rwa : ‖a‖₊⁻¹ ≤ ‖c‖₊ * ‖x‖₊ / r
Tactic: rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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
⊢ (↑‖a‖₊⁻¹ : ℝ≥0∞) ≤ (↑(‖c‖₊ * ‖x‖₊ / r) : ℝ≥0∞)
have rwa₁ : ‖a‖₊⁻¹ ≤ r⁻¹ * (‖c‖₊ * ‖x‖₊)
Tactic: rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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‖₊)
⊢ (↑‖a‖₊⁻¹ : ℝ≥0∞) ≤ (↑(‖c‖₊ * ‖x‖₊ / r) : ℝ≥0∞)
have rwa₂ : ‖a‖₊⁻¹ ≤ r⁻¹ * ‖c‖₊ * ‖x‖₊
Tactic: rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Convex.EGauge (goal)
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 ≤ ‖c‖ₑ * ‖x‖ₑ / (↑r : ℝ≥0∞)
have egauge : (↑‖a‖₊⁻¹ : ℝ≥0∞) ≤ (↑(‖c‖₊ * ‖x‖₊ / r) : ℝ≥0∞)
Tactic: calc
        egauge 𝕜 (ball 0 r) x ≤ ↑(‖a‖₊⁻¹) :=
          egauge_le_of_smul_mem_of_ne (mem_ball_zero_iff.2 har) ha₀
        _ ≤ ↑(‖c‖₊ * ‖x‖₊ / r) := by rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]
        _ ≤ ‖c‖ₑ * ‖x‖ₑ / r := ENNReal.coe_div_le.trans <| by simp [ENNReal.coe_mul, enorm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
h : Set.Nonempty.{u_2} (α := E) ∅
w : E
hx : Membership.mem (γ := Set E) ∅ w
⊢ ∃ (l : StrongDual 𝕜 E),
    Eq.{u_2 + 1} (α := Set E) ∅
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
x : E
hx : x ∈ B
⊢ x ∈ A
have obtain : ∀ (w : StrongDual 𝕜 E)
  (hAB :
    IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((w : (a : E) → 𝕜) y : 𝕜) ((w : (a : E) → 𝕜) x : 𝕜)})
  (hx :
    Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((w : (a : E) → 𝕜) y : 𝕜) ((w : (a : E) → 𝕜) x : 𝕜)} x),
  x ∈ A
Tactic: obtain ⟨_, rfl⟩ := hAB ⟨x, hx⟩
Cleared hypotheses: B, hAB, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ (l : StrongDual 𝕜 E),
    C = {x : E | x ∈ B ∧ ∀ y ∈ B, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
have obtain : ∀ (l : StrongDual 𝕜 E)
  (hC :
    IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)})
  (hCB : {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} ⊆ B)
  (hw :
    Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} w),
  ∃ (l_1 : StrongDual 𝕜 E),
    Eq.{u_2 + 1} (α := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
      {x : E | x ∈ B ∧ ∀ y ∈ B, LE.le.{u_1} (α := 𝕜) ((l_1 : (a : E) → 𝕜) y : 𝕜) ((l_1 : (a : E) → 𝕜) x : 𝕜)}
Tactic: obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩
Cleared hypotheses: C, hC, hCB, hw
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
hB : B.Nonempty
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
have obtain : ∀ (l : StrongDual 𝕜 E)
  (hAB :
    IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)})
  (hB :
    Set.Nonempty.{u_2} (α := E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}),
  ∃ (l_1 : StrongDual 𝕜 E) (a : 𝕜),
    Eq.{u_2 + 1} (α := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
      {x : E | x ∈ A ∧ a ≤ (l_1 : (a : E) → 𝕜) x}
Tactic: obtain ⟨l, rfl⟩ := hAB hB
Cleared hypotheses: B, hAB, hB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
A : Set E
l : StrongDual 𝕜 E
hAB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
hB :
  Set.Nonempty.{u_2} (α := E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
⊢ ∃ (l_1 : StrongDual 𝕜 E) (a : 𝕜),
    Eq.{u_2 + 1} (α := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
      {x : E | x ∈ A ∧ a ≤ (l_1 : (a : E) → 𝕜) x}
have obtain : ∀ (w : E)
  (hw :
    Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)} w),
  ∃ (l_1 : StrongDual 𝕜 E) (a : 𝕜),
    Eq.{u_2 + 1} (α := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
      {x : E | x ∈ A ∧ a ≤ (l_1 : (a : E) → 𝕜) x}
Tactic: obtain ⟨w, hw⟩ := hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
have inl : ∀ (hAB : IsExposed 𝕜 A ∅),
  ∃ (l : StrongDual 𝕜 E) (a : 𝕜), Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
Tactic: obtain rfl | hB := B.eq_empty_or_nonempty
Cleared hypotheses: B, hAB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : Nontrivial 𝕜
A B : Set E
hAB : IsExposed 𝕜 A B
inl :
  ∀ (hAB : IsExposed 𝕜 A ∅),
    ∃ (l : StrongDual 𝕜 E) (a : 𝕜), Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
have inr : ∀ (hB : B.Nonempty), ∃ (l : StrongDual 𝕜 E) (a : 𝕜), B = {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
Tactic: obtain rfl | hB := B.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ ∃ (l : StrongDual 𝕜 E) (a : 𝕜), Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ a ≤ (l : (a : E) → 𝕜) x}
have inl : Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ LE.le.{u_1} (α := 𝕜) (1 : 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜)}
Tactic: refine ⟨0, 1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
⊢ Eq.{u_2 + 1} (α := Set E) ∅ {x : E | x ∈ A ∧ LE.le.{u_1} (α := 𝕜) (1 : 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜)}
have inl : ∀ (x : E), x ∉ {x : E | x ∈ A ∧ LE.le.{u_1} (α := 𝕜) (1 : 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜)}
Tactic: rw [eq_comm, eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : LE.le.{u_1} (α := 𝕜) (1 : 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜)
⊢ False
have h₁ : LE.le.{u_1} (α := 𝕜) 1 0
Tactic: rw [ContinuousLinearMap.zero_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : Nontrivial 𝕜
A : Set E
hAB : IsExposed 𝕜 A ∅
x : E
h : LE.le.{u_1} (α := 𝕜) 1 0
⊢ False
have this : ¬LE.le.{u_1} (α := 𝕜) 1 0
Tactic: have : ¬(1 : 𝕜) ≤ 0 := not_le_of_gt zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
A B C : Set E
hB : IsExposed 𝕜 A B
hC : IsExposed 𝕜 A C
w : E
hwB : w ∈ B
hwC : w ∈ C
⊢ ∃ (l : StrongDual 𝕜 E),
    B ∩ C = {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
have obtain : ∀ (l₁ : StrongDual 𝕜 E)
  (hB :
    IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)})
  (hwB :
    Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} w),
  ∃ (l : StrongDual 𝕜 E),
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩ C =
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
Tactic: obtain ⟨l₁, rfl⟩ := hB ⟨w, hwB⟩
Cleared hypotheses: B, hB, hwB
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
A C : Set E
hC : IsExposed 𝕜 A C
w : E
hwC : w ∈ C
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)}
hwB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} w
⊢ ∃ (l : StrongDual 𝕜 E),
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩ C =
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
have obtain : ∀ (l₂ : StrongDual 𝕜 E)
  (hC :
    IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
  (hwC :
    Membership.mem (γ := Set E)
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)} w),
  ∃ (l : StrongDual 𝕜 E),
    Eq.{u_2 + 1} (α := Set E)
      ({x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
Tactic: obtain ⟨l₂, rfl⟩ := hC ⟨w, hwC⟩
Cleared hypotheses: C, hC, hwC
-- Lean 4 proof step from Mathlib.Analysis.Convex.Exposed (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace 𝕜
inst_1 : Ring 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : AddCommMonoid E
inst_4 : TopologicalSpace E
inst_5 : Module 𝕜 E
inst_6 : IsOrderedRing 𝕜
inst_7 : ContinuousAdd 𝕜
A : Set E
w : E
l₁ : StrongDual 𝕜 E
hB : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)}
hwB :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} w
l₂ : StrongDual 𝕜 E
hC : IsExposed 𝕜 A {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)}
hwC :
  Membership.mem (γ := Set E)
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)} w
⊢ ∃ (l : StrongDual 𝕜 E),
    Eq.{u_2 + 1} (α := Set E)
      ({x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩
        {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
      {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l : (a : E) → 𝕜) y : 𝕜) ((l : (a : E) → 𝕜) x : 𝕜)}
have refine_1 : Subset.{u_2} (α := Set E)
  ({x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ : (a : E) → 𝕜) y : 𝕜) ((l₁ : (a : E) → 𝕜) x : 𝕜)} ∩
    {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₂ : (a : E) → 𝕜) y : 𝕜) ((l₂ : (a : E) → 𝕜) x : 𝕜)})
  {x : E | x ∈ A ∧ ∀ y ∈ A, LE.le.{u_1} (α := 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) y : 𝕜) ((l₁ + l₂ : (a : E) → 𝕜) x : 𝕜)}
Tactic: refine ⟨l₁ + l₂, Subset.antisymm ?_ ?_⟩