awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖
have neg : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) * ‖z‖ / r ≤ c * ‖z‖ / r
Tactic: rw [eq, norm_mul, norm_div, RCLike.norm_coe_norm, RCLike.norm_of_nonneg r_pos.le,
    div_mul_eq_mul_div, div_mul_eq_mul_div, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) * ‖z‖ / r ≤ c * ‖z‖ / r
have apply : 0 ≤ c * ‖z‖
Tactic: apply div_le_div₀ _ _ r_pos rfl.ge
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
apply : 0 ≤ c * ‖z‖
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) * ‖z‖ / r ≤ c * ‖z‖ / r
have apply₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) * ‖z‖ ≤ c * ‖z‖
Tactic: apply div_le_div₀ _ _ r_pos rfl.ge
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
⊢ ‖f‖ ≤ c / r
have hMp : 0 ≤ c / r
Tactic: apply ContinuousLinearMap.opNorm_le_bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
hMp : 0 ≤ c / r
⊢ ‖f‖ ≤ c / r
have hM : ∀ (x : E), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) ≤ c / r * ‖x‖
Tactic: apply ContinuousLinearMap.opNorm_le_bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
⊢ 0 ≤ c / r
have apply : 0 ≤ c
Tactic: apply div_nonneg _ r_pos.le
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
⊢ ∀ (x : E), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) ≤ c / r * ‖x‖
have hM : ∀ (z : E),
  Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) (((↑f : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) ≤ c
Tactic: apply LinearMap.bound_of_ball_bound' r_pos
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝓕 : Type u_3
E : Type u_4
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
inst_5 : FunLike 𝓕 E F
inst_6 : AddMonoidHomClass 𝓕 E F
inst_7 : MulActionHomClass 𝓕 𝕜 E F
f : 𝓕
K : NNReal
h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
x : E
⊢ ‖x‖ ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have inl : norm.{u_4} (E := E) 0 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) 0 : F)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝓕 : Type u_3
E : Type u_4
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
inst_5 : FunLike 𝓕 E F
inst_6 : AddMonoidHomClass 𝓕 E F
inst_7 : MulActionHomClass 𝓕 𝕜 E F
f : 𝓕
K : NNReal
h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
x : E
inl : norm.{u_4} (E := E) 0 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) 0 : F)
⊢ ‖x‖ ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
have inr : ∀ (hx : x ≠ 0), ‖x‖ ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
⊢ norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
have pos : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)),
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
Tactic: by_cases h : lm x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
pos :
  ∀ (h : Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)),
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
⊢ norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
have neg : ∀ (h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)),
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
Tactic: by_cases h : lm x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
have pos : 0 ≤ ‖fr‖ * ‖x‖
Tactic: rw [h, norm_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
have neg : HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜)) 2 ≤
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
Tactic: rw [← mul_le_mul_iff_right₀ (norm_pos_iff.2 h), ← sq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ ‖fr‖ * ‖HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x‖ =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
have rw : ‖fr‖ * (norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) * ‖x‖) =
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
Tactic: rw [norm_smul, norm_conj, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
rw :
  ‖fr‖ * (norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) * ‖x‖) =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
⊢ ‖fr‖ * ‖HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x‖ =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
have rw₁ : ‖fr‖ * (norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * ‖x‖) =
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
Tactic: rw [norm_smul, norm_conj, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
rw :
  ‖fr‖ * (norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) * ‖x‖) =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
rw₁ :
  ‖fr‖ * (norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * ‖x‖) =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
⊢ ‖fr‖ * ‖HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x‖ =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
have rw₂ : norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖) =
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
Tactic: rw [norm_smul, norm_conj, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Extend (goal)
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜)) 2 ≤
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
have fr₁ : ‖fr‖ * ‖HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x‖ =
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
Tactic: calc
    ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) := Module.Dual.norm_extendRCLike_apply_sq fr.toLinearMap x
    _ ≤ ‖fr (conj (lm x : 𝕜) • x)‖ := le_abs_self _
    _ ≤ ‖fr‖ * ‖conj (lm x : 𝕜) • x‖ := le_opNorm _ _
    _ = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) := by rw [norm_smul, norm_conj, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
⊢ ‖t • x‖ = t * ‖x‖
have rw : ‖t‖ * ‖x‖ = t * ‖x‖
Tactic: rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
rw : ‖t‖ * ‖x‖ = t * ‖x‖
⊢ ‖t • x‖ = t * ‖x‖
have rw₁ : |t| * ‖x‖ = t * ‖x‖
Tactic: rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
rw : ‖t‖ * ‖x‖ = t * ‖x‖
rw₁ : |t| * ‖x‖ = t * ‖x‖
⊢ ‖t • x‖ = t * ‖x‖
have rw₂ : t * ‖x‖ = t * ‖x‖
Tactic: rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖
have simp_rw : ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖
Tactic: simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
simp_rw : ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖
have simp_rw₁ : ‖x - (r • x + (1 - r) • y)‖ = ‖(1 - r) • (x - y)‖
Tactic: simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
simp_rw : ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖
simp_rw₁ : ‖x - (r • x + (1 - r) • y)‖ = ‖(1 - r) • (x - y)‖
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖
have simp_rw₂ : ‖x - (r • x + (HSMul.hSMul (α := ℝ) 1 y - r • y))‖ = ‖HSMul.hSMul (α := ℝ) 1 (x - y) - r • (x - y)‖
Tactic: simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
simp_rw : ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖
simp_rw₁ : ‖x - (r • x + (1 - r) • y)‖ = ‖(1 - r) • (x - y)‖
simp_rw₂ : ‖x - (r • x + (HSMul.hSMul (α := ℝ) 1 y - r • y))‖ = ‖HSMul.hSMul (α := ℝ) 1 (x - y) - r • (x - y)‖
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖
have simp_rw₃ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - r • (x - y)‖
Tactic: simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
simp_rw : ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖
simp_rw₁ : ‖x - (r • x + (1 - r) • y)‖ = ‖(1 - r) • (x - y)‖
simp_rw₂ : ‖x - (r • x + (HSMul.hSMul (α := ℝ) 1 y - r • y))‖ = ‖HSMul.hSMul (α := ℝ) 1 (x - y) - r • (x - y)‖
simp_rw₃ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - r • (x - y)‖
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖
have simp_rw₄ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - (r • x - r • y)‖
Tactic: simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
simp_rw : ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖
simp_rw₁ : ‖x - (r • x + (1 - r) • y)‖ = ‖(1 - r) • (x - y)‖
simp_rw₂ : ‖x - (r • x + (HSMul.hSMul (α := ℝ) 1 y - r • y))‖ = ‖HSMul.hSMul (α := ℝ) 1 (x - y) - r • (x - y)‖
simp_rw₃ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - r • (x - y)‖
simp_rw₄ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - (r • x - r • y)‖
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖
have simp_rw₅ : ‖x - r • x - (y - r • y)‖ = ‖x - y - (r • x - r • y)‖
Tactic: simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
simp_rw : ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖
simp_rw₁ : ‖x - (r • x + (1 - r) • y)‖ = ‖(1 - r) • (x - y)‖
simp_rw₂ : ‖x - (r • x + (HSMul.hSMul (α := ℝ) 1 y - r • y))‖ = ‖HSMul.hSMul (α := ℝ) 1 (x - y) - r • (x - y)‖
simp_rw₃ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - r • (x - y)‖
simp_rw₄ : ‖x - (r • x + (y - r • y))‖ = ‖x - y - (r • x - r • y)‖
simp_rw₅ : ‖x - r • x - (y - r • y)‖ = ‖x - y - (r • x - r • y)‖
⊢ dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖
have simp_rw₆ : ‖x - r • x - y + r • y‖ = ‖x - y - r • x + r • y‖
Tactic: simp_rw [dist_eq_norm', ← norm_smul, sub_smul, one_smul, smul_sub, ← sub_sub, ← sub_add,
        sub_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
⊢ ‖1 - r‖ * ‖x - y‖ = (1 - r) * dist y x
have rw : |1 - r| * ‖x - y‖ = (1 - r) * dist y x
Tactic: rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
rw : |1 - r| * ‖x - y‖ = (1 - r) * dist y x
⊢ ‖1 - r‖ * ‖x - y‖ = (1 - r) * dist y x
have rw₁ : (1 - r) * ‖x - y‖ = (1 - r) * dist y x
Tactic: rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
rw : |1 - r| * ‖x - y‖ = (1 - r) * dist y x
rw₁ : (1 - r) * ‖x - y‖ = (1 - r) * dist y x
⊢ ‖1 - r‖ * ‖x - y‖ = (1 - r) * dist y x
have rw₂ : (1 - r) * ‖x - y‖ = (1 - r) * ‖x - y‖
Tactic: rw [Real.norm_eq_abs, abs_eq_self.mpr (sub_nonneg.mpr h.2), dist_eq_norm']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
⊢ (1 - r) * dist y x ≤ HSub.hSub (α := ℝ) 1 0 * dist y x
have hbc : 0 ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
⊢ HSub.hSub (α := ℝ) 1 0 * dist y x = dist y x
have rw : 1 * dist y x = dist y x
Tactic: rw [sub_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
x y : E
h : Membership.mem (γ := Set ℝ) (Icc 0 1) r
rw : 1 * dist y x = dist y x
⊢ HSub.hSub (α := ℝ) 1 0 * dist y x = dist y x
have rw₁ : dist y x = dist y x
Tactic: rw [sub_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) = closedBall x r
have refine : ∀ (y : E) (hy : y ∈ closedBall x r), y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)
Tactic: refine Subset.antisymm closure_ball_subset_closedBall fun y hy => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)
have this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
Tactic: have : ContinuousWithinAt (fun c : ℝ => c • (y - x) + x) (Ico 0 1) 1 := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)
have h : y = HSMul.hSMul (α := ℝ) 1 (y - x) + x
Tactic: convert! this.mem_closure _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
h : y = HSMul.hSMul (α := ℝ) 1 (y - x) + x
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)
have convert_2 : Membership.mem (γ := Set ℝ) (closure (Ico 0 1)) 1
Tactic: convert! this.mem_closure _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
h : y = HSMul.hSMul (α := ℝ) 1 (y - x) + x
convert_2 : Membership.mem (γ := Set ℝ) (closure (Ico 0 1)) 1
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)
have convert_3 : MapsTo (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) (ball x r)
Tactic: convert! this.mem_closure _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
⊢ y = HSMul.hSMul (α := ℝ) 1 (y - x) + x
have h : y = y - x + x
Tactic: rw [one_smul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
h : y = y - x + x
⊢ y = HSMul.hSMul (α := ℝ) 1 (y - x) + x
have h₁ : y = y
Tactic: rw [one_smul, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ (fun (c : ℝ) ↦ c • (y - x) + x) c ∈ ball x r
have convert_3 : ‖y - x‖ * c < r * 1
Tactic: rw [mem_ball, dist_eq_norm, add_sub_cancel_right, norm_smul, Real.norm_eq_abs,
      abs_of_nonneg hc0, mul_comm, ← mul_one r]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.RCLike.Real (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖y - x‖ * c < r * 1
have convert_3 : ∀ (hy : ‖y - x‖ ≤ r) (this : ContinuousWithinAt.{0, u_1} (Y := E) (fun (c : ℝ) ↦ c • (y - x) + x) (Ico 0 1) 1) ⦃c : ℝ⦄
  (hc0 : 0 ≤ c) (hc1 : c < 1), ‖y - x‖ * c < r * 1
Tactic: rw [mem_closedBall, dist_eq_norm] at hy
Cleared hypotheses: hy, this, c, hc0, hc1