case intro.intro.intro
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
g : N →L[R] G
c : R
hg : IsConformalMap g
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
⊢ IsConformalMap (ContinuousLinearMap.comp g (cf • toContinuousLinearMap lif))
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c : R
hg : IsConformalMap g
hf : IsConformalMap f
⊢ IsConformalMap (ContinuousLinearMap.comp g f)
rcases hf with ⟨cf, hcf, lif, rfl⟩
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ IsConformalMap (ContinuousLinearMap.comp (cg • toContinuousLinearMap lig) (cf • toContinuousLinearMap lif))
case intro.intro.intro
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
g : N →L[R] G
c : R
hg : IsConformalMap g
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
⊢ IsConformalMap (ContinuousLinearMap.comp g (cf • toContinuousLinearMap lif))
rcases hg with ⟨cg, hcg, lig, rfl⟩
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ ContinuousLinearMap.comp (cg • toContinuousLinearMap lig) (cf • toContinuousLinearMap lif) =
    (cg * cf) • toContinuousLinearMap (LinearIsometry.comp lig lif)
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ IsConformalMap (ContinuousLinearMap.comp (cg • toContinuousLinearMap lig) (cf • toContinuousLinearMap lif))
refine' ⟨cg * cf, mul_ne_zero hcg hcf, lig.comp lif, _⟩
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ cg • cf • ContinuousLinearMap.comp (toContinuousLinearMap lig) (toContinuousLinearMap lif) =
    cg • cf • toContinuousLinearMap (LinearIsometry.comp lig lif)
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ ContinuousLinearMap.comp (cg • toContinuousLinearMap lig) (cf • toContinuousLinearMap lif) =
    (cg * cf) • toContinuousLinearMap (LinearIsometry.comp lig lif)
rw [smul_comp, comp_smul, mul_smul]
no goals
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_4
N : Type u_2
G : Type u_3
M' : Type ?u.216873
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ cg • cf • ContinuousLinearMap.comp (toContinuousLinearMap lig) (toContinuousLinearMap lif) =
    cg • cf • toContinuousLinearMap (LinearIsometry.comp lig lif)
rfl