awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
have neg : ∀ (z : W)
  (hz :
    ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
        ((0 : (a : W) → W) z : W)),
  ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
Tactic: obtain ⟨z, hz⟩ : ∃ z : W, ¬ f (smulRight v u) z = (0 : W →L[𝕜] W) z := by
    simp_rw [← not_forall, ← ContinuousLinearMap.ext_iff, map_eq_zero_iff,
      ContinuousLinearMap.ext_iff, not_forall, smulRight_apply, zero_apply,
      smul_eq_zero_iff_left hu]
    exact ⟨u, huv⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
have hT : ∀ (x : V),
  Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
    ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
Tactic: have hT x : T x = f (smulRight v x) z := rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
A : V →L[𝕜] V
x : V
⊢ Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
    ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
have simp : Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v ((A : (a : V) → V) x)) : W →L[𝕜] W) : (a : W) → W) z : W)
  ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (A * smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
Tactic: simp only [hT, ← mul_apply, ← map_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
A : V →L[𝕜] V
x : V
⊢ Eq (α := W)
    ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v ((A : (a : V) → V) x)) : W →L[𝕜] W) : (a : W) → W) z : W)
    ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (A * smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
have e_a : smulRight v ((A : (a : V) → V) x) = A * smulRight v x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
A : V →L[𝕜] V
x : V
⊢ smulRight v ((A : (a : V) → V) x) = A * smulRight v x
have e_a : ∀ (x_1 : V),
  Eq (α := V) (((smulRight v ((A : (a : V) → V) x) : V →L[𝕜] V) : (a : V) → V) x_1 : V)
    ((A * smulRight v x : (a : V) → V) x_1 : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
have this : ∀ (A : V →L[𝕜] V) (x : V),
  Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
    ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
Tactic: have this A x : T (A x) = f A (T x) := by
    simp only [hT, ← mul_apply, ← map_mul]
    congr; ext; simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
have neg : ∀ (d : StrongDual 𝕜 W)
  (hd :
    Eq.{u_1 + 1} (α := 𝕜)
      ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
      (1 : 𝕜)),
  ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
Tactic: have ⟨d, hd⟩ := SeparatingDual.exists_eq_one (R := 𝕜) hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
    (1 : 𝕜)
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
have surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
Tactic: have surj : Function.Surjective T := fun w ↦ ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
    (1 : 𝕜)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
x y : V
hxy : Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W) ((T : (a : V) → W) y : W)
⊢ Eq (α := V →L[𝕜] V) (smulRight v x) (smulRight v y)
have apply : ∀ (z : W),
  Eq (α := W) ((((f.toAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
    ((((f.toAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v y) : W →L[𝕜] W) : (a : W) → W) z : W)
Tactic: apply f.injective <| ContinuousLinearMap.ext fun z ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z_1 : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z_1 : W)
      ((0 : (a : W) → W) z_1 : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z_1)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z_1 : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z_1 : W) : 𝕜)
    (1 : 𝕜)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
x y : V
hxy : Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W) ((T : (a : V) → W) y : W)
z : W
⊢ Eq (α := W) ((((f.toAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
    ((((f.toAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v y) : W →L[𝕜] W) : (a : W) → W) z : W)
have obtain : ∀ (w : V),
  Eq.{u_3 + 1} (α := W)
    ((((f.toAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W)
        ((T : (a : V) → W) w : W) :
      W)
    ((((f.toAlgEquiv : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v y) : W →L[𝕜] W) : (a : W) → W)
        ((T : (a : V) → W) w : W) :
      W)
Tactic: obtain ⟨w, rfl⟩ := surj z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
    (1 : 𝕜)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
x y : V
hxy : Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W) ((T : (a : V) → W) y : W)
⊢ x = y
have h_smul : Eq (α := V →L[𝕜] V) (smulRight v x) (smulRight v y)
Tactic: have h_smul : smulRight v x = smulRight v y := by
      apply f.injective <| ContinuousLinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp [← this, hxy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
    (1 : 𝕜)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
⊢ ∃ (U : V ≃L[𝕜] W),
    ∀ (x : V →L[𝕜] V),
      comp (σ₂₃ := RingHom.id 𝕜) ((f : (a : V →L[𝕜] V) → W →L[𝕜] W) x) (↑U : V →L[𝕜] W) = (↑U : V →L[𝕜] W) ∘SL x
have inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
Tactic: have inj : Function.Injective T := fun x y hxy ↦ by
    have h_smul : smulRight v x = smulRight v y := by
      apply f.injective <| ContinuousLinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp [← this, hxy]
    simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup V
inst_2 : SeminormedAddCommGroup W
inst_3 : NormedSpace 𝕜 V
inst_4 : NormedSpace 𝕜 W
inst_5 : SeparatingDual 𝕜 V
inst_6 : SeparatingDual 𝕜 W
f : ContinuousAlgEquiv.{u_1, u_2, u_3} 𝕜 (V →L[𝕜] V) (W →L[𝕜] W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : Ne.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) u : 𝕜) (0 : 𝕜)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →L[𝕜] W :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' W (RingHom.id 𝕜) : (a : W) → (W →L[𝕜] W) →L[𝕜] W) z)
    ((↑f : (V →L[𝕜] V) →A[𝕜] W →L[𝕜] W).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 V V : (a : StrongDual 𝕜 V) → V →L[𝕜] V →L[𝕜] V) v))
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v x) : W →L[𝕜] W) : (a : W) → W) z : W)
this :
  ∀ (A : V →L[𝕜] V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) A : W →L[𝕜] W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
d : StrongDual 𝕜 W
hd :
  Eq.{u_1 + 1} (α := 𝕜)
    ((d : (a : W) → 𝕜) ((((f : (a : V →L[𝕜] V) → W →L[𝕜] W) (smulRight v u) : W →L[𝕜] W) : (a : W) → W) z : W) : 𝕜)
    (1 : 𝕜)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
Tₗ : V ≃ₗ[𝕜] W := LinearEquiv.ofBijective (↑T : V →ₗ[𝕜] W) ⋯
T' : W →L[𝕜] V :=
  comp (σ₂₃ := RingHom.id 𝕜) ((apply' V (RingHom.id 𝕜) : (a : V) → (V →L[𝕜] V) →L[𝕜] V) u)
    ((↑f.symm : (W →L[𝕜] W) →A[𝕜] V →L[𝕜] V).toContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜)
      ((smulRightL 𝕜 W W : (a : StrongDual 𝕜 W) → W →L[𝕜] W →L[𝕜] W) d))
⊢ Continuous Tₗ.invFun
have change : Continuous.{u_3, u_2} (X := W) (Y := V) (⇑(↑Tₗ.symm : W →ₗ[𝕜] V) : (a : W) → V)
Tactic: change Continuous Tₗ.symm.toLinearMap