awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : NormedSpace R M
inst_4 : NormedSpace R N
c : R
hc : c ≠ 0
c' : R
hc' : c' ≠ 0
li : M →ₗᵢ[R] N
⊢ IsConformalMap (c • c' • li.toContinuousLinearMap)

Tactic:
exact ⟨c * c', mul_ne_zero hc hc', li, smul_smul _ _ _⟩
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : NormedSpace R M
c : R
hc : c ≠ 0
⊢ IsConformalMap (HSMul.hSMul (β := M →L[R] M) c (ContinuousLinearMap.id R M))

Tactic:
isConformalMap_id.smul hc

Premises used: isConformalMap_id, IsConformalMap.smul
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : NormedSpace R M
inst_4 : NormedSpace R N
f' : M →ₗᵢ[R] N
⊢ IsConformalMap f'.toContinuousLinearMap

Tactic:
⟨1, one_ne_zero, f', (one_smul _ _).symm⟩

Premises used: one_smul, And.intro, Exists.intro, IsConformalMap, one_ne_zero, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : NormedSpace R M
inst_4 : NormedSpace R N
inst_5 : Subsingleton M
f' : M →L[R] N
x : M
⊢ norm.{u_3} (E := N) ((0 : (a : M) → N) x : N) = ‖x‖

Tactic:
simp [Subsingleton.elim x 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
f : M →L[R] N
g : N →L[R] G
hg : IsConformalMap g
hf : IsConformalMap f
rcases : ∀ (cf : R) (hcf : cf ≠ 0) (lif : M →ₗᵢ[R] N), IsConformalMap (g ∘SL (cf • lif.toContinuousLinearMap))
⊢ IsConformalMap (g ∘SL f)

Tactic:
rcases hf with ⟨cf, hcf, lif, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
g : N →L[R] G
hg : IsConformalMap g
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
rcases :
  ∀ (cg : R) (hcg : cg ≠ 0) (lig : N →ₗᵢ[R] G),
    IsConformalMap ((cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap))
⊢ IsConformalMap (g ∘SL (cf • lif.toContinuousLinearMap))

Tactic:
rcases hg with ⟨cg, hcg, lig, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ IsConformalMap ((cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap))

Tactic:
⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro, LinearIsometry.comp, mul_ne_zero, IsConformalMap
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
refine :
  (cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap) =
    (cg * cf) • (lig.comp lif).toContinuousLinearMap
⊢ IsConformalMap ((cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap))

Tactic:
refine ⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, ?_⟩
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
rw : cg • cf • lig.toContinuousLinearMap ∘SL lif.toContinuousLinearMap = cg • cf • (lig.comp lif).toContinuousLinearMap
⊢ (cg • lig.toContinuousLinearMap) ∘SL (cf • lif.toContinuousLinearMap) =
    (cg * cf) • (lig.comp lif).toContinuousLinearMap

Tactic:
rw [smul_comp, comp_smul, mul_smul]

Premises used: ContinuousLinearMap.smul_comp, SemigroupAction.mul_smul, ContinuousLinearMap.comp_smul
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst : NormedField R
inst_1 : SeminormedAddCommGroup M
inst_2 : SeminormedAddCommGroup N
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace R M
inst_5 : NormedSpace R N
inst_6 : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ cg • cf • lig.toContinuousLinearMap ∘SL lif.toContinuousLinearMap = cg • cf • (lig.comp lif).toContinuousLinearMap

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
N : Type u_3
M' : Type u_5
inst : NormedField R
inst_1 : SeminormedAddCommGroup N
inst_2 : NormedSpace R N
inst_3 : NormedAddCommGroup M'
inst_4 : NormedSpace R M'
f : M' →L[R] N
h : IsConformalMap f
rcases :
  ∀ (c : R) (hc : c ≠ 0) (li : M' →ₗᵢ[R] N),
    Injective.{u_5 + 1, u_3 + 1} (α := M') (β := N) (⇑(c • li.toContinuousLinearMap) : (a : M') → N)
⊢ Injective.{u_5 + 1, u_3 + 1} (α := M') (β := N) (⇑f : (a : M') → N)

Tactic:
rcases h with ⟨c, hc, li, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
N : Type u_3
M' : Type u_5
inst : NormedField R
inst_1 : SeminormedAddCommGroup N
inst_2 : NormedSpace R N
inst_3 : NormedAddCommGroup M'
inst_4 : NormedSpace R M'
c : R
hc : c ≠ 0
li : M' →ₗᵢ[R] N
⊢ Injective.{u_5 + 1, u_3 + 1} (α := M') (β := N) (⇑(c • li.toContinuousLinearMap) : (a : M') → N)

Tactic:
(smul_right_injective _ hc).comp li.injective

Premises used: smul_right_injective, LinearIsometry.injective, Function.Injective.comp
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
N : Type u_3
M' : Type u_5
inst : NormedField R
inst_1 : SeminormedAddCommGroup N
inst_2 : NormedSpace R N
inst_3 : NormedAddCommGroup M'
inst_4 : NormedSpace R M'
c : R
hc : c ≠ 0
li : M' →ₗᵢ[R] N
⊢ Injective.{u_5 + 1, u_3 + 1} (α := M') (β := N) (⇑(c • li.toContinuousLinearMap) : (a : M') → N)

Tactic:
exact (smul_right_injective _ hc).comp li.injective

Premises used: smul_right_injective, LinearIsometry.injective, Function.Injective.comp
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
N : Type u_3
M' : Type u_5
inst : NormedField R
inst_1 : SeminormedAddCommGroup N
inst_2 : NormedSpace R N
inst_3 : NormedAddCommGroup M'
inst_4 : NormedSpace R M'
inst_5 : Nontrivial M'
hf' : IsConformalMap.{u_1, u_5, u_3} (R := R) (X := M') (Y := N) 0
rcases : ∀ (a : M') (ha : a ≠ 0), False
⊢ False

Tactic:
rcases exists_ne (0 : M') with ⟨a, ha⟩

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
N : Type u_3
M' : Type u_5
inst : NormedField R
inst_1 : SeminormedAddCommGroup N
inst_2 : NormedSpace R N
inst_3 : NormedAddCommGroup M'
inst_4 : NormedSpace R M'
inst_5 : Nontrivial M'
hf' : IsConformalMap.{u_1, u_5, u_3} (R := R) (X := M') (Y := N) 0
a : M'
ha : a ≠ 0
⊢ False

Tactic:
ha (hf'.injective rfl)

Premises used: IsConformalMap.injective, rfl
-- Module: Mathlib.Analysis.Normed.Operator.Conformal
Goal:
R : Type u_1
N : Type u_3
M' : Type u_5
inst : NormedField R
inst_1 : SeminormedAddCommGroup N
inst_2 : NormedSpace R N
inst_3 : NormedAddCommGroup M'
inst_4 : NormedSpace R M'
inst_5 : Nontrivial M'
hf' : IsConformalMap.{u_1, u_5, u_3} (R := R) (X := M') (Y := N) 0
a : M'
ha : a ≠ 0
⊢ False

Tactic:
exact ha (hf'.injective rfl)

Premises used: IsConformalMap.injective, 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)
pos : ∀ (hV : Subsingleton V), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
neg : ∀ (hV : Nontrivial V), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv

Tactic:
by_cases! hV : Subsingleton V

Premises used: Subsingleton
-- 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 : Subsingleton V
pos : ∀ (hV : Subsingleton W), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
neg : ∀ (hV : Nontrivial W), ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv

Tactic:
by_cases! hV : Subsingleton W

Premises used: Subsingleton
-- 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_1 : Subsingleton V
hV : Subsingleton W
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv

Tactic:
⟨{ toLinearEquiv := 0 }, ext <| Subsingleton.allEq _ _⟩

Premises used: ContinuousLinearEquiv.mk, Subsingleton.allEq, Exists.intro, ContinuousAlgEquiv.ext, OfNat.ofNat
-- 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_1 : Subsingleton V
hV : Subsingleton W
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv

Tactic:
exact ⟨{ toLinearEquiv := 0 }, ext <| Subsingleton.allEq _ _⟩
-- 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_1 : Subsingleton V
hV : Nontrivial W
⊢ ∃ (U : V ≃L[𝕜] W), f = U.conjContinuousAlgEquiv

Tactic:
simpa using congr(f $(Subsingleton.allEq 0 1))
-- 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
neg :
  ∃ (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), f = U.conjContinuousAlgEquiv

Tactic:
simp_rw [ContinuousAlgEquiv.ext_iff, funext_iff, conjContinuousAlgEquiv_apply, ← comp_assoc,
    eq_comp_toContinuousLinearMap_symm]

Premises used: ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, funext_iff, ContinuousAlgEquiv.ext_iff, ContinuousLinearEquiv.eq_comp_toContinuousLinearMap_symm, ContinuousLinearMap.comp_assoc
-- 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
neg :
  ∀ (u : V) (hu : 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
⊢ ∃ (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 ⟨u, hu⟩ := exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- 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
neg :
  ∀ (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
⊢ ∃ (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 ⟨v, huv⟩ := SeparatingDual.exists_ne_zero (R := 𝕜) hu

Premises used: SeparatingDual.exists_ne_zero
-- 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 : 𝕜)
simp_rw : ∃ (x : V), ¬Eq.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ ∃ (z : W),
    ¬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)

Tactic:
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]

Premises used: smul_eq_zero_iff_left, ContinuousLinearMap.ext_iff, ContinuousAlgEquiv.map_eq_zero_iff, ContinuousLinearMap.smulRight_apply, Classical.not_forall, ContinuousLinearMap.zero_apply
-- 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 : 𝕜)
⊢ ∃ (x : V), ¬Eq.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
⟨u, huv⟩

Premises used: Exists.intro
-- 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 : 𝕜)
⊢ ∃ (x : V), ¬Eq.{u_1 + 1} (α := 𝕜) ((v : (a : V) → 𝕜) x : 𝕜) (0 : 𝕜)

Tactic:
exact ⟨u, huv⟩
-- 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 : 𝕜)
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
⊢ ∃ (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⟩
-- 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))
⊢ ∀ (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
-- 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
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)
⊢ 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:
simp only [hT, ← mul_apply, ← map_mul]

Premises used: ContinuousLinearMap.mul_apply, map_mul
-- 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
e_a : smulRight v ((A : (a : V) → V) x) = A * smulRight v x
⊢ 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:
congr
-- 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
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)
⊢ smulRight v ((A : (a : V) → V) x) = A * smulRight v x

Tactic:
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 : 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 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:
simp