awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
rw : a • s = b • b⁻¹ • a • s
⊢ a • s = b • (b⁻¹ • a) • s
have rw₁ : a • s = a • s
Tactic: rw [smul_assoc, smul_inv_smul₀ hb]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖b⁻¹ • a‖ ≤ 1
have rw : ‖a‖ / ‖b‖ ≤ 1
Tactic: rw [norm_smul, norm_inv, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ a • s ⊆ b • s
have a₁ : a • s = b • (b⁻¹ • a) • s
Tactic: calc
      a • s = b • (b⁻¹ • a) • s := by rw [smul_assoc, smul_inv_smul₀ hb]
      _ ⊆ b • s := smul_set_mono <| hs _ <| by
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ h (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
⊢ b • x ∈ s
have inl : ∀ (ha : HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x ∈ s) (hba : ‖b‖ ≤ norm.{u_1} (E := 𝕜) 0), b • x ∈ s
Tactic: rcases eq_or_ne a 0 with rfl | ha₀
Cleared hypotheses: a, ha, hba
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
inl : ∀ (ha : HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 x ∈ s) (hba : ‖b‖ ≤ norm.{u_1} (E := 𝕜) 0), b • x ∈ s
⊢ b • x ∈ s
have inr : ∀ (ha₀ : a ≠ 0), b • x ∈ s
Tactic: rcases eq_or_ne a 0 with rfl | ha₀
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ (a⁻¹ • b) • a • x ∈ s
have refine : ‖a⁻¹ • b‖ ≤ 1
Tactic: refine hs.smul_mem ?_ ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖a⁻¹ • b‖ ≤ 1
have rw : ‖b‖ / ‖a‖ ≤ 1
Tactic: rw [norm_smul, norm_inv, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ (a⁻¹ • b) • a • x = b • x
have rw : a • (a⁻¹ • b) • x = b • x
Tactic: rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
rw : a • (a⁻¹ • b) • x = b • x
⊢ (a⁻¹ • b) • a • x = b • x
have rw₁ : a • a⁻¹ • b • x = b • x
Tactic: rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
rw : a • (a⁻¹ • b) • x = b • x
rw₁ : a • a⁻¹ • b • x = b • x
⊢ (a⁻¹ • b) • a • x = b • x
have rw₂ : b • x = b • x
Tactic: rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ b • x ∈ s
have a₁ : (a⁻¹ • b) • a • x ∈ s
Tactic: calc
      (a⁻¹ • b) • a • x ∈ s := by
        refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)
      (a⁻¹ • b) • a • x = b • x := by rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormedRing 𝕝
inst_4 : Module 𝕜 𝕝
inst_5 : NormSMulClass 𝕜 𝕝
inst_6 : SMulWithZero 𝕝 E
inst_7 : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst_8 : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
a₁ : (a⁻¹ • b) • a • x ∈ s
⊢ b • x ∈ s
have a₂ : (a⁻¹ • b) • a • x = b • x
Tactic: calc
      (a⁻¹ • b) • a • x ∈ s := by
        refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)
      (a⁻¹ • b) • a • x = b • x := by rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • s
have ha₁ : norm.{u_1} (E := 𝕜) 1 ≤ ‖a‖
Tactic: rw [← @norm_one 𝕜] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • insert 0 (interior A) ⊆ insert 0 (interior A)
have inl : ∀ (ha : norm.{u_1} (E := 𝕜) 0 ≤ 1),
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 (insert 0 (interior A)) ⊆ insert 0 (interior A)
Tactic: obtain rfl | h := eq_or_ne a 0
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
inl :
  ∀ (ha : norm.{u_1} (E := 𝕜) 0 ≤ 1),
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 (insert 0 (interior A)) ⊆ insert 0 (interior A)
⊢ a • insert 0 (interior A) ⊆ insert 0 (interior A)
have inr : ∀ (h : a ≠ 0), a • insert 0 (interior A) ⊆ insert 0 (interior A)
Tactic: obtain rfl | h := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : norm.{u_1} (E := 𝕜) 0 ≤ 1
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 (insert 0 (interior A)) ⊆ insert 0 (interior A)
have inl : 0 ⊆ insert 0 (interior A)
Tactic: rw [zero_smul_set]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : norm.{u_1} (E := 𝕜) 0 ≤ 1
inl : 0 ⊆ insert 0 (interior A)
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 (insert 0 (interior A)) ⊆ insert 0 (interior A)
have inl₁ : (insert 0 (interior A)).Nonempty
Tactic: rw [zero_smul_set]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ a • insert 0 (interior A) ⊆ insert 0 (interior A)
have inr : insert 0 ((fun (x : E) ↦ a • x) '' interior A) ⊆ insert 0 (interior A)
Tactic: rw [← image_smul, image_insert_eq, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ insert 0 ((fun (x : E) ↦ a • x) '' interior A) ⊆ insert 0 (interior A)
have inr : (fun (x : E) ↦ a • x) '' interior A ⊆ interior A
Tactic: apply insert_subset_insert
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
A : Set E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ interior A
⊢ Balanced 𝕜 (interior A)
have rw : Balanced 𝕜 (insert 0 (interior A))
Tactic: rw [← insert_eq_self.2 h]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : Balanced 𝕜 s
this :
  Convex.{u_1, u_3} 𝕜 (E := E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) s)
have rw : ∀ (hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s)
  (this :
    Convex.{u_1, u_3} 𝕜 (E := E)
      {x : E |
        ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)})
  ⦃a : 𝕜⦄,
  ‖a‖ ≤ 1 →
    ∀ ⦃x : E⦄,
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x →
        Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)
Tactic: rw [balanced_iff_smul_mem] at hs ⊢
Cleared hypotheses: hs, this
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this :
  Convex.{u_1, u_3} 𝕜 (E := E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
⊢ ∀ ⦃a : 𝕜⦄,
    ‖a‖ ≤ 1 →
      ∀ ⦃x : E⦄,
        Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x →
          Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)
have refine : ∀ (a : 𝕜) (ha : ‖a‖ ≤ 1) (x : E) (hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x),
  s ⊆
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
Tactic: refine fun a ha x hx => convexHull_min ?_ this hx a ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : Balanced 𝕜 s
⊢ Balanced.{u_1, u_3} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) s)
have suffices : Convex.{u_1, u_3} 𝕜 (E := E)
  {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
Tactic: suffices Convex 𝕜 { x | ∀ a : 𝕜, ‖a‖ ≤ 1 → a • x ∈ convexHull 𝕜 s } by
    rw [balanced_iff_smul_mem] at hs ⊢
    refine fun a ha x hx => convexHull_min ?_ this hx a ha
    exact fun y hy a ha => subset_convexHull 𝕜 s (hs ha hy)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx :
  Membership.mem (γ := Set E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
    x
y : E
hy :
  Membership.mem (γ := Set E)
    {x : E | ∀ (a : 𝕜), ‖a‖ ≤ 1 → Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • x)}
    y
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (a • (u • x + v • y))
have rw : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (u • a • x + v • a • y)
Tactic: rw [smul_add, ← smul_comm u, ← smul_comm v]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
S : Type u_7
inst_3 : SetLike S E
inst_4 : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 (↑V : Set E)
⊢ (↑V : Set E) = univ
have rw : ∀ (x : E), x ∈ (↑V : Set E)
Tactic: rw [eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
S : Type u_7
inst_3 : SetLike S E
inst_4 : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 (↑V : Set E)
x : E
⊢ x ∈ (↑V : Set E)
have obtain : ∀ (c : 𝕜) (hc : c • x ∈ (↑V : Set E)) (hc' : Membership.mem (γ := Set 𝕜) {0}ᶜ c), x ∈ (↑V : Set E)
Tactic: obtain ⟨c, hc, hc'⟩ :=
    ((absorbent_iff_eventually_nhdsNE_zero.mp hV x).and eventually_mem_nhdsWithin).exists
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
S : Type u_7
inst_3 : SetLike S E
inst_4 : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 (↑V : Set E)
x : E
c : 𝕜
hc : c • x ∈ (↑V : Set E)
hc' : Membership.mem (γ := Set 𝕜) {0}ᶜ c
⊢ x ∈ (↑V : Set E)
have rw : c⁻¹ • c • x ∈ (↑V : Set E)
Tactic: rw [← inv_smul_smul₀ hc' x]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
have refine : ∀ (h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s) (a : ℝ) (ha : ‖a‖ ≤ 1) (x : E) (hx : x ∈ s), a • x ∈ s
Tactic: refine ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
have rw : ∀ (ha : -1 ≤ a ∧ a ≤ 1) (x : E) (hx : x ∈ s), a • x ∈ s
Tactic: rw [Real.norm_eq_abs, abs_le] at ha
Cleared hypotheses: ha, x, hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Basic (goal)
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
have rw : ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s
Tactic: rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
⊢ IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
have refine : ∀ (hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A) (V : Set E) (hV : Membership.mem (γ := Filter E) (𝓝 0) V), Absorbs 𝕜 V A
Tactic: refine ⟨fun hA i hi => hA (h.mem_of_mem hi), fun hA V hV => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
ι : Type u_5
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
q : ι → Prop
s : ι → Set E
A : Set E
h : HasBasis (𝓝 0) q s
hA : ∀ (i : ι), q i → Absorbs 𝕜 (s i) A
V : Set E
hV : Membership.mem (γ := Filter E) (𝓝 0) V
⊢ Absorbs 𝕜 V A
have rcases : ∀ (i : ι) (hi : q i) (hV : s i ⊆ V), Absorbs 𝕜 V A
Tactic: rcases h.mem_iff.mp hV with ⟨i, hi, hV⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
⊢ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
have x : Finite.{u_6 + 1} (↑I : Type u_6)
Tactic: have _ := hI.to_subtype
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
h : Finite.{u_6 + 1} (↑I : Type u_6)
⊢ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
have rw : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ (x : (↑I : Type u_6)), s (↑x : ι)) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
Tactic: rw [biUnion_eq_iUnion, isVonNBounded_iUnion, Subtype.forall]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
h : Finite.{u_6 + 1} (↑I : Type u_6)
rw : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ (x : (↑I : Type u_6)), s (↑x : ι)) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
⊢ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
have rw₁ : (∀ (i : (↑I : Type u_6)), IsVonNBounded 𝕜 (s (↑i : ι))) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
Tactic: rw [biUnion_eq_iUnion, isVonNBounded_iUnion, Subtype.forall]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
ι : Type u_6
I : Set ι
hI : I.Finite
s : ι → Set E
h : Finite.{u_6 + 1} (↑I : Type u_6)
rw : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ (x : (↑I : Type u_6)), s (↑x : ι)) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
rw₁ : (∀ (i : (↑I : Type u_6)), IsVonNBounded 𝕜 (s (↑i : ι))) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
⊢ IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
have rw₂ : (∀ (a : ι) (b : a ∈ I), IsVonNBounded 𝕜 (s (↑(Subtype.mk (p := fun (a : ι) ↦ a ∈ I) a b) : ι))) ↔
  ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
Tactic: rw [biUnion_eq_iUnion, isVonNBounded_iUnion, Subtype.forall]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
S : Set (Set E)
hS : S.Finite
⊢ IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
have rw : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
Tactic: rw [sUnion_eq_biUnion, isVonNBounded_biUnion hS]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
inst_2 : Zero E
inst_3 : TopologicalSpace E
S : Set (Set E)
hS : S.Finite
rw : IsVonNBounded.{u_1, u_3} 𝕜 (E := E) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
have rw₁ : (∀ i ∈ S, IsVonNBounded 𝕜 i) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s
Tactic: rw [sUnion_eq_biUnion, isVonNBounded_biUnion hS]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddZeroClass E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : DistribSMul 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Absorbs 𝕜 U (s + t)
have rcases : ∀ (V : Set E) (hVo : IsOpen[inst_2] V) (hV : 0 ∈ V) (hVU : V + V ⊆ U), Absorbs 𝕜 U (s + t)
Tactic: rcases exists_open_nhds_zero_add_subset hU with ⟨V, hVo, hV, hVU⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s : Set E
hs : IsVonNBounded 𝕜 s
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Absorbs 𝕜 U (-s)
have rw : Absorbs 𝕜 (- -U) (-s)
Tactic: rw [← neg_neg U]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : SeminormedRing 𝕜
inst_1 : AddGroup E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : DistribMulAction 𝕜 E
s t : Set E
hs : IsVonNBounded 𝕜 s
ht : IsVonNBounded 𝕜 t
⊢ IsVonNBounded 𝕜 (s - t)
have rw : IsVonNBounded 𝕜 (s + -t)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_6
E : Type u_7
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ Tendsto.{u_6, u_7} (β := Set E) (fun (x : 𝕜) ↦ x • S) (𝓝 0) (smallSets (𝓝 0))
have rw : IsVonNBounded 𝕜 S ↔ ∀ (t : Set E), Membership.mem (γ := Filter E) (𝓝 0) t → ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t
Tactic: rw [tendsto_smallSets_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_6
E : Type u_7
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
S : Set E
⊢ IsVonNBounded 𝕜 S ↔ ∀ (t : Set E), Membership.mem (γ := Filter E) (𝓝 0) t → ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ t
have refine : ∀ (V : Set E) (hV : Membership.mem (γ := Filter E) (𝓝 0) V), Absorbs 𝕜 V S ↔ ∀ᶠ (x : 𝕜) in 𝓝 0, x • S ⊆ V
Tactic: refine forall₂_congr fun V hV ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Bounded (goal)
Goal:
𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst : NormedDivisionRing 𝕜
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_6, u_8} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval (β := E) i '' S)
have simp_rw : Tendsto (β := Set ((i : ι) → E i)) (fun (x : 𝕜) ↦ x • S) (𝓝 0) (smallSets (𝓝 0)) ↔
  ∀ (i : ι), Tendsto.{u_6, u_8} (β := Set (E i)) (fun (x : 𝕜) ↦ x • eval (β := E) i '' S) (𝓝 0) (smallSets (𝓝 0))
Tactic: simp_rw [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf,
    smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff, Function.comp_def,
    ← image_smul, image_image, eval, Pi.smul_apply, Pi.zero_apply]