awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ Antitone B.polar

Tactic:
B.polar_gc.monotone_l

Premises used: setOf, LinearMap.polar, LinearMap.polar_gc, Antitone, GaloisConnection.monotone_l
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ B.polar ∅ = Set.univ

Tactic:
B.polar_gc.l_bot

Premises used: Set.Mem, setOf, LinearMap.polar, LinearMap.polar_gc, GaloisConnection.l_bot, OrderDual
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
a : E
y : F
hy :
  Membership.mem (γ := Set F)
    {y : F | norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1} y
x : E
hb : Membership.mem (γ := Set E) {a} x
rw : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
rw [Set.mem_singleton_iff.mp hb]

Premises used: Set.mem_singleton_iff, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
a : E
y : F
hy :
  Membership.mem (γ := Set F)
    {y : F | norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1} y
x : E
hb : Membership.mem (γ := Set E) {a} x
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
hy

Premises used: Set.Mem
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
a : E
y : F
hy :
  Membership.mem (γ := Set F)
    {y : F | norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1} y
x : E
hb : Membership.mem (γ := Set E) {a} x
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
exact hy
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
x : E
y : F
⊢ y ∈ B.polar {x} ↔ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
simp only [polar_singleton, Set.mem_setOf_eq]

Premises used: LinearMap.polar_singleton, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
⊢ B.polar {0} = Set.univ

Tactic:
simp only [polar_singleton, map_zero, zero_apply, norm_zero, zero_le_one, Set.setOf_true]

Premises used: LinearMap.zero_apply, LinearMap.polar_singleton, norm_zero, map_zero, zero_le_one, Set.setOf_true
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ B.polar s
rw : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
⊢ norm.{u_1} (E := 𝕜) ((((B.flip : (a : F) → E →ₗ[𝕜] 𝕜) y : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ≤ 1

Tactic:
rw [B.flip_apply]

Premises used: LinearMap.flip_apply
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
hy x hx
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
exact hy x hx
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ B.polar (B.flip.polar (B.polar s)) = B.polar s

Tactic:
(B.polar_antitone (B.subset_bipolar s)).antisymm (subset_bipolar B.flip (B.polar s))

Premises used: LinearMap.subset_bipolar, LinearMap.polar_antitone, LE.le.antisymm, LinearMap.polar, LinearMap.flip
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
h : ∀ (x : F), x ∈ ⋂₀ (B.polar '' {F : Set E | F.Finite ∧ F ⊆ s}) ↔ x ∈ B.polar s
⊢ ⋂₀ (B.polar '' {F : Set E | F.Finite ∧ F ⊆ s}) = B.polar s

Tactic:
ext x
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
h : (∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) ↔ x ∈ B.polar s
⊢ x ∈ ⋂₀ (B.polar '' {F : Set E | F.Finite ∧ F ⊆ s}) ↔ x ∈ B.polar s

Tactic:
simp only [Set.sInter_image, Set.mem_setOf_eq, Set.mem_iInter, and_imp]

Premises used: and_imp, Set.mem_setOf_eq, Set.mem_iInter, Set.sInter_image
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
⊢ (∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) ↔ x ∈ B.polar s

Tactic:
⟨fun hx a ha ↦ ?_, fun hx F _ hF₂ => polar_antitone _ hF₂ hx⟩

Premises used: LinearMap.polar_antitone, Iff.intro
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
h :
  ∀ (hx : ∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) (a : E) (ha : a ∈ s),
    norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) ≤ 1
⊢ (∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i) ↔ x ∈ B.polar s

Tactic:
refine ⟨fun hx a ha ↦ ?_, fun hx F _ hF₂ => polar_antitone _ hF₂ hx⟩
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedCommRing 𝕜
inst_1 : AddCommMonoid E
inst_2 : AddCommMonoid F
inst_3 : Module 𝕜 E
inst_4 : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : F
hx : ∀ (i : Set E), i.Finite → i ⊆ s → x ∈ B.polar i
a : E
ha : a ∈ s
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) x : 𝕜) ≤ 1

Tactic:
simpa [mem_polar_singleton] using hx _ (Set.finite_singleton a) (Set.singleton_subset_iff.mpr ha)

Premises used: Iff.mpr, Set.singleton_subset_iff, LinearMap.mem_polar_singleton, Set.finite_singleton
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
rw :
  Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) 0 ∧
    ∀ (x : F), Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) x → x = 0
⊢ Eq (α := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) {0}

Tactic:
rw [Set.eq_singleton_iff_unique_mem]

Premises used: Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
⊢ Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) 0

Tactic:
simp only [zero_mem_polar]

Premises used: LinearMap.zero_mem_polar
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
refine :
  ∀ (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 : 𝕜)
⊢ Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) 0 ∧
    ∀ (x : F), Membership.mem (γ := Set F) (polar.{u_1, u_2, u_3} (𝕜 := 𝕜) (E := E) B Set.univ) x → x = 0

Tactic:
refine ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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 : 𝕜)

Tactic:
norm_le_zero_iff.mp (le_of_forall_gt_imp_ge_of_dense fun ε hε => ?_)

Premises used: norm_le_zero_iff, Iff.mp, le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
refine :
  ∀ (ε : ℝ) (hε : 0 < ε), norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε
⊢ Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)

Tactic:
refine norm_le_zero_iff.mp (le_of_forall_gt_imp_ge_of_dense fun ε hε => ?_)

Premises used: norm_le_zero_iff, Iff.mp, le_of_forall_gt_imp_ge_of_dense
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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 < ε
rcases :
  ∀ (c : 𝕜) (hc : 0 < ‖c‖) (hcε : ‖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 : 𝕜) ≤ ε

Tactic:
rcases NormedField.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩

Premises used: NormedField.exists_norm_lt
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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 : 𝕜))
rw₅ 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 : 𝕜)
⊢ 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:
rw [B.map_smul, LinearMap.smul_apply, smul_eq_mul, norm_mul, norm_inv,
        mul_inv_cancel_left₀ hc.ne']

Premises used: mul_inv_cancel_left₀, LinearMap.smul_apply, norm_mul, norm_inv, LT.lt.ne', LinearMap.map_smul, smul_eq_mul
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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‖ < ε
h₂ : norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
⊢ ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε * 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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 →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
hy _ trivial

Premises used: trivial
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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 →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
exact hy _ trivial

Premises used: trivial
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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‖ < ε
⊢ ε * 1 = ε

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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 : 𝕜)
x₂ : ‖c‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) (c⁻¹ • x) : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ ε * 1
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) 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 _

Premises used: Inv.inv, HSMul.hSMul, mul_one, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
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
⊢ 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 : 𝕜)}

Tactic:
ext y
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
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
⊢ 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
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
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 : 𝕜)
⊢ 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‖⁻¹

Premises used: Norm.norm, NormedField.exists_lt_norm, Inv.inv, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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‖
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 : 𝕜))⁻¹
⊢ Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)

Tactic:
contrapose! hr
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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 : 𝕜)
h : ‖r‖ * norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1
⊢ ‖r‖ ≤ (norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜))⁻¹

Tactic:
rw [← one_div, le_div_iff₀ (norm_pos_iff.2 hr)]

Premises used: Iff.mpr, norm_pos_iff, one_div, le_div_iff₀
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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 : 𝕜) ≤ 1

Tactic:
simpa using hy _ (SMulMemClass.smul_mem r hx)

Premises used: SMulMemClass.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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)
    {y : F | ∀ x ∈ m, Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) (0 : 𝕜)} y
x : E
hx : x ∈ (↑m : Set E)
⊢ norm.{u_1} (E := 𝕜) ((((B : (a : E) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) : (a : F) → 𝕜) y : 𝕜) ≤ 1

Tactic:
simp [h x hx]
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
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:
simp [polar_subMulAction]

Premises used: LinearMap.polar_subMulAction