awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
rw : Function.Injective (α := M →L[R] R) (β := M →ₗ[R] R) (⇑(topDualPairing R M) : (a : M →L[R] R) → M →ₗ[R] R)
⊢ LinearMap.SeparatingLeft (M₁ := M →L[R] R) (topDualPairing R M)

Tactic:
rw [LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot, LinearMap.separatingLeft_iff_ker_eq_bot
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
⊢ Function.Injective (α := M →L[R] R) (β := M →ₗ[R] R) (⇑(topDualPairing R M) : (a : M →L[R] R) → M →ₗ[R] R)

Tactic:
ContinuousLinearMap.coe_injective

Premises used: ContinuousLinearMap.coe_injective
-- Module: Mathlib.Analysis.LocallyConvex.Polar
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
⊢ Function.Injective (α := M →L[R] R) (β := M →ₗ[R] R) (⇑(topDualPairing R M) : (a : M →L[R] R) → M →ₗ[R] R)

Tactic:
exact ContinuousLinearMap.coe_injective

Premises used: ContinuousLinearMap.coe_injective
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
m : SubMulAction 𝕜 E
⊢ (↑(polarSubmodule 𝕜 m) : Set (StrongDual 𝕜 E)) = polar 𝕜 (↑m : Set E)

Tactic:
rfl

Premises used: setOf, StrongDual.polar, LinearMap.polar, rfl
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
x' : StrongDual 𝕜 E
s : Set E
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) x' ↔
    ∀ z ∈ s, norm.{u_4} (E := 𝕜) ((x' : (a : E) → 𝕜) z : 𝕜) ≤ 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, StrongDual.polar, LinearMap.polar
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
S : Type u_6
inst_4 : SetLike S E
inst_5 : SMulMemClass S 𝕜 E
m : S
⊢ (↑(polarSubmodule 𝕜 m) : Set (StrongDual 𝕜 E)) =
    {y : StrongDual 𝕜 E | ∀ x ∈ m, Eq.{u_4 + 1} (α := 𝕜) ((y : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)}

Tactic:
(topDualPairing 𝕜 E).flip.polar_subMulAction _

Premises used: setOf, LinearMap.polar, topDualPairing, LinearMap.flip, LinearMap.polar_subMulAction
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
S : Type u_6
inst_4 : SetLike S E
inst_5 : SMulMemClass S 𝕜 E
m : S
y : StrongDual 𝕜 E
⊢ Membership.mem (γ := Submodule 𝕜 (StrongDual 𝕜 E)) (polarSubmodule 𝕜 m) y ↔
    ∀ x ∈ m, Eq.{u_4 + 1} (α := 𝕜) ((y : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
propext_iff.mp congr($(polarSubmodule_eq_setOf 𝕜 m) y)

Premises used: StrongDual.polarSubmodule_eq_setOf, id, congrFun, Iff.mp, propext_iff
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
s : Set E
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 s) 0

Tactic:
LinearMap.zero_mem_polar _ s

Premises used: Set.Mem, LinearMap.zero_mem_polar, StrongDual.polar
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
s : Set E
⊢ Set.Nonempty (α := StrongDual 𝕜 E) (polar 𝕜 s)

Tactic:
LinearMap.polar_nonempty _ _

Premises used: StrongDual.polar, LinearMap.polar_nonempty
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 ∅) univ

Tactic:
LinearMap.polar_empty _

Premises used: StrongDual.polar, LinearMap.polar_empty
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
a : E
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 {a}) {x : StrongDual 𝕜 E | norm.{u_4} (E := 𝕜) ((x : (a : E) → 𝕜) a : 𝕜) ≤ 1}

Tactic:
simp only [polar, LinearMap.polar_singleton, LinearMap.flip_apply, topDualPairing_apply]

Premises used: LinearMap.polar_singleton, StrongDual.polar, LinearMap.flip_apply, topDualPairing_apply
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
a : E
y : StrongDual 𝕜 E
⊢ Membership.mem (γ := Set (StrongDual 𝕜 E)) (polar 𝕜 {a}) y ↔ norm.{u_4} (E := 𝕜) ((y : (a : E) → 𝕜) a : 𝕜) ≤ 1

Tactic:
simp only [polar_singleton, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, StrongDual.polar_singleton
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommMonoid E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 {0}) univ

Tactic:
LinearMap.polar_zero _

Premises used: StrongDual.polar, LinearMap.polar_zero
-- Module: Mathlib.Analysis.LocallyConvex.Polar
Goal:
𝕜 : Type u_4
inst : NontriviallyNormedField 𝕜
E : Type u_5
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
⊢ Eq (α := Set (StrongDual 𝕜 E)) (polar 𝕜 univ) {0}

Tactic:
(topDualPairing 𝕜 E).flip.polar_univ
    (LinearMap.flip_separatingRight.mpr (dualPairing_separatingLeft 𝕜 E))

Premises used: Iff.mpr, StrongDual.polar, StrongDual.dualPairing_separatingLeft, LinearMap.flip_separatingRight, topDualPairing, LinearMap.flip, LinearMap.polar_univ
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
rcases :
  ∀ (f : StrongDual ℝ E) (hf : LT.lt (α := ℝ) ((f : (a : E) → ℝ) 0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)),
    ∃ (f : StrongDual ℝ E), Ne (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ ∃ (f : StrongDual ℝ E), Ne (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rcases geometric_hahn_banach_point_point hx.symm with ⟨f, hf⟩

Premises used: geometric_hahn_banach_point_point, Ne.symm
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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 : ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)

Tactic:
simp only [map_zero] at hf

Premises used: map_zero
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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 (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∃ (f : StrongDual ℝ E), Ne (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
⟨f, hf.ne'⟩

Premises used: LT.lt.ne', Exists.intro
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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 (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) x : ℝ)
⊢ ∃ (f : StrongDual ℝ E), Ne (α := ℝ) ((f : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact ⟨f, hf.ne'⟩
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this_1 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : LocallyConvexSpace ℝ E
f : StrongDual 𝕜 E
hf :
  LT.lt (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) x : 𝕜) : ℝ)
    ((RCLike.re : (a : 𝕜) → ℝ) ((f : (a : E) → 𝕜) 0 : 𝕜) : ℝ)
hf' : Eq.{u_2 + 1} (α := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ False

Tactic:
simp [hf'] at hf
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
hx : x ≠ 0
⊢ ∃ (f : StrongDual R V), Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)

Tactic:
exists_ne_zero' x hx

Premises used: SeparatingDual.exists_ne_zero'
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
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)
⊢ ∃ (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⟩

Premises used: SeparatingDual.exists_ne_zero, sub_ne_zero_of_ne
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) (x - y) : R) (0 : R)
⊢ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) y : R)

Tactic:
simpa [sub_ne_zero] using hf

Premises used: sub_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
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:
exact ⟨f, by simpa [sub_ne_zero] using hf⟩
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
apply : ∀ (x y : V) (hxy : x ≠ y), ∃ (U : Set V), IsOpen U ∧ x ∈ U ∧ y ∉ U
⊢ T1Space V

Tactic:
apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)

Premises used: Iff.mpr, t1Space_iff_exists_open
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
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
⊢ ∃ (U : Set V), IsOpen U ∧ x ∈ U ∧ y ∉ U

Tactic:
rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩

Premises used: SeparatingDual.exists_separating_of_ne
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
f : StrongDual R V
hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) ((f : (a : V) → R) y : R)
⊢ y ∉ Set.preimage (β := R) (⇑f : (a : V) → R) (singleton (α := R) ((f : (a : V) → R) y : R))ᶜ

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
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:
exact ⟨f ⁻¹' {f y}ᶜ, isOpen_compl_singleton.preimage f.continuous, hf, by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
apply : ∀ {x y : V} (hxy : x ≠ y), ∃ (u : Set V) (v : Set V), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
⊢ T2Space V

Tactic:
apply (t2Space_iff _).2 (fun {x} {y} hxy ↦ ?_)

Premises used: Iff.mpr, t2Space_iff
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
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
⊢ ∃ (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⟩

Premises used: SeparatingDual.exists_separating_of_ne
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
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:
separated_by_continuous f.continuous hf

Premises used: separated_by_continuous, ContinuousLinearMap.continuous
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
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:
exact separated_by_continuous f.continuous hf

Premises used: separated_by_continuous, ContinuousLinearMap.continuous
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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)
by_contra : ∀ (hx : ¬x = 0), False
⊢ x = 0

Tactic:
by_contra hx
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
rcases : ∀ (f : StrongDual R V) (hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)), False
⊢ False

Tactic:
rcases exists_ne_zero (R := R) hx with ⟨f, hf⟩

Premises used: SeparatingDual.exists_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
f : StrongDual R V
hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)
⊢ False

Tactic:
hf (h f)
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
f : StrongDual R V
hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)
⊢ False

Tactic:
exact hf (h f)
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
⊢ x = 0 → ∀ (g : StrongDual R V), Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) (0 : R)

Tactic:
simp +contextual
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
rw :
  (∀ (g : StrongDual R V), Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) (x - y) : R) (0 : R)) ↔
    ∀ (g : StrongDual R V), Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) ((g : (a : V) → R) y : R)
⊢ x = y ↔ ∀ (g : StrongDual R V), Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) ((g : (a : V) → R) y : R)

Tactic:
rw [← sub_eq_zero, eq_zero_iff_forall_dual_eq_zero (R := R) (x - y)]

Premises used: sub_eq_zero, HSub.hSub, SeparatingDual.eq_zero_iff_forall_dual_eq_zero
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
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
⊢ (∀ (g : StrongDual R V), Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) (x - y) : R) (0 : R)) ↔
    ∀ (g : StrongDual R V), Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) ((g : (a : V) → R) y : R)

Tactic:
simp [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
simp_rw :
  (∀ (x : V), ¬x = 0 → ∃ (f : StrongDual R V), ¬Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)) ↔
    ∀ (a : V),
      Eq (α := (V →L[R] R) →ₗ[R] R)
          ((LinearMap.flip (ContinuousLinearMap.coeLM R) : (a : V) → (V →L[R] R) →ₗ[R] R) a : (V →L[R] R) →ₗ[R] R)
          (0 : (V →L[R] R) →ₗ[R] R) →
        a = 0
⊢ SeparatingDual R V ↔
    Function.Injective (α := V) (β := (V →L[R] R) →ₗ[R] R)
      (⇑(LinearMap.flip (ContinuousLinearMap.coeLM R)) : (a : V) → (V →L[R] R) →ₗ[R] R)

Tactic:
simp_rw [separatingDual_def, Ne, injective_iff_map_eq_zero]

Premises used: Ne, injective_iff_map_eq_zero, separatingDual_def
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
a :
  ∀ (v : V),
    (¬v = 0 → ∃ (f : StrongDual R V), ¬Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)) ↔
      Eq (α := (V →L[R] R) →ₗ[R] R)
          ((LinearMap.flip (ContinuousLinearMap.coeLM R) : (a : V) → (V →L[R] R) →ₗ[R] R) v : (V →L[R] R) →ₗ[R] R)
          (0 : (V →L[R] R) →ₗ[R] R) →
        v = 0
⊢ (∀ (x : V), ¬x = 0 → ∃ (f : StrongDual R V), ¬Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)) ↔
    ∀ (a : V),
      Eq (α := (V →L[R] R) →ₗ[R] R)
          ((LinearMap.flip (ContinuousLinearMap.coeLM R) : (a : V) → (V →L[R] R) →ₗ[R] R) a : (V →L[R] R) →ₗ[R] R)
          (0 : (V →L[R] R) →ₗ[R] R) →
        a = 0

Tactic:
congrm ∀ v, ?_
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
v : V
a :
  (¬∃ (f : StrongDual R V), ¬Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)) → v = 0 ↔
    (∀ (x : V →L[R] R),
        Eq.{u_1 + 1} (α := R)
          ((((LinearMap.flip (ContinuousLinearMap.coeLM R) : (a : V) → (V →L[R] R) →ₗ[R] R) v : (V →L[R] R) →ₗ[R] R) :
                (a : V →L[R] R) → R)
              x :
            R)
          ((0 : (a : V →L[R] R) → R) x : R)) →
      v = 0
⊢ (¬v = 0 → ∃ (f : StrongDual R V), ¬Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)) ↔
    Eq (α := (V →L[R] R) →ₗ[R] R)
        ((LinearMap.flip (ContinuousLinearMap.coeLM R) : (a : V) → (V →L[R] R) →ₗ[R] R) v : (V →L[R] R) →ₗ[R] R)
        (0 : (V →L[R] R) →ₗ[R] R) →
      v = 0

Tactic:
rw [not_imp_comm, LinearMap.ext_iff]

Premises used: not_imp_comm, LinearMap.ext_iff
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
v : V
a :
  (∀ (f : StrongDual R V), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)) → v = 0 ↔
    (∀ (x : V →L[R] R),
        Eq.{u_1 + 1} (α := R)
          ((((LinearMap.flip (ContinuousLinearMap.coeLM R) : (a : V) → (V →L[R] R) →ₗ[R] R) v : (V →L[R] R) →ₗ[R] R) :
                (a : V →L[R] R) → R)
              x :
            R)
          ((0 : (a : V →L[R] R) → R) x : R)) →
      v = 0
⊢ (¬∃ (f : StrongDual R V), ¬Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)) → v = 0 ↔
    (∀ (x : V →L[R] R),
        Eq.{u_1 + 1} (α := R)
          ((((LinearMap.flip (ContinuousLinearMap.coeLM R) : (a : V) → (V →L[R] R) →ₗ[R] R) v : (V →L[R] R) →ₗ[R] R) :
                (a : V →L[R] R) → R)
              x :
            R)
          ((0 : (a : V →L[R] R) → R) x : R)) →
      v = 0

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
v : V
⊢ (∀ (f : StrongDual R V), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)) → v = 0 ↔
    (∀ (x : V →L[R] R),
        Eq.{u_1 + 1} (α := R)
          ((((LinearMap.flip (ContinuousLinearMap.coeLM R) : (a : V) → (V →L[R] R) →ₗ[R] R) v : (V →L[R] R) →ₗ[R] R) :
                (a : V →L[R] R) → R)
              x :
            R)
          ((0 : (a : V →L[R] R) → R) x : R)) →
      v = 0

Tactic:
rfl
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_1
V : Type u_2
inst : Field R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalRing R
inst_5 : Module R V
inst_6 : SeparatingDual R V
W : Type u_3
inst_7 : AddCommGroup W
inst_8 : Module R W
inst_9 : FiniteDimensional R W
f : W →ₗ[R] V
mp :
  Surjective (α := V →L[R] R) (β := Module.Dual R W)
      ((⇑f.dualMap : (a : Module.Dual R V) → Module.Dual R W) ∘ ContinuousLinearMap.toLinearMap) →
    Injective.{u_3 + 1, u_2 + 1} (α := W) (β := V) (⇑f : (a : W) → V)
mpr :
  Injective.{u_3 + 1, u_2 + 1} (α := W) (β := V) (⇑f : (a : W) → V) →
    Surjective (α := V →L[R] R) (β := Module.Dual R W)
      ((⇑f.dualMap : (a : Module.Dual R V) → Module.Dual R W) ∘ ContinuousLinearMap.toLinearMap)
⊢ Surjective (α := V →L[R] R) (β := Module.Dual R W)
      ((⇑f.dualMap : (a : Module.Dual R V) → Module.Dual R W) ∘ ContinuousLinearMap.toLinearMap) ↔
    Injective.{u_3 + 1, u_2 + 1} (α := W) (β := V) (⇑f : (a : W) → V)

Tactic:
constructor