awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
⊢ z ∈ U
have a : Membership.mem (γ := Set F) (sphere 0 r) z
Tactic: apply hU_sub
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
⊢ x ∈ U
have hz : z ∈ U
Tactic: have hz : z ∈ U := by
    apply hU_sub
    simp_all [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
⊢ x ∈ U
have this : (r⁻¹ * ‖x‖) • z ∈ U
Tactic: have := StarConvex.smul_mem (hU.starConvex zero_mem) hz (by positivity) hr₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
⊢ x ∈ U
have neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₄ : ∀ (this : (‖x‖⁻¹ * (r⁻¹ * ‖x‖ * r)) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₄ : ∀ (this : (‖x‖⁻¹ * (r⁻¹ * ‖x‖ * r)) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₅ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * r⁻¹ * r)) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₄ : ∀ (this : (‖x‖⁻¹ * (r⁻¹ * ‖x‖ * r)) • x ∈ U), x ∈ U
neg₅ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * r⁻¹ * r)) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₆ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * (r⁻¹ * r))) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₄ : ∀ (this : (‖x‖⁻¹ * (r⁻¹ * ‖x‖ * r)) • x ∈ U), x ∈ U
neg₅ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * r⁻¹ * r)) • x ∈ U), x ∈ U
neg₆ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * (r⁻¹ * r))) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₇ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * 1)) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₄ : ∀ (this : (‖x‖⁻¹ * (r⁻¹ * ‖x‖ * r)) • x ∈ U), x ∈ U
neg₅ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * r⁻¹ * r)) • x ∈ U), x ∈ U
neg₆ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * (r⁻¹ * r))) • x ∈ U), x ∈ U
neg₇ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * 1)) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₈ : ∀ (this : (‖x‖⁻¹ * ‖x‖) • x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₄ : ∀ (this : (‖x‖⁻¹ * (r⁻¹ * ‖x‖ * r)) • x ∈ U), x ∈ U
neg₅ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * r⁻¹ * r)) • x ∈ U), x ∈ U
neg₆ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * (r⁻¹ * r))) • x ∈ U), x ∈ U
neg₇ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * 1)) • x ∈ U), x ∈ U
neg₈ : ∀ (this : (‖x‖⁻¹ * ‖x‖) • x ∈ U), x ∈ U
⊢ x ∈ U
have neg₉ : ∀ (this : HSMul.hSMul (α := ℝ) 1 x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Nontrivial F
x_1 : F
r : ℝ
hr : 0 ≤ r
x : F
h : Membership.mem (γ := Set F) (closedBall 0 r) x
U : Set F
hU_sub : sphere 0 r ⊆ U
hU : Convex ℝ U
zero_mem : 0 ∈ U
hr₀ : ¬r = 0
x_zero : ¬x = 0
z : F := (r * ‖x‖⁻¹) • x
hz_def : z = (r * ‖x‖⁻¹) • x
hr₁ : r⁻¹ * ‖x‖ ≤ 1
hz : z ∈ U
this : (r⁻¹ * ‖x‖) • z ∈ U
neg : ∀ (this : (r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₁ : ∀ (this : ((r⁻¹ * ‖x‖) • (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₂ : ∀ (this : (r⁻¹ * ‖x‖ * (r * ‖x‖⁻¹)) • x ∈ U), x ∈ U
neg₃ : ∀ (this : (r⁻¹ * ‖x‖ * r * ‖x‖⁻¹) • x ∈ U), x ∈ U
neg₄ : ∀ (this : (‖x‖⁻¹ * (r⁻¹ * ‖x‖ * r)) • x ∈ U), x ∈ U
neg₅ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * r⁻¹ * r)) • x ∈ U), x ∈ U
neg₆ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * (r⁻¹ * r))) • x ∈ U), x ∈ U
neg₇ : ∀ (this : (‖x‖⁻¹ * (‖x‖ * 1)) • x ∈ U), x ∈ U
neg₈ : ∀ (this : (‖x‖⁻¹ * ‖x‖) • x ∈ U), x ∈ U
neg₉ : ∀ (this : HSMul.hSMul (α := ℝ) 1 x ∈ U), x ∈ U
⊢ x ∈ U
have neg₁₀ : ∀ (this : x ∈ U), x ∈ U
Tactic: rwa [hz_def, ← smul_assoc, smul_eq_mul, ← mul_assoc, mul_comm, mul_comm r⁻¹, mul_assoc _ r⁻¹,
    inv_mul_cancel₀ hr₀, mul_one, inv_mul_cancel₀ (by simp_all), one_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.thickening δ s)
have rw : Convex ℝ (s + ball 0 δ)
Tactic: rw [← add_ball_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.cthickening δ s)
have inl : ∀ (hδ : 0 ≤ δ), Convex ℝ (Metric.cthickening δ s)
Tactic: obtain hδ | hδ := le_total 0 δ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
inl : ∀ (hδ : 0 ≤ δ), Convex ℝ (Metric.cthickening δ s)
⊢ Convex ℝ (Metric.cthickening δ s)
have inr : ∀ (hδ : δ ≤ 0), Convex ℝ (Metric.cthickening δ s)
Tactic: obtain hδ | hδ := le_total 0 δ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : 0 ≤ δ
⊢ Convex ℝ (Metric.cthickening δ s)
have inl : Convex.{0, u_1} ℝ (E := E) (⋂ (ε : ℝ), ⋂ (_ : δ < ε), Metric.thickening ε s)
Tactic: rw [cthickening_eq_iInter_thickening hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
δ : ℝ
hδ : δ ≤ 0
⊢ Convex ℝ (Metric.cthickening δ s)
have inr : Convex ℝ (closure s)
Tactic: rw [cthickening_of_nonpos hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set E
x y : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) y
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
have rcases : ∀ (x' : E) (hx' : x' ∈ s) (Hx' : dist x y ≤ dist x' y), ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
Tactic: rcases convexHull_exists_dist_ge hx y with ⟨x', hx', Hx'⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set E
x y : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) y
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
have rcases : ∀ (y' : E) (hy' : y' ∈ t) (Hy' : dist y x' ≤ dist y' x'), ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
Tactic: rcases convexHull_exists_dist_ge hy x' with ⟨y', hy', Hy'⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s t : Set E
x y : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) y
x' : E
hx' : x' ∈ s
Hx' : dist x y ≤ dist x' y
y' : E
hy' : y' ∈ t
Hy' : dist y x' ≤ dist y' x'
⊢ ∃ x' ∈ s, ∃ y' ∈ t, dist x y ≤ dist x' y'
have right : dist x y ≤ dist x' y'
Tactic: use x', hx', y', hy'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
⊢ ediam.{u_1} (X := E) ((convexHull ℝ : (a : Set E) → Set E) s) = ediam s
have refine : ∀ (x : E) (hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x) (y : E)
  (hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y), edist x y ≤ ediam s
Tactic: refine (ediam_le fun x hx y hy => ?_).antisymm (ediam_mono <| subset_convexHull ℝ s)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
⊢ edist x y ≤ ediam s
have rcases : ∀ (x' : E) (hx' : x' ∈ s) (y' : E) (hy' : y' ∈ s) (H : dist x y ≤ dist x' y'), edist x y ≤ ediam s
Tactic: rcases convexHull_exists_dist_ge2 hx hy with ⟨x', hx', y', hy', H⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ edist x y ≤ ediam s
have rw : ENNReal.ofReal (dist x y) ≤ ediam s
Tactic: rw [edist_dist]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x y) ≤ ediam s
have apply : ENNReal.ofReal (dist x' y') ≤ ediam s
Tactic: apply le_trans (ENNReal.ofReal_le_ofReal H)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x : E
hx : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) x
y : E
hy : Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) y
x' : E
hx' : x' ∈ s
y' : E
hy' : y' ∈ s
H : dist x y ≤ dist x' y'
⊢ ENNReal.ofReal (dist x' y') ≤ ediam s
have rw : edist x' y' ≤ ediam s
Tactic: rw [← edist_dist]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
⊢ IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}
have pos : ∀ (hx : x = 0), IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
pos : ∀ (hx : x = 0), IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}
⊢ IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}
have neg : ∀ (hx : ¬x = 0), IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y}
have neg : IsConnected.{u_1} (α := E) {y : E | ∃ (r : ℝ), 0 ≤ r ∧ r • x = y}
Tactic: simp_rw [← exists_nonneg_left_iff_sameRay hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
hx : x ≠ 0
⊢ IsConnected.{u_1} (α := E) {y : E | SameRay ℝ x y ∧ y ≠ 0}
have simp_rw : IsConnected.{u_1} (α := E) {y : E | ∃ (r : ℝ), 0 < r ∧ r • x = y}
Tactic: simp_rw [← exists_pos_left_iff_sameRay_and_ne_zero hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y z : E
hy : y ∈ segment ℝ x z
⊢ ‖y - x‖ ≤ ‖z - x‖
have hy₁ : Membership.mem (γ := Set E) ((fun (θ : ℝ) ↦ x + θ • (z - x)) '' Icc 0 1) y
Tactic: rw [segment_eq_image'] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y z : E
hy : Membership.mem (γ := Set E) ((fun (θ : ℝ) ↦ x + θ • (z - x)) '' Icc 0 1) y
⊢ ‖y - x‖ ≤ ‖z - x‖
have hy₁ : ∃ (x_1 : ℝ), (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ x + x_1 • (z - x) = y
Tactic: simp only [mem_image, mem_Icc] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y z : E
hy : ∃ (x_1 : ℝ), (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ x + x_1 • (z - x) = y
⊢ ‖y - x‖ ≤ ‖z - x‖
have obtain : ∀ (u : ℝ) (hu_nonneg : 0 ≤ u) (hu_le_one : u ≤ 1), ‖x + u • (z - x) - x‖ ≤ ‖z - x‖
Tactic: obtain ⟨u, ⟨hu_nonneg, hu_le_one⟩, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
⊢ ‖x + u • (z - x) - x‖ ≤ ‖z - x‖
have simp : |u| * ‖z - x‖ ≤ ‖z - x‖
Tactic: simp only [add_sub_cancel_left, norm_smul, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
⊢ |u| * ‖z - x‖ ≤ ‖z - x‖
have rw : u * ‖z - x‖ ≤ ‖z - x‖
Tactic: rw [abs_of_nonneg hu_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
| ‖z - x‖
have rw : 1 * ‖z - x‖
Tactic: rw [← one_mul (‖z - x‖)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
⊢ u * ‖z - x‖ ≤ ‖z - x‖
have conv_rhs : u * ‖z - x‖ ≤ 1 * ‖z - x‖
Tactic: conv_rhs => rw [← one_mul (‖z - x‖)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
u : ℝ
hu_nonneg : 0 ≤ u
hu_le_one : u ≤ 1
⊢ u * ‖z - x‖ ≤ 1 * ‖z - x‖
have ha : 0 ≤ ‖z - x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
have obtain : ∀ (p : α → Prop) (hp : ∀ᶠ (i : α) in f, p i) (δ : ℝ) (hδ : δ > 0)
  (hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2),
  ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
Tactic: obtain ⟨p, hp, δ, hδ, hr⟩ := eventually_prod_nhds_iff.mp hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Convex (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
α : Type u_2
f : Filter α
x : E
y z : α → E
r : α → E → Prop
hy : Tendsto y f (𝓝 x)
hz : Tendsto z f (𝓝 x)
hr_1 : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2
p : α → Prop
hp : ∀ᶠ (i : α) in f, p i
δ : ℝ
hδ : δ > 0
hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2
⊢ ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
have rw : ∀ (hy : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (y x_1) x < ε) (hz : ∀ ε > 0, ∀ᶠ (x_1 : α) in f, dist (z x_1) x < ε)
  (hr : ∀ᶠ (p : α × E) in f ×ˢ 𝓝 x, r p.1 p.2) (p : α → Prop) (hp : ∀ᶠ (i : α) in f, p i) (δ : ℝ) (hδ : δ > 0)
  (hr : ∀ ⦃i : α⦄, p i → ∀ ⦃x_1 : E⦄, dist x_1 x < δ → r (i, x_1).1 (i, x_1).2),
  ∀ᶠ (χ : α) in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v
Tactic: rw [Metric.tendsto_nhds] at hy hz
Cleared hypotheses: hy, hz, hr_1, p, hp, δ, hδ, hr