awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hf :
  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:
LinearMap.dualMap_surjective_iff.mp hf.of_comp

Premises used: Function.Surjective.of_comp, Iff.mp, LinearMap.dualMap_surjective_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
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
hf :
  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:
exact LinearMap.dualMap_surjective_iff.mp hf.of_comp

Premises used: Function.Surjective.of_comp, Iff.mp, LinearMap.dualMap_surjective_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
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
hf : Injective.{u_3 + 1, u_2 + 1} (α := W) (β := V) (⇑f : (a : W) → V)
⊢ Injective (α := W) (β := (V →L[R] R) →ₗ[R] R)
    (comp (β := V) (⇑(LinearMap.flip (ContinuousLinearMap.coeLM R)) : (a : V) → (V →L[R] R) →ₗ[R] R) (⇑f : (a : W) → V))

Tactic:
have := (separatingDual_iff_injective.mp ‹_›).comp hf
-- 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
hf : Injective.{u_3 + 1, u_2 + 1} (α := W) (β := V) (⇑f : (a : W) → V)
this :
  Injective (α := W) (β := (V →L[R] R) →ₗ[R] R)
    (comp (β := V) (⇑(LinearMap.flip (ContinuousLinearMap.coeLM R)) : (a : V) → (V →L[R] R) →ₗ[R] R) (⇑f : (a : W) → V))
⊢ Injective (α := W) (β := (V →L[R] R) →ₗ[R] R)
    (⇑(LinearMap.flip (ContinuousLinearMap.coeLM R) ∘ₗ f) : (a : W) → (V →L[R] R) →ₗ[R] R)

Tactic:
rw [← LinearMap.coe_comp] at this

Premises used: LinearMap.coe_comp
-- 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
hf : Injective.{u_3 + 1, u_2 + 1} (α := W) (β := V) (⇑f : (a : W) → V)
this :
  Injective (α := W) (β := (V →L[R] R) →ₗ[R] R)
    (⇑(LinearMap.flip (ContinuousLinearMap.coeLM R) ∘ₗ f) : (a : W) → (V →L[R] R) →ₗ[R] R)
⊢ Surjective (α := V →L[R] R) (β := Module.Dual R W)
    ((⇑f.dualMap : (a : Module.Dual R V) → Module.Dual R W) ∘ ContinuousLinearMap.toLinearMap)

Tactic:
LinearMap.flip_surjective_iff₁.mpr this

Premises used: Iff.mpr, LinearMap.flip_surjective_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
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
hf : Injective.{u_3 + 1, u_2 + 1} (α := W) (β := V) (⇑f : (a : W) → V)
this :
  Injective (α := W) (β := (V →L[R] R) →ₗ[R] R)
    (⇑(LinearMap.flip (ContinuousLinearMap.coeLM R) ∘ₗ f) : (a : W) → (V →L[R] R) →ₗ[R] R)
⊢ Surjective (α := V →L[R] R) (β := Module.Dual R W)
    ((⇑f.dualMap : (a : Module.Dual R V) → Module.Dual R W) ∘ ContinuousLinearMap.toLinearMap)

Tactic:
exact LinearMap.flip_surjective_iff₁.mpr this

Premises used: Iff.mpr, LinearMap.flip_surjective_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
inst_6 : SeparatingDual R V
W : Type u_3
inst_7 : AddCommGroup W
inst_8 : TopologicalSpace W
inst_9 : Module R W
inst_10 : Nontrivial W
inst_11 : ContinuousSMul R W
inst_12 : Nontrivial V
obtain : ∀ (v : V) (hv : v ≠ 0), Nontrivial (V →L[R] W)
⊢ Nontrivial (V →L[R] W)

Tactic:
obtain ⟨v, hv⟩ := exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- 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 : TopologicalSpace W
inst_9 : Module R W
inst_10 : Nontrivial W
inst_11 : ContinuousSMul R W
inst_12 : Nontrivial V
v : V
hv : v ≠ 0
obtain : ∀ (w : W) (hw : w ≠ 0), Nontrivial (V →L[R] W)
⊢ Nontrivial (V →L[R] W)

Tactic:
obtain ⟨w, hw⟩ := exists_ne (0 : W)

Premises used: exists_ne, OfNat.ofNat
-- 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 : TopologicalSpace W
inst_9 : Module R W
inst_10 : Nontrivial W
inst_11 : ContinuousSMul R W
inst_12 : Nontrivial V
v : V
hv : v ≠ 0
w : W
hw : w ≠ 0
obtain : ∀ (ψ : StrongDual R V) (hψ : Ne.{u_1 + 1} (α := R) ((ψ : (a : V) → R) v : R) (0 : R)), Nontrivial (V →L[R] W)
⊢ Nontrivial (V →L[R] W)

Tactic:
obtain ⟨ψ, hψ⟩ := exists_ne_zero (R := R) hv

Premises used: SeparatingDual.exists_ne_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
inst_6 : SeparatingDual R V
W : Type u_3
inst_7 : AddCommGroup W
inst_8 : TopologicalSpace W
inst_9 : Module R W
inst_10 : Nontrivial W
inst_11 : ContinuousSMul R W
inst_12 : Nontrivial V
v : V
hv : v ≠ 0
w : W
hw : w ≠ 0
ψ : StrongDual R V
hψ : Ne.{u_1 + 1} (α := R) ((ψ : (a : V) → R) v : R) (0 : R)
⊢ Ne.{u_3 + 1} (α := W) ((smulRight ψ w : (a : V) → W) v : W) ((0 : (a : V) → W) v : W)

Tactic:
simp_all
-- 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 : TopologicalSpace W
inst_9 : Module R W
inst_10 : Nontrivial W
inst_11 : ContinuousSMul R W
inst_12 : Nontrivial V
v : V
hv : v ≠ 0
w : W
hw : w ≠ 0
ψ : StrongDual R V
hψ : Ne.{u_1 + 1} (α := R) ((ψ : (a : V) → R) v : R) (0 : R)
⊢ Nontrivial (V →L[R] W)

Tactic:
exact ⟨ψ.smulRight w, 0, DFunLike.ne_iff.mpr ⟨v, by simp_all⟩⟩
-- 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
x : V
hx : x ≠ 0
rcases :
  ∀ (f : StrongDual R V) (hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)),
    ∃ (f : StrongDual R V), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R)
⊢ ∃ (f : StrongDual R V), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R)

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 : 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
x : V
hx : x ≠ 0
f : StrongDual R V
hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)
⊢ ∃ (f : StrongDual R V), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R)

Tactic:
⟨(f x)⁻¹ • f, inv_mul_cancel₀ hf⟩

Premises used: Inv.inv, Exists.intro, HSMul.hSMul, DFunLike.coe, inv_mul_cancel₀
-- 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
x : V
hx : x ≠ 0
f : StrongDual R V
hf : Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (0 : R)
⊢ ∃ (f : StrongDual R V), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R)

Tactic:
exact ⟨(f x)⁻¹ • f, inv_mul_cancel₀ hf⟩
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ (u : StrongDual R V), Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)

Tactic:
exists_eq_one hx

Premises used: SeparatingDual.exists_eq_one
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
obtain :
  ∀ (u : StrongDual R V) (ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)),
    ∃ (f : StrongDual R V),
      Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)
⊢ ∃ (f : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)

Tactic:
obtain ⟨u, ux⟩ : ∃ u : StrongDual R V, u x = 1 := exists_eq_one hx

Premises used: SeparatingDual.exists_eq_one, StrongDual
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
inl :
  ∀ (uy : Ne.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)),
    ∃ (f : StrongDual R V),
      Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)
inr :
  ∀ (uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)),
    ∃ (f : StrongDual R V),
      Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)
⊢ ∃ (f : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)

Tactic:
rcases ne_or_eq (u y) 0 with uy | uy

Premises used: ne_or_eq, OfNat.ofNat, DFunLike.coe
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Ne.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
⊢ ∃ (f : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)

Tactic:
⟨u, ux, uy⟩

Premises used: And.intro, Exists.intro
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Ne.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
⊢ ∃ (f : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)

Tactic:
exact ⟨u, ux, uy⟩
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
⊢ ∃ (v : StrongDual R V), Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) y : R) (1 : R)

Tactic:
exists_eq_one hy

Premises used: SeparatingDual.exists_eq_one
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
inr :
  ∀ (v : StrongDual R V) (vy : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) y : R) (1 : R)),
    ∃ (f : StrongDual R V),
      Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)
⊢ ∃ (f : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)

Tactic:
obtain ⟨v, vy⟩ : ∃ v : StrongDual R V, v y = 1 := exists_eq_one hy

Premises used: SeparatingDual.exists_eq_one, StrongDual
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
v : StrongDual R V
vy : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) y : R) (1 : R)
inr :
  ∀ (vx : Ne.{u_1 + 1} (α := R) ((v : (a : V) → R) x : R) (0 : R)),
    ∃ (f : StrongDual R V),
      Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)
inr₁ :
  ∀ (vx : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) x : R) (0 : R)),
    ∃ (f : StrongDual R V),
      Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)
⊢ ∃ (f : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)

Tactic:
rcases ne_or_eq (v x) 0 with vx | vx

Premises used: ne_or_eq, OfNat.ofNat, DFunLike.coe
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
v : StrongDual R V
vy : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) y : R) (1 : R)
vx : Ne.{u_1 + 1} (α := R) ((v : (a : V) → R) x : R) (0 : R)
⊢ HMul.hMul (α := R) (β := R) (((v : (a : V) → R) x)⁻¹ : R) ((v : (a : V) → R) y : R) ≠ 0

Tactic:
simp [vx, vy]
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
v : StrongDual R V
vy : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) y : R) (1 : R)
vx : Ne.{u_1 + 1} (α := R) ((v : (a : V) → R) x : R) (0 : R)
⊢ ∃ (f : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)

Tactic:
exact ⟨(v x)⁻¹ • v, inv_mul_cancel₀ vx, show (v x)⁻¹ * v y ≠ 0 by simp [vx, vy]⟩
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
v : StrongDual R V
vy : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) y : R) (1 : R)
vx : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) x : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((u + v : (a : V) → R) x : R) (1 : R)

Tactic:
simp [ux, vx]
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
v : StrongDual R V
vy : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) y : R) (1 : R)
vx : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) x : R) (0 : R)
⊢ Ne.{u_1 + 1} (α := R) ((u + v : (a : V) → R) y : R) (0 : R)

Tactic:
simp [uy, vy]
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) x : R) (1 : R)
uy : Eq.{u_1 + 1} (α := R) ((u : (a : V) → R) y : R) (0 : R)
v : StrongDual R V
vy : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) y : R) (1 : R)
vx : Eq.{u_1 + 1} (α := R) ((v : (a : V) → R) x : R) (0 : R)
⊢ ∃ (f : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((f : (a : V) → R) y : R) (0 : R)

Tactic:
exact ⟨u + v, by simp [ux, vx], by simp [uy, vy]⟩
-- 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
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
S : Type u_3
inst_9 : CommSemiring S
inst_10 : Module S V
inst_11 : SMulCommClass R S V
inst_12 : Algebra S R
inst_13 : IsScalarTower S R V
inst_14 : ContinuousConstSMul S V
inst_15 : Algebra.IsCentral S R
f : V →L[R] V
hf : Membership.mem (γ := Subalgebra S (V →L[R] V)) (Subalgebra.center S (V →L[R] V)) f
this :
  ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
w : R
y : S
h : (AlgHom.toRingHom (Algebra.ofId S R) : (a : S) → R) y = w
right : f = HSMul.hSMul (β := V →L[R] V) w (ContinuousLinearMap.id R V)
⊢ (AlgHom.toRingHom (Algebra.ofId S (V →L[R] V)) : (a : S) → V →L[R] V) y = f

Tactic:
aesop
-- 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
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
S : Type u_3
inst_9 : CommSemiring S
inst_10 : Module S V
inst_11 : SMulCommClass R S V
inst_12 : Algebra S R
inst_13 : IsScalarTower S R V
inst_14 : ContinuousConstSMul S V
inst_15 : Algebra.IsCentral S R
f : V →L[R] V
hf : Membership.mem (γ := Subalgebra S (V →L[R] V)) (Subalgebra.center S (V →L[R] V)) f
suffices :
  ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
⊢ Membership.mem (γ := Subalgebra S (V →L[R] V)) ⊥ f

Tactic:
suffices ∃ α ∈ Subalgebra.center S R, f = α • .id R V from
      have ⟨_, ⟨y, _⟩, _⟩ := Algebra.IsCentral.center_eq_bot S R ▸ this
      ⟨y, by aesop⟩
-- 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
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
S : Type u_3
inst_9 : CommSemiring S
inst_10 : Module S V
inst_11 : SMulCommClass R S V
inst_12 : Algebra S R
inst_13 : IsScalarTower S R V
inst_14 : ContinuousConstSMul S V
inst_15 : Algebra.IsCentral S R
f : V →L[R] V
hf : Membership.mem (γ := Subalgebra S (V →L[R] V)) (Subalgebra.center S (V →L[R] V)) f
⊢ Nontrivial V

Tactic:
nontriviality 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
inst_6 : SeparatingDual R V
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
S : Type u_3
inst_9 : CommSemiring S
inst_10 : Module S V
inst_11 : SMulCommClass R S V
inst_12 : Algebra S R
inst_13 : IsScalarTower S R V
inst_14 : ContinuousConstSMul S V
inst_15 : Algebra.IsCentral S R
f : V →L[R] V
hf : Membership.mem (γ := Subalgebra S (V →L[R] V)) (Subalgebra.center S (V →L[R] V)) f
h : Nontrivial V
obtain :
  ∀ (x : V) (hx : x ≠ 0),
    ∃ (α : R),
      Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
        f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
⊢ ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- 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
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
S : Type u_3
inst_9 : CommSemiring S
inst_10 : Module S V
inst_11 : SMulCommClass R S V
inst_12 : Algebra S R
inst_13 : IsScalarTower S R V
inst_14 : ContinuousConstSMul S V
inst_15 : Algebra.IsCentral S R
f : V →L[R] V
hf : Membership.mem (γ := Subalgebra S (V →L[R] V)) (Subalgebra.center S (V →L[R] V)) f
h : Nontrivial V
x : V
hx : x ≠ 0
obtain :
  ∀ (g : StrongDual R V) (hg : Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) (1 : R)),
    ∃ (α : R),
      Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
        f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
⊢ ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)

Tactic:
obtain ⟨g, hg⟩ := exists_eq_one (R := R) hx

Premises used: SeparatingDual.exists_eq_one