awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
y : E
hy : y ∈ s
h : a • y = r⁻¹ • x
hr : 0 < r
inr : (a⁻¹ • r⁻¹) • x ∈ s
inr₁ : a⁻¹ • r⁻¹ • x ∈ s
⊢ (a • r)⁻¹ • x ∈ s
have inr₂ : a⁻¹ • a • y ∈ s
Tactic: rwa [smul_inv₀, smul_assoc, ← h, inv_smul_smul₀ ha'.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
hx : r⁻¹ • x ∈ s
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (a⁻¹ • r) ∧ ∃ y ∈ s, a • y = (a⁻¹ • r)⁻¹ • x
have hr₁ : 0 < r
Tactic: rw [mem_Ioi] at hr ⊢
Cleared hypotheses: hr, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
⊢ 0 < a⁻¹ • r ∧ ∃ y ∈ s, a • y = (a⁻¹ • r)⁻¹ • x
have inr : a • r⁻¹ • x = (a⁻¹ • r)⁻¹ • x
Tactic: refine ⟨smul_pos (inv_pos.2 ha') hr, r⁻¹ • x, hx, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
⊢ a • r⁻¹ • x = (a⁻¹ • r)⁻¹ • x
have inr : a • r⁻¹ • x = (a⁻¹⁻¹ • r⁻¹) • x
Tactic: rw [smul_inv₀, smul_assoc, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
inr : a • r⁻¹ • x = (a⁻¹⁻¹ • r⁻¹) • x
⊢ a • r⁻¹ • x = (a⁻¹ • r)⁻¹ • x
have inr₁ : a • r⁻¹ • x = a⁻¹⁻¹ • r⁻¹ • x
Tactic: rw [smul_inv₀, smul_assoc, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : MulActionWithZero α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
hr : 0 < r
hx : r⁻¹ • x ∈ s
inr : a • r⁻¹ • x = (a⁻¹⁻¹ • r⁻¹) • x
inr₁ : a • r⁻¹ • x = a⁻¹⁻¹ • r⁻¹ • x
⊢ a • r⁻¹ • x = (a⁻¹ • r)⁻¹ • x
have inr₂ : a • r⁻¹ • x = a • r⁻¹ • x
Tactic: rw [smul_inv₀, smul_assoc, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
⊢ gauge (a • s) = |a|⁻¹ • gauge s
have rw : gauge (a • s) = gauge (|a| • s)
Tactic: rw [← gauge_smul_left_of_nonneg (abs_nonneg a)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
⊢ gauge (a • s) = gauge (|a| • s)
have inl : ∀ (h : |a| = a), gauge (a • s) = gauge (|a| • s)
Tactic: obtain h | h := abs_choice a
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
inl : ∀ (h : |a| = a), gauge (a • s) = gauge (|a| • s)
⊢ gauge (a • s) = gauge (|a| • s)
have inr : ∀ (h : |a| = -a), gauge (a • s) = gauge (|a| • s)
Tactic: obtain h | h := abs_choice a
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = a
⊢ gauge (a • s) = gauge (|a| • s)
have inl : gauge (a • s) = gauge (a • s)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
⊢ gauge (a • s) = gauge (|a| • s)
have inr : gauge (a • s) = gauge (a • -s)
Tactic: rw [h, Set.neg_smul_set, ← Set.smul_set_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
⊢ gauge (a • s) = gauge (a • -s)
have inr : s = -s
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
⊢ s = -s
have inr : ∀ (y : E), y ∈ s ↔ y ∈ -s
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
y : E
⊢ y ∈ s ↔ y ∈ -s
have inr : ∀ (hy : y ∈ -s), y ∈ s
Tactic: refine ⟨symmetric _, fun hy => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
α : Type u_3
inst_2 : Field α
inst_3 : LinearOrder α
inst_4 : IsStrictOrderedRing α
inst_5 : MulActionWithZero α ℝ
inst_6 : IsStrictOrderedModule α ℝ
inst_7 : Module α E
inst_8 : SMulCommClass α ℝ ℝ
inst_9 : IsScalarTower α ℝ ℝ
inst_10 : IsScalarTower α ℝ E
s : Set E
symmetric : ∀ x ∈ s, -x ∈ s
a : α
h : |a| = -a
y : E
hy : y ∈ -s
⊢ y ∈ s
have inr : - -y ∈ s
Tactic: rw [← neg_neg y]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ Eq (α := ℝ) (sInf {r_1 : ℝ | 0 < r_1 ∧ ‖r‖ • x ∈ r_1 • s}) (sInf {r_1 : ℝ | 0 < r_1 ∧ r • x ∈ r_1 • s})
have e_a : ∀ (θ : ℝ), 0 < θ ∧ ‖r‖ • x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s
Tactic: congr with θ
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ 0 < θ ∧ ‖r‖ • x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s
have e_a : 0 < θ ∧ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖r‖ : 𝕜) x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s
Tactic: rw [@RCLike.real_smul_eq_coe_smul 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
⊢ 0 < θ ∧ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑‖r‖ : 𝕜) x ∈ θ • s ↔ 0 < θ ∧ r • x ∈ θ • s
have e_a : ∀ (hθ : 0 < θ), norm.{u_1} (E := 𝕜) (↑‖r‖ : 𝕜) = ‖r‖
Tactic: refine and_congr_right fun hθ => (hs.smul _).smul_mem_iff ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
hθ : 0 < θ
⊢ norm.{u_1} (E := 𝕜) (↑‖r‖ : 𝕜) = ‖r‖
have e_a : |‖r‖| = ‖r‖
Tactic: rw [RCLike.norm_ofReal, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
θ : ℝ
hθ : 0 < θ
e_a : |‖r‖| = ‖r‖
⊢ norm.{u_1} (E := 𝕜) (↑‖r‖ : 𝕜) = ‖r‖
have e_a₁ : ‖r‖ = ‖r‖
Tactic: rw [RCLike.norm_ofReal, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (r • x) = ‖r‖ * gauge s x
have rw : gauge s (r • x) = ‖r‖ • gauge s x
Tactic: rw [← smul_eq_mul, ← gauge_smul_of_nonneg (norm_nonneg r), gauge_norm_smul hs]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
rw : gauge s (r • x) = ‖r‖ • gauge s x
⊢ gauge s (r • x) = ‖r‖ * gauge s x
have rw₁ : gauge s (r • x) = gauge s (‖r‖ • x)
Tactic: rw [← smul_eq_mul, ← gauge_smul_of_nonneg (norm_nonneg r), gauge_norm_smul hs]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : RCLike 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
rw : gauge s (r • x) = ‖r‖ • gauge s x
rw₁ : gauge s (r • x) = gauge s (‖r‖ • x)
⊢ gauge s (r • x) = ‖r‖ * gauge s x
have rw₂ : gauge s (r • x) = gauge s (r • x)
Tactic: rw [← smul_eq_mul, ← gauge_smul_of_nonneg (norm_nonneg r), gauge_norm_smul hs]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
⊢ u ∈ comap (gauge s) (𝓝 0)
have rcases : ∀ (r : ℝ) (hr₀ : r > 0) (hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u), u ∈ comap (gauge s) (𝓝 0)
Tactic: rcases (hb hu).exists_pos with ⟨r, hr₀, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
x : E
⊢ x ∈ gauge s ⁻¹' {x : ℝ | x < r⁻¹} → x ∈ u
have h : ∀ (hx : gauge s x < r⁻¹), x ∈ u
Tactic: (hx : gauge s x < r⁻¹)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
⊢ u ∈ comap (gauge s) (𝓝 0)
have h : ∀ (x : E) (hx : gauge s x < r⁻¹), x ∈ u
Tactic: filter_upwards [preimage_mem_comap (gt_mem_nhds (inv_pos.2 hr₀))] with x (hx : gauge s x < r⁻¹)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
x : E
hx : gauge s x < r⁻¹
⊢ x ∈ u
have h : ∀ (c : ℝ) (hc₀ : 0 < c) (hcr : c < r⁻¹) (y : E) (hy : y ∈ s) (hx : gauge s ((fun (x : E) ↦ c • x) y) < r⁻¹),
  (fun (x : E) ↦ c • x) y ∈ u
Tactic: rcases exists_lt_of_gauge_lt ha hx with ⟨c, hc₀, hcr, y, hy, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun (x : E) ↦ c • x) y) < r⁻¹
⊢ (fun (x : E) ↦ c • x) y ∈ u
have hrc : r < c⁻¹
Tactic: have hrc := (lt_inv_comm₀ hr₀ hc₀).2 hcr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : Membership.mem (γ := Filter E) (𝓝 0) u
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun (x : E) ↦ c • x) y) < r⁻¹
hrc : r < c⁻¹
⊢ (fun (x : E) ↦ c • x) y ∈ u
have h : ∀ (z : E) (hz : z ∈ u) (hy : (fun (x : E) ↦ c⁻¹ • x) z ∈ s)
  (hx : gauge s ((fun (x : E) ↦ c • x) ((fun (x : E) ↦ c⁻¹ • x) z)) < r⁻¹),
  (fun (x : E) ↦ c • x) ((fun (x : E) ↦ c⁻¹ • x) z) ∈ u
Tactic: rcases hr c⁻¹ (hrc.le.trans (le_abs_self _)) hy with ⟨z, hz, rfl⟩
Cleared hypotheses: y, hy, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
⊢ gauge s x = 0 ↔ x = 0
have refine : ∀ (h₀ : gauge s x = 0) (hne : x ≠ 0), False
Tactic: refine ⟨fun h₀ ↦ by_contra fun (hne : x ≠ 0) ↦ ?_, fun h ↦ h.symm ▸ gauge_zero⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
⊢ False
have this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
Tactic: have : {x}ᶜ ∈ comap (gauge s) (𝓝 0) :=
    comap_gauge_nhds_zero_le hs hb (isOpen_compl_singleton.mem_nhds hne.symm)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
⊢ False
have rcases : ∀ (r : ℝ) (hr₀ : 0 < r) (hr : gauge s ⁻¹' {b : ℝ | |b| < r} ⊆ {x}ᶜ), False
Tactic: rcases ((nhds_basis_zero_abs_lt _).comap _).mem_iff.1 this with ⟨r, hr₀, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
have H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 (HSMul.hSMul (α := ℝ) 1⁻¹ x))
Tactic: have H₁ : Tendsto (fun r : ℝ ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 ((1 : ℝ)⁻¹ • x)) :=
    ((tendsto_id.inv₀ one_ne_zero).smul tendsto_const_nhds).mono_left inf_le_left
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 (HSMul.hSMul (α := ℝ) 1⁻¹ x))
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
have H₂ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
Tactic: rw [inv_one, one_smul] at H₁
Cleared hypotheses: H₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
have h : ∀ (r : ℝ) (h₁ : Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ r⁻¹ • x) ⁻¹' s) r)
  (h₂ : Membership.mem (γ := Set ℝ) (Ioo 0 1) r), x ∈ r • s ∧ 0 < r ∧ r < 1
Tactic: filter_upwards [H₁ (mem_interior_iff_mem_nhds.1 hx), Ioo_mem_nhdsLT one_pos] with r h₁ h₂
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
have H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
Tactic: have H₂ : ∀ᶠ r in 𝓝[<] (1 : ℝ), x ∈ r • s ∧ 0 < r ∧ r < 1 := by
    filter_upwards [H₁ (mem_interior_iff_mem_nhds.1 hx), Ioo_mem_nhdsLT one_pos] with r h₁ h₂
    exact ⟨(mem_smul_set_iff_inv_smul_mem₀ h₂.1.ne' _ _).2 h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun (r : ℝ) ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
⊢ Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
have rcases : ∀ (r : ℝ) (hxr : x ∈ r • s) (hr₀ : 0 < r) (hr₁ : r < 1), Membership.mem (γ := Set E) {x : E | gauge s x < 1} x
Tactic: rcases H₂.exists with ⟨r, hxr, hr₀, hr₁⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen[inst_2] s
⊢ {x : E | gauge s x < 1} = s
have refine : s ⊆ {x : E | gauge s x < 1}
Tactic: refine (gauge_lt_one_subset_self hs₁ ‹_› <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀).antisymm ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : IsOpen[inst_2] s
⊢ s ⊆ {x : E | gauge s x < 1}
have h : s = interior s
Tactic: convert! interior_subset_gauge_lt_one s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
⊢ gauge s x < ε
have this : ε⁻¹ • x ∈ s
Tactic: have : ε⁻¹ • x ∈ s := by rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (hypothesis)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
⊢ gauge s x < ε
have h_gauge_lt : gauge s (ε⁻¹ • x) < 1
Tactic: have h_gauge_lt := gauge_lt_one_of_mem_of_isOpen hs₂ this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
⊢ gauge s x < ε
have rwa : ∀ (h_gauge_lt : ε⁻¹ • gauge s x < 1), gauge s x < ε
Tactic: rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one]
    at h_gauge_lt
Cleared hypotheses: h_gauge_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
rwa : ∀ (h_gauge_lt : ε⁻¹ • gauge s x < 1), gauge s x < ε
⊢ gauge s x < ε
have rwa₁ : ∀ (h_gauge_lt : ε⁻¹ * gauge s x < 1), gauge s x < ε
Tactic: rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one]
    at h_gauge_lt
Cleared hypotheses: h_gauge_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
rwa : ∀ (h_gauge_lt : ε⁻¹ • gauge s x < 1), gauge s x < ε
rwa₁ : ∀ (h_gauge_lt : ε⁻¹ * gauge s x < 1), gauge s x < ε
⊢ gauge s x < ε
have rwa₂ : ∀ (h_gauge_lt : gauge s x < ε * 1), gauge s x < ε
Tactic: rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one]
    at h_gauge_lt
Cleared hypotheses: h_gauge_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst_2] s
hx : x ∈ ε • s
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s (ε⁻¹ • x) < 1
rwa : ∀ (h_gauge_lt : ε⁻¹ • gauge s x < 1), gauge s x < ε
rwa₁ : ∀ (h_gauge_lt : ε⁻¹ * gauge s x < 1), gauge s x < ε
rwa₂ : ∀ (h_gauge_lt : gauge s x < ε * 1), gauge s x < ε
⊢ gauge s x < ε
have rwa₃ : ∀ (h_gauge_lt : gauge s x < ε), gauge s x < ε
Tactic: rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one]
    at h_gauge_lt
Cleared hypotheses: h_gauge_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ico 0 1) r → r • x ∈ s
have h₁ : ∀ (hr₀ : 0 ≤ r) (hr₁ : r < 1), r • x ∈ s
Tactic: ⟨hr₀, hr₁⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Gauge (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
have h₁ : ∀ (r : ℝ) (hr₀ : 0 ≤ r) (hr₁ : r < 1), r • x ∈ s
Tactic: filter_upwards [Ico_mem_nhdsLT one_pos] with r ⟨hr₀, hr₁⟩