awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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)

Tactic:
have this A x : T (A x) = f A (T x) := by
    simp only [hT, ← mul_apply, ← map_mul]
    congr; ext; simp
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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)
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
⊢ ∃ (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
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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 : 𝕜)
w : W
⊢ (T : (a : V) → W) ((((f.symm : (a : W →L[𝕜] W) → V →L[𝕜] V) (smulRight d w) : V →L[𝕜] V) : (a : V) → V) u : V) = w

Tactic:
simp [T, this, hd]
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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 : 𝕜)
⊢ 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]⟩
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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)
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)
⊢ Eq (α := V →L[𝕜] V) (smulRight v x) (smulRight v y)

Tactic:
apply f.injective <| ContinuousLinearMap.ext fun z ↦ ?_

Premises used: AlgEquiv.injective, ContinuousAlgEquiv.toAlgEquiv, ContinuousLinearMap.ext
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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
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)
⊢ 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:
obtain ⟨w, rfl⟩ := surj z

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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)
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:
simp [← this, hxy]
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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)

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]
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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)
h_smul : Eq (α := V →L[𝕜] V) (smulRight v x) (smulRight v y)
⊢ x = y

Tactic:
simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)

Premises used: Ne.isUnit, IsUnit.smul_left_cancel
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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)
⊢ 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)
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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))
change : Continuous.{u_3, u_2} (X := W) (Y := V) (⇑(↑Tₗ.symm : W →ₗ[𝕜] V) : (a : W) → V)
⊢ Continuous Tₗ.invFun

Tactic:
change Continuous Tₗ.symm.toLinearMap

Premises used: LinearEquiv.symm, Continuous, LinearEquiv.toLinearMap, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
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))
suffices : (↑T' : W →ₗ[𝕜] V) = (↑Tₗ.symm : W →ₗ[𝕜] V)
⊢ Continuous.{u_3, u_2} (X := W) (Y := V) (⇑(↑Tₗ.symm : W →ₗ[𝕜] V) : (a : W) → V)

Tactic:
suffices T'.toLinearMap = Tₗ.symm from this ▸ T'.continuous