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
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
g : StrongDual R V
hg : Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) (1 : R)
y : V
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : V) → R) ((f : (a : V) → V) x : V) : R) y = (f : (a : V) → V) y

Tactic:
simpa [hg] using congr($(Subalgebra.mem_center_iff.mp hf (g.smulRight y)) x)
-- 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
g : StrongDual R V
hg : Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) (1 : R)
⊢ ∀ (y : V),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : V) → R) ((f : (a : V) → V) x : V) : R) y = (f : (a : V) → V) y

Tactic:
have (y : V) := by simpa [hg] using congr($(Subalgebra.mem_center_iff.mp hf (g.smulRight y)) x)
-- 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
g : StrongDual R V
hg : Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) (1 : R)
this :
  ∀ (y : V),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : V) → R) ((f : (a : V) → V) x : V) : R) y = (f : (a : V) → V) y
⊢ Membership.mem (α := R) (γ := Subalgebra S R) (Subalgebra.center S R)
      ((g : (a : V) → R) ((f : (a : V) → V) x : V) : R) ∧
    f =
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →L[R] V) ((g : (a : V) → R) ((f : (a : V) → V) x : V) : R)
        (ContinuousLinearMap.id R V)

Tactic:
simp [this, ContinuousLinearMap.ext_iff]

Premises used: ContinuousLinearMap.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
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
g : StrongDual R V
hg : Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) (1 : R)
this :
  ∀ (y : V),
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((g : (a : V) → R) ((f : (a : V) → V) x : V) : R) y = (f : (a : V) → V) y
⊢ ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)

Tactic:
exact ⟨g (f x), by simp [this, ContinuousLinearMap.ext_iff]⟩
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
rw :
  Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) g.conjContinuousAlgEquiv
    f.conjContinuousAlgEquiv
| Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) f.conjContinuousAlgEquiv
    g.conjContinuousAlgEquiv

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
conv_lhs :
  Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) g.conjContinuousAlgEquiv
      f.conjContinuousAlgEquiv ↔
    ∃ (α : Rˣ), f = α • g
⊢ Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) f.conjContinuousAlgEquiv
      g.conjContinuousAlgEquiv ↔
    ∃ (α : Rˣ), f = α • g

Tactic:
conv_lhs => rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
simp_rw :
  (∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)) ↔
    ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
⊢ Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) g.conjContinuousAlgEquiv
      f.conjContinuousAlgEquiv ↔
    ∃ (α : Rˣ), f = α • g

Tactic:
simp_rw [ContinuousAlgEquiv.ext_iff, funext_iff, conjContinuousAlgEquiv_apply,
    ← eq_toContinuousLinearMap_symm_comp, ← ContinuousLinearMap.comp_assoc,
    eq_comp_toContinuousLinearMap_symm, ContinuousLinearMap.comp_assoc,
    ← ContinuousLinearMap.comp_assoc _ f.toContinuousLinearMap, comp_coe, ← mul_def,
    ← Subalgebra.mem_center_iff (R := R), Algebra.IsCentral.center_eq_bot, ← comp_coe,
    Algebra.mem_bot, Set.mem_range, Algebra.algebraMap_eq_smul_one, ContinuousLinearEquiv.ext_iff]

Premises used: Set.mem_range, Subalgebra.mem_center_iff, ContinuousLinearEquiv.ext_iff, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, Algebra.mem_bot, funext_iff, ContinuousAlgEquiv.ext_iff, ContinuousLinearEquiv.eq_toContinuousLinearMap_symm_comp, ContinuousLinearEquiv.comp_coe, ContinuousLinearEquiv.eq_comp_toContinuousLinearMap_symm, Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.comp_assoc, Algebra.IsCentral.center_eq_bot, ContinuousLinearMap.mul_def, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
y : Rˣ
h : Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(y • g) : (a : V) → W)
h₁ :
  ∀ (x : V),
    Eq (α := V) ((HSMul.hSMul (β := V →L[R] V) (↑y : R) 1 : (a : V) → V) x : V)
      (((↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W) : (a : V) → V) x : V)
⊢ HSMul.hSMul (β := V →L[R] V) (↑y : R) 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)

Tactic:
ext
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
y : Rˣ
h : Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(y • g) : (a : V) → W)
x : V
⊢ Eq (α := V) ((HSMul.hSMul (β := V →L[R] V) (↑y : R) 1 : (a : V) → V) x : V)
    (((↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W) : (a : V) → V) x : V)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
refine :
  (∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)) →
    ∀ (y : R) (h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)),
      ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
⊢ (∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)) ↔
    ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)

Tactic:
refine ⟨fun ⟨y, h⟩ ↦ ?_, fun ⟨y, h⟩ ↦ ⟨(y : R), by ext; simp [h]⟩⟩
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
y : R
h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
hy : y = 0
x : V
⊢ x = 0

Tactic:
simpa [hy] using congr($h x).symm

Premises used: congrArg, id, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
y : R
h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
hy : y = 0
⊢ ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)

Tactic:
exact ⟨1, funext fun x ↦ by simp [by simpa [hy] using congr($h x).symm]⟩
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
y : R
h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
hy : ¬y = 0
x : V
⊢ HSMul.hSMul (β := W) y ((g : (a : V) → W) x : W) = (f : (a : V) → W) x

Tactic:
simpa [eq_symm_apply] using congr($h x)

Premises used: ContinuousLinearEquiv.eq_symm_apply
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
y : R
h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
hy : ¬y = 0
⊢ ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)

Tactic:
exact ⟨.mk0 y hy, funext fun x ↦ by simp [by simpa [eq_symm_apply] using congr($h x)]⟩
-- Module: Mathlib.Analysis.LocallyConvex.SeparatingDual
Goal:
R : Type u_4
V : Type u_5
W : Type u_6
inst : NormedField R
inst_1 : AddCommGroup V
inst_2 : AddCommGroup W
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace W
inst_6 : IsTopologicalRing R
inst_7 : Module R V
inst_8 : Module R W
inst_9 : SeparatingDual R V
inst_10 : IsTopologicalAddGroup V
inst_11 : IsTopologicalAddGroup W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
f g : V ≃L[R] W
h_1 : ∃ (y : R), HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
y : R
h : HSMul.hSMul (β := V →L[R] V) y 1 = (↑g.symm : W →L[R] V) ∘SL (↑f : V →L[R] W)
if : ∀ (hy : y = 0), ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
if₁ : ∀ (hy : ¬y = 0), ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
if₂ : ∀ (hy : y = 0), ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
if₃ if₄ : ∀ (hy : ¬y = 0), ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)
⊢ ∃ (α : Rˣ), Eq (α := (a : V) → W) (⇑f : (a : V) → W) (⇑(α • g) : (a : V) → W)

Tactic:
if hy : y = 0 then exact ⟨1, funext fun x ↦ by simp [by simpa [hy] using congr($h x).symm]⟩
  else exact ⟨.mk0 y hy, funext fun x ↦ by simp [by simpa [eq_symm_apply] using congr($h x)]⟩
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ (G : StrongDual R V),
    Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R) ∧ Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)

Tactic:
exists_eq_one_ne_zero_of_ne_zero_pair hx hy

Premises used: SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
obtain :
  ∀ (G : StrongDual R V) (Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R))
    (Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)), ∃ (A : V ≃L[R] V), (A : (a : V) → V) x = y
⊢ ∃ (A : V ≃L[R] V), (A : (a : V) → V) x = y

Tactic:
obtain ⟨G, Gx, Gy⟩ : ∃ G : StrongDual R V, G x = 1 ∧ G y ≠ 0 :=
    exists_eq_one_ne_zero_of_ne_zero_pair hx hy

Premises used: SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair, 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
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
a b : V
simp :
  a + b +
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) a : R) (y - x) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) b : R) (y - x)) =
    a + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) a : R) (y - x) +
      (b + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) b : R) (y - x))
⊢ a + b + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) (a + b) : R) (y - x) =
    a + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) a : R) (y - x) +
      (b + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) b : R) (y - x))

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
a b : V
⊢ a + b +
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) a : R) (y - x) +
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) b : R) (y - x)) =
    a + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) a : R) (y - x) +
      (b + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) b : R) (y - x))

Tactic:
abel
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
⊢ ∀ (m : R) (x_1 : V),
    m • x_1 + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) (m • x_1) : R) (y - x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        (x_1 + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) x_1 : R) (y - x))

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
z : V
simp :
  z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x) +
      HMul.hMul (α := R) (((G : (a : V) → R) y)⁻¹ : R)
          (HMul.hMul (α := R) (β := R) ((G : (a : V) → R) z : R) ((G : (a : V) → R) y : R)) •
        (x - y) =
    z
⊢ (fun (z : V) ↦ z + HMul.hMul (α := R) (β := R) (((G : (a : V) → R) y)⁻¹ : R) ((G : (a : V) → R) z : R) • (x - y))
      ((fun (z : V) ↦ z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x)) z) =
    z

Tactic:
simp only [RingHom.id_apply, smul_eq_mul,
        -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `map_smulₛₗ` into `map_smulₛₗ _`
        map_add, map_smulₛₗ _, map_sub, Gx, mul_sub, mul_one, add_sub_cancel]

Premises used: map_sub, RingHom.id_apply, mul_sub, map_add, MulActionSemiHomClass.map_smulₛₗ, add_sub_cancel, smul_eq_mul, mul_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
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
z : V
rw :
  z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x) +
      HMul.hMul (α := R) (β := R) (1 : R) ((G : (a : V) → R) z : R) • (x - y) =
    z
⊢ z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x) +
      HMul.hMul (α := R) (((G : (a : V) → R) y)⁻¹ : R)
          (HMul.hMul (α := R) (β := R) ((G : (a : V) → R) z : R) ((G : (a : V) → R) y : R)) •
        (x - y) =
    z

Tactic:
rw [mul_comm (G z), ← mul_assoc, inv_mul_cancel₀ Gy]

Premises used: mul_assoc, mul_comm, 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
inst_7 : IsTopologicalAddGroup V
inst_8 : ContinuousSMul R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
z : V
simp :
  z +
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) y -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) x) +
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) x -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) y) =
    z
⊢ z + HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) (y - x) +
      HMul.hMul (α := R) (β := R) (1 : R) ((G : (a : V) → R) z : R) • (x - y) =
    z

Tactic:
simp only [smul_sub, one_mul]

Premises used: smul_sub, one_mul
-- 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
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : Eq.{u_1 + 1} (α := R) ((G : (a : V) → R) x : R) (1 : R)
Gy : Ne.{u_1 + 1} (α := R) ((G : (a : V) → R) y : R) (0 : R)
z : V
⊢ z +
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) y -
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) x) +
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) x -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((G : (a : V) → R) z : R) y) =
    z

Tactic:
abel