awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
⊢ Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)
have refine : ∀ (ε : ℝ) (hε : 0 < ε), norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε
Tactic: refine norm_le_zero_iff.mp (le_of_forall_gt_imp_ge_of_dense fun ε hε => ?_)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε
have rcases : ∀ (c : 𝕜) (hc : 0 < ‖c‖) (hcε : ‖c‖ < ε),
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε
Tactic: rcases NormedField.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
have rw : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
  ‖c‖ *
    norm.{u_1} (E := 𝕜)
      ((HSMul.hSMul (β := F →ₗ[𝕜] 𝕜) c⁻¹ ((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
Tactic: rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
rw :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ *
      norm.{u_1} (E := 𝕜)
        ((HSMul.hSMul (β := F →ₗ[𝕜] 𝕜) c⁻¹ ((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
have rw₁ : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
  ‖c‖ * ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
Tactic: rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
rw :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ *
      norm.{u_1} (E := 𝕜)
        ((HSMul.hSMul (β := F →ₗ[𝕜] 𝕜) c⁻¹ ((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
rw₁ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
have rw₂ : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
  ‖c‖ * ‖HMul.hMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
Tactic: rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
rw :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ *
      norm.{u_1} (E := 𝕜)
        ((HSMul.hSMul (β := F →ₗ[𝕜] 𝕜) c⁻¹ ((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
rw₁ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
rw₂ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * ‖HMul.hMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
have rw₃ : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
  ‖c‖ * (‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))
Tactic: rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
rw :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ *
      norm.{u_1} (E := 𝕜)
        ((HSMul.hSMul (β := F →ₗ[𝕜] 𝕜) c⁻¹ ((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
rw₁ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
rw₂ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * ‖HMul.hMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
rw₃ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * (‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
have rw₄ : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
  ‖c‖ * (‖c‖⁻¹ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))
Tactic: rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
rw :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ *
      norm.{u_1} (E := 𝕜)
        ((HSMul.hSMul (β := F →ₗ[𝕜] 𝕜) c⁻¹ ((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
rw₁ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * ‖HSMul.hSMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
rw₂ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * ‖HMul.hMul (β := 𝕜) c⁻¹ ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)‖
rw₃ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * (‖c⁻¹‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))
rw₄ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * (‖c‖⁻¹ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
have rw₅ : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
Tactic: rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε * 1
have h₂ : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε
have x₁ : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
  ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
Tactic: calc
    ‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
      rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
    _ ≤ ε * 1 := by gcongr; exact hy _ trivial
    _ = ε := mul_one _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : B.SeparatingRight
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) y
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
x₁ :
  norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) =
    ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜)
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε
have x₂ : ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε * 1
Tactic: calc
    ‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
      rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']
    _ ≤ ε * 1 := by gcongr; exact hy _ trivial
    _ = ε := mul_one _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst_5 : SetLike S E
inst_6 : SMulMemClass S 𝕜 E
m : S
⊢ Eq.{u_3 + 1} (α := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E))
    {y : F | ∀ x ∈ m, Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)}
have h : ∀ (y : F),
  Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y ↔
    Membership.mem (γ := Set F)
      {y : F | ∀ x ∈ m, Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)}
      y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst_5 : SetLike S E
inst_6 : SMulMemClass S 𝕜 E
m : S
y : F
⊢ Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y ↔
    Membership.mem (γ := Set F)
      {y : F | ∀ x ∈ m, Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)}
      y
have h : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y →
  Membership.mem (γ := Set F)
    {y : F | ∀ x ∈ m, Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)} y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst_5 : SetLike S E
inst_6 : SMulMemClass S 𝕜 E
m : S
y : F
h :
  Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y →
    Membership.mem (γ := Set F)
      {y : F | ∀ x ∈ m, Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)}
      y
⊢ Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y ↔
    Membership.mem (γ := Set F)
      {y : F | ∀ x ∈ m, Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)}
      y
have h₁ : Membership.mem (γ := Set F)
    {y : F | ∀ x ∈ m, Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)}
    y →
  Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst_5 : SetLike S E
inst_6 : SMulMemClass S 𝕜 E
m : S
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y
x : E
hx : x ∈ m
⊢ Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)
have h : ∀ (r : 𝕜) (hr : (norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))⁻¹ < ‖r‖),
  Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)
Tactic: obtain ⟨r, hr⟩ := NormedField.exists_lt_norm 𝕜 ‖B x y‖⁻¹
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst_5 : SetLike S E
inst_6 : SMulMemClass S 𝕜 E
m : S
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y
x : E
hx : x ∈ m
r : 𝕜
hr : (norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))⁻¹ < ‖r‖
⊢ Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)
have h : ∀ (hr : Ne.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)),
  ‖r‖ ≤ (norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))⁻¹
Tactic: contrapose! hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst_5 : SetLike S E
inst_6 : SMulMemClass S 𝕜 E
m : S
y : F
hy : Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) y
x : E
hx : x ∈ m
r : 𝕜
hr : Ne.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)
⊢ ‖r‖ ≤ (norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))⁻¹
have h : ‖r‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
Tactic: rw [← one_div, le_div_iff₀ (norm_pos_iff.2 hr)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
S : Type u_4
inst_5 : SetLike S E
inst_6 : SMulMemClass S 𝕜 E
m : S
⊢ polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E) =
    (↑(⨅ x ∈ m, ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜) ((B : (a : E) → F →ₗ[𝕜] 𝕜) x)) : Set F)
have h : ∀ (x : F),
  Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) B (↑m : Set E)) x ↔
    x ∈ (↑(⨅ x ∈ m, ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜) ((B : (a : E) → F →ₗ[𝕜] 𝕜) x)) : Set F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Polar (goal)
Goal:
R : Type u_4
M : Type u_5
inst : SeminormedCommRing R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ LinearMap.SeparatingLeft (M₁ := M →L[R] R) (topDualPairing R M)
have rw : Function.Injective (α := M →L[R] R) (β := M →ₗ[R] R) (⇑(topDualPairing R M) : (a : M →L[R] R) → M →ₗ[R] R)
Tactic: rw [LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : T1Space E
x : E
hx : x ≠ 0
⊢ ∃ (f : StrongDual ℝ E), Ne (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have rcases : ∀ (f : StrongDual ℝ E) (hf : LT.lt (α := ℝ) ((f : (a : E) → ℝ) 0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)),
  ∃ (f : StrongDual ℝ E), Ne (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
Tactic: rcases geometric_hahn_banach_point_point hx.symm with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (hypothesis)
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : AddCommGroup E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : T1Space E
x : E
hx : x ≠ 0
f : StrongDual ℝ E
hf : LT.lt (α := ℝ) ((f : (a : E) → ℝ) 0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∃ (f : StrongDual ℝ E), Ne (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have hf₁ : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
Tactic: simp only [map_zero] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace R
inst_4 : Module R V
inst_5 : SeparatingDual R V
x y : V
h : x ≠ y
⊢ ∃ (f : StrongDual R V), Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) y : R)
have rcases : ∀ (f : StrongDual R V) (hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) (x - y) : R) (0 : R)),
  ∃ (f : StrongDual R V), Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) y : R)
Tactic: rcases exists_ne_zero (R := R) (sub_ne_zero_of_ne h) with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace R
inst_4 : Module R V
inst_5 : SeparatingDual R V
inst_6 : T1Space R
⊢ T1Space V
have apply : ∀ (x y : V) (hxy : x ≠ y), ∃ (U : Set V), IsOpen U ∧ x ∈ U ∧ y ∉ U
Tactic: apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace R
inst_4 : Module R V
inst_5 : SeparatingDual R V
inst_6 : T1Space R
x y : V
hxy : x ≠ y
⊢ ∃ (U : Set V), IsOpen U ∧ x ∈ U ∧ y ∉ U
have rcases : ∀ (f : StrongDual R V) (hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) y : R)),
  ∃ (U : Set V), IsOpen U ∧ x ∈ U ∧ y ∉ U
Tactic: rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace R
inst_4 : Module R V
inst_5 : SeparatingDual R V
inst_6 : T2Space R
⊢ T2Space V
have apply : ∀ {x y : V} (hxy : x ≠ y), ∃ (u : Set V) (v : Set V), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Tactic: apply (t2Space_iff _).2 (fun {x} {y} hxy ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace R
inst_4 : Module R V
inst_5 : SeparatingDual R V
inst_6 : T2Space R
x y : V
hxy : x ≠ y
⊢ ∃ (u : Set V) (v : Set V), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
have rcases : ∀ (f : StrongDual R V) (hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) y : R)),
  ∃ (u : Set V) (v : Set V), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Tactic: rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace R
inst_4 : Module R V
inst_5 : SeparatingDual R V
x : V
h : ∀ (f : StrongDual R V), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)
⊢ x = 0
have by_contra : ∀ (hx : ¬x = 0), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace R
inst_4 : Module R V
inst_5 : SeparatingDual R V
x : V
h : ∀ (f : StrongDual R V), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)
hx : ¬x = 0
⊢ False
have rcases : ∀ (f : StrongDual R V) (hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)), False
Tactic: rcases exists_ne_zero (R := R) hx with ⟨f, hf⟩