awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : TopologicalSpace V
inst_3 : TopologicalSpace R
inst_4 : Module R V
inst_5 : SeparatingDual R V
x y : V
⊢ x = y ↔ ∀ (g : StrongDual R V), Eq.{u_1 + 1} (α := R) ((g : (a : V) → R) x : R) ((g : (a : V) → R) y : R)
have 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)
Tactic: rw [← sub_eq_zero, eq_zero_iff_forall_dual_eq_zero (R := R) (x - y)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ 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)
have 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
Tactic: simp_rw [separatingDual_def, Ne, injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ (∀ (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
have 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
Tactic: congrm ∀ v, ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ (¬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
have 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
Tactic: rw [not_imp_comm, LinearMap.ext_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
have 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
Tactic: push Not
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (hypothesis)
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)
⊢ Surjective (α := V →L[R] R) (β := Module.Dual R W)
    ((⇑f.dualMap : (a : Module.Dual R V) → Module.Dual R W) ∘ ContinuousLinearMap.toLinearMap)
have 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))
Tactic: have := (separatingDual_iff_injective.mp ‹_›).comp hf
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (hypothesis)
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))
⊢ Surjective (α := V →L[R] R) (β := Module.Dual R W)
    ((⇑f.dualMap : (a : Module.Dual R V) → Module.Dual R W) ∘ ContinuousLinearMap.toLinearMap)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ Nontrivial (V →L[R] W)
have obtain : ∀ (v : V) (hv : v ≠ 0), Nontrivial (V →L[R] W)
Tactic: obtain ⟨v, hv⟩ := exists_ne (0 : V)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ Nontrivial (V →L[R] W)
have obtain : ∀ (w : W) (hw : w ≠ 0), Nontrivial (V →L[R] W)
Tactic: obtain ⟨w, hw⟩ := exists_ne (0 : W)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ Nontrivial (V →L[R] W)
have obtain : ∀ (ψ : StrongDual R V) (hψ : Ne.{u_1 + 1} (α := R) ((ψ : (a : V) → R) v : R) (0 : R)), Nontrivial (V →L[R] W)
Tactic: obtain ⟨ψ, hψ⟩ := exists_ne_zero (R := R) hv
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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), Eq.{u_1 + 1} (α := R) ((f : (a : V) → R) x : R) (1 : R)
have 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)
Tactic: rcases exists_ne_zero (R := R) hx with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨u, ux⟩ : ∃ u : StrongDual R V, u x = 1 := exists_eq_one hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases ne_or_eq (u y) 0 with uy | uy
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases ne_or_eq (u y) 0 with uy | uy
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨v, vy⟩ : ∃ v : StrongDual R V, v y = 1 := exists_eq_one hy
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases ne_or_eq (v x) 0 with vx | vx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases ne_or_eq (v x) 0 with vx | vx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ Membership.mem (γ := Subalgebra S (V →L[R] V)) ⊥ f
have suffices : ∃ (α : R),
  Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
    f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
Tactic: suffices ∃ α ∈ Subalgebra.center S R, f = α • .id R V from
      have ⟨_, ⟨y, _⟩, _⟩ := Algebra.IsCentral.center_eq_bot S R ▸ this
      ⟨y, by aesop⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (hypothesis)
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
⊢ ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
have a : Nontrivial V
Tactic: nontriviality V
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
have 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)
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : V)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
have 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)
Tactic: obtain ⟨g, hg⟩ := exists_eq_one (R := R) hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (hypothesis)
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)
⊢ ∃ (α : R),
    Membership.mem (γ := Subalgebra S R) (Subalgebra.center S R) α ∧
      f = HSMul.hSMul (β := V →L[R] V) α (ContinuousLinearMap.id R V)
have 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
Tactic: have (y : V) := by simpa [hg] using congr($(Subalgebra.mem_center_iff.mp hf (g.smulRight y)) x)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
| Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) f.conjContinuousAlgEquiv
    g.conjContinuousAlgEquiv
have rw : Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) g.conjContinuousAlgEquiv f.conjContinuousAlgEquiv
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.SeparatingDual (goal)
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
⊢ Eq (α := ContinuousAlgEquiv.{u_4, u_5, u_6} R (V →L[R] V) (W →L[R] W)) f.conjContinuousAlgEquiv
      g.conjContinuousAlgEquiv ↔
    ∃ (α : Rˣ), f = α • g
have 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
Tactic: conv_lhs => rw [eq_comm]