awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
⊢ ∃ (gs : ℕ → WeakDual 𝕜 E → 𝕜),
    (∀ (n : ℕ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (gs n)) ∧
      ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ (n : ℕ), gs n x ≠ gs n y
have h : (∀ (n : ℕ),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n)) ∧
  ∀ ⦃x y : WeakDual 𝕜 E⦄,
    x ≠ y →
      ∃ (n : ℕ),
        Ne.{u_1 + 1} (α := 𝕜) ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n x)
          ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n y)
Tactic: use (fun n φ ↦ φ (denseSeq E n))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
⊢ (∀ (n : ℕ),
      Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n)) ∧
    ∀ ⦃x y : WeakDual 𝕜 E⦄,
      x ≠ y →
        ∃ (n : ℕ),
          Ne.{u_1 + 1} (α := 𝕜) ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n x)
            ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n y)
have h : ∀ (n : ℕ),
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (φ : WeakDual 𝕜 E) ↦
    (φ : (a : E) → 𝕜) (denseSeq E n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
h :
  ∀ (n : ℕ),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (φ : WeakDual 𝕜 E) ↦
      (φ : (a : E) → 𝕜) (denseSeq E n)
⊢ (∀ (n : ℕ),
      Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n)) ∧
    ∀ ⦃x y : WeakDual 𝕜 E⦄,
      x ≠ y →
        ∃ (n : ℕ),
          Ne.{u_1 + 1} (α := 𝕜) ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n x)
            ((fun (n : ℕ) (φ : WeakDual 𝕜 E) ↦ ((φ : (a : E) → 𝕜) (denseSeq E n) : 𝕜)) n y)
have h₁ : ∀ ⦃x y : WeakDual 𝕜 E⦄,
  x ≠ y → ∃ (n : ℕ), Ne.{u_1 + 1} (α := 𝕜) ((x : (a : E) → 𝕜) (denseSeq E n) : 𝕜) ((y : (a : E) → 𝕜) (denseSeq E n) : 𝕜)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
w y : WeakDual 𝕜 E
w_ne_y : w ≠ y
⊢ ∃ (n : ℕ), Ne.{u_1 + 1} (α := 𝕜) ((w : (a : E) → 𝕜) (denseSeq E n) : 𝕜) ((y : (a : E) → 𝕜) (denseSeq E n) : 𝕜)
have h : ∀
  (w_ne_y :
    ∀ (n : ℕ), Eq.{u_1 + 1} (α := 𝕜) ((w : (a : E) → 𝕜) (denseSeq E n) : 𝕜) ((y : (a : E) → 𝕜) (denseSeq E n) : 𝕜)),
  w = y
Tactic: contrapose! w_ne_y
Cleared hypotheses: w_ne_y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
K : Set (WeakDual 𝕜 E)
K_cpt : IsCompact K
⊢ MetrizableSpace (↑K : Type (max u_1 u_3))
have this : CompactSpace (↑K : Type (max u_1 u_3))
Tactic: have : CompactSpace K := isCompact_iff_compactSpace.mp K_cpt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
K : Set (WeakDual 𝕜 E)
K_cpt : IsCompact K
this : CompactSpace (↑K : Type (max u_1 u_3))
⊢ MetrizableSpace (↑K : Type (max u_1 u_3))
have obtain : ∀ (gs : ℕ → WeakDual 𝕜 E → 𝕜)
  (gs_cont : ∀ (n : ℕ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (gs n))
  (gs_sep : ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ (n : ℕ), gs n x ≠ gs n y), MetrizableSpace (↑K : Type (max u_1 u_3))
Tactic: obtain ⟨gs, gs_cont, gs_sep⟩ := exists_countable_separating 𝕜 E
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
⊢ IsSeqCompact s
have b_isCompact' : CompactSpace (↑s : Type (max u_1 u_3))
Tactic: have b_isCompact' : CompactSpace s :=
    isCompact_iff_compactSpace.mp <| isCompact_of_bounded_of_closed hb hc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
b_isCompact' : CompactSpace (↑s : Type (max u_1 u_3))
⊢ IsSeqCompact s
have b_isMetrizable : MetrizableSpace (↑s : Type (max u_1 u_3))
Tactic: have b_isMetrizable : TopologicalSpace.MetrizableSpace s :=
    metrizable_of_isCompact 𝕜 E s <| isCompact_of_bounded_of_closed hb hc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.WeakDual (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeparableSpace E
inst_4 : ProperSpace 𝕜
s : Set (WeakDual 𝕜 E)
hb : Bornology.IsBounded s
hc : IsClosed s
b_isCompact' : CompactSpace (↑s : Type (max u_1 u_3))
b_isMetrizable : MetrizableSpace (↑s : Type (max u_1 u_3))
⊢ IsSeqCompact s
have seq_cont_phi : SeqContinuous (Y := WeakDual 𝕜 E) fun (φ : (↑s : Type (max u_1 u_3))) ↦ (↑φ : WeakDual 𝕜 E)
Tactic: have seq_cont_phi : SeqContinuous (fun φ : s ↦ (φ : WeakDual 𝕜 E)) :=
    continuous_iff_seqContinuous.mp continuous_subtype_val
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
x y : β
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y
have simp_rw : ‖s • x - s • y‖ = ‖s‖ * ‖x - y‖
Tactic: simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : SeminormedRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
x y : β
simp_rw : ‖s • x - s • y‖ = ‖s‖ * ‖x - y‖
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y
have simp_rw₁ : ‖s • x - s • y‖ = ‖s • (x - y)‖
Tactic: simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
have pos : ∀ (h : r = 0), ‖r • x‖ = ‖r‖ * ‖x‖
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
pos : ∀ (h : r = 0), ‖r • x‖ = ‖r‖ * ‖x‖
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
have neg : ∀ (h : ¬r = 0), ‖r • x‖ = ‖r‖ * ‖x‖
Tactic: by_cases h : r = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
have neg : ‖r‖ * ‖x‖ ≤ ‖r • x‖
Tactic: refine le_antisymm (norm_smul_le r x) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖
have rw : ‖r‖ * ‖x‖ = ‖r‖ * ‖x‖
Tactic: rw [inv_smul_smul₀ h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)
have hbc : ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
have rw : ‖r‖ * (‖r‖⁻¹ * ‖r • x‖) = ‖r • x‖
Tactic: rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
rw : ‖r‖ * (‖r‖⁻¹ * ‖r • x‖) = ‖r • x‖
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
have rw₁ : ‖r‖ * ‖r‖⁻¹ * ‖r • x‖ = ‖r • x‖
Tactic: rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
rw : ‖r‖ * (‖r‖⁻¹ * ‖r • x‖) = ‖r • x‖
rw₁ : ‖r‖ * ‖r‖⁻¹ * ‖r • x‖ = ‖r • x‖
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
have rw₂ : 1 * ‖r • x‖ = ‖r • x‖
Tactic: rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
rw : ‖r‖ * (‖r‖⁻¹ * ‖r • x‖) = ‖r • x‖
rw₁ : ‖r‖ * ‖r‖⁻¹ * ‖r • x‖ = ‖r • x‖
rw₂ : 1 * ‖r • x‖ = ‖r • x‖
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
have rw₃ : ‖r • x‖ = ‖r • x‖
Tactic: rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖
have r₁ : ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖
Tactic: calc
      ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
      _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
      _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
r₁ : ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖
have r₂ : ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)
Tactic: calc
      ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
      _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
      _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddGroup β
inst_2 : MulActionWithZero α β
inst_3 : IsBoundedSMul α β
r : α
x : β
h : ¬r = 0
r₁ : ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖
r₂ : ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖
have r₃ : ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
Tactic: calc
      ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
      _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
      _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel₀ (mt norm_eq_zero.1 h), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
⊢ (fun (x : β) ↦ s • x) '' ball x ε = ball (s • x) (‖s‖ * ε)
have h : ∀ (p : β), Membership.mem (γ := Set β) ((fun (x : β) ↦ s • x) '' ball x ε) p ↔ p ∈ ball (s • x) (‖s‖ * ε)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p) ↔ dist p (s • x) < ‖s‖ * ε
have h : (∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p) → dist p (s • x) < ‖s‖ * ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : (∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p) → dist p (s • x) < ‖s‖ * ε
⊢ (∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p) ↔ dist p (s • x) < ‖s‖ * ε
have h₁ : dist p (s • x) < ‖s‖ * ε → ∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) < ‖s‖ * ε → ∃ (x_1 : β), dist x_1 x < ε ∧ s • x_1 = p
have h : ∀ (h : dist p (s • x) < ‖s‖ * ε), dist (s⁻¹ • p) x < ε
Tactic: refine fun h ↦ ⟨s⁻¹ • p, ?_, by simp [smul_smul, hs]⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ dist (s⁻¹ • p) x < ε
have h₁ : ‖s‖ * dist (s⁻¹ • p) x < ‖s‖ * ε
Tactic: refine lt_of_mul_lt_mul_of_nonneg_left ?_ (norm_nonneg s)
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) < ‖s‖ * ε
⊢ ‖s‖ * dist (s⁻¹ • p) x < ‖s‖ * ε
have h₁ : dist (s • s⁻¹ • p) (s • x) < ‖s‖ * ε
Tactic: rw [← dist_smul₀]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
⊢ (fun (x : β) ↦ s • x) '' closedBall x ε = closedBall (s • x) (‖s‖ * ε)
have h : ∀ (p : β), Membership.mem (γ := Set β) ((fun (x : β) ↦ s • x) '' closedBall x ε) p ↔ p ∈ closedBall (s • x) (‖s‖ * ε)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ (∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p) ↔ dist p (s • x) ≤ ‖s‖ * ε
have h : (∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p) → dist p (s • x) ≤ ‖s‖ * ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : (∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p) → dist p (s • x) ≤ ‖s‖ * ε
⊢ (∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p) ↔ dist p (s • x) ≤ ‖s‖ * ε
have h₁ : dist p (s • x) ≤ ‖s‖ * ε → ∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) ≤ ‖s‖ * ε → ∃ (x_1 : β), dist x_1 x ≤ ε ∧ s • x_1 = p
have h : ∀ (h : dist p (s • x) ≤ ‖s‖ * ε), dist (s⁻¹ • p) x ≤ ε
Tactic: refine fun h ↦ ⟨s⁻¹ • p, ?_, by simp [smul_smul, hs]⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ dist (s⁻¹ • p) x ≤ ε
have h₁ : ‖s‖ * dist (s⁻¹ • p) x ≤ ‖s‖ * ε
Tactic: refine le_of_mul_le_mul_of_pos_left ?_ (norm_pos_iff.mpr hs)
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
h : dist p (s • x) ≤ ‖s‖ * ε
⊢ ‖s‖ * dist (s⁻¹ • p) x ≤ ‖s‖ * ε
have h₁ : dist (s • s⁻¹ • p) (s • x) ≤ ‖s‖ * ε
Tactic: rw [← dist_smul₀]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
⊢ (fun (x : β) ↦ s • x) '' sphere x ε = sphere (s • x) (‖s‖ * ε)
have simp_rw : (fun (x : β) ↦ s • x) '' (closedBall x ε \ ball x ε) = closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
Tactic: simp_rw [← Metric.closedBall_diff_ball, Set.image_diff (smul_right_injective β hs),
    smul_image_ball hs, smul_image_closedBall hs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
simp_rw : (fun (x : β) ↦ s • x) '' (closedBall x ε \ ball x ε) = closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
⊢ (fun (x : β) ↦ s • x) '' sphere x ε = sphere (s • x) (‖s‖ * ε)
have simp_rw₁ : (fun (x : β) ↦ s • x) '' closedBall x ε \ (fun (x : β) ↦ s • x) '' ball x ε =
  closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
Tactic: simp_rw [← Metric.closedBall_diff_ball, Set.image_diff (smul_right_injective β hs),
    smul_image_ball hs, smul_image_closedBall hs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.MulAction (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedDivisionRing α
inst_1 : SeminormedAddCommGroup β
inst_2 : Module α β
inst_3 : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
simp_rw : (fun (x : β) ↦ s • x) '' (closedBall x ε \ ball x ε) = closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
simp_rw₁ :
  (fun (x : β) ↦ s • x) '' closedBall x ε \ (fun (x : β) ↦ s • x) '' ball x ε =
    closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
⊢ (fun (x : β) ↦ s • x) '' sphere x ε = sphere (s • x) (‖s‖ * ε)
have simp_rw₂ : (fun (x : β) ↦ s • x) '' closedBall x ε \ ball (s • x) (‖s‖ * ε) = closedBall (s • x) (‖s‖ * ε) \ ball (s • x) (‖s‖ * ε)
Tactic: simp_rw [← Metric.closedBall_diff_ball, Set.image_diff (smul_right_injective β hs),
    smul_image_ball hs, smul_image_closedBall hs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ Eq.{u_4 + 1} (α := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    Set.univ
have refine : ∀ (y : F),
  Membership.mem (γ := Set F) Set.univ y →
    Membership.mem (γ := Set F)
      (⋃ (n : ℕ),
        closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
          (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
      y
Tactic: refine Subset.antisymm (subset_univ _) fun y _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
y : F
h : Membership.mem (γ := Set F) Set.univ y
⊢ Membership.mem (γ := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    y
have rcases : ∀ (x : E) (hx : (f : (a : E) → F) x = y),
  Membership.mem (γ := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    y
Tactic: rcases surj y with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
y : F
h : Membership.mem (γ := Set F) Set.univ y
x : E
hx : (f : (a : E) → F) x = y
⊢ Membership.mem (γ := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    y
have rcases : ∀ (n : ℕ) (hn : ‖x‖ < (↑n : ℝ)),
  Membership.mem (γ := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    y
Tactic: rcases exists_nat_gt ‖x‖ with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Banach (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomIsometric σ
inst_8 : RingHomIsometric σ'
inst_9 : CompleteSpace F
surj : Surjective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
y : F
h : Membership.mem (γ := Set F) Set.univ y
x : E
hx : (f : (a : E) → F) x = y
n : ℕ
hn : ‖x‖ < (↑n : ℝ)
⊢ Membership.mem (γ := Set F)
    (⋃ (n : ℕ),
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
        (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))))
    y
have refine : Membership.mem (γ := Set F) (Set.image.{u_3, u_4} (α := E) (⇑f : (a : E) → F) (ball 0 (↑n : ℝ))) y
Tactic: refine mem_iUnion.2 ⟨n, subset_closure ?_⟩