-- Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean
theorem comp (hg : IsConformalMap g) (hf : IsConformalMap f) : IsConformalMap (g.comp f)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : NormedSpace R G
f : M →L[R] N
g : N →L[R] G
hg : IsConformalMap g
hf : IsConformalMap f
⊢ IsConformalMap (g.comp f)

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

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : NormedSpace R G
g : N →L[R] G
hg : IsConformalMap g
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
⊢ IsConformalMap (g.comp (cf • lif.toContinuousLinearMap))

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ (cg • lig.toContinuousLinearMap).comp (cf • lif.toContinuousLinearMap) =
    (cg * cf) • (lig.comp lif).toContinuousLinearMap

Tactic:
rw [smul_comp, comp_smul, mul_smul]

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : 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.comp lif.toContinuousLinearMap = cg • cf • (lig.comp lif).toContinuousLinearMap

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : NormedSpace R G
g : N →L[R] G
hg : IsConformalMap g
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
⊢ IsConformalMap (g.comp (cf • lif.toContinuousLinearMap))

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

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : 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).comp (cf • lif.toContinuousLinearMap))

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : 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.comp lif.toContinuousLinearMap = cg • cf • (lig.comp lif).toContinuousLinearMap

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : 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).comp (cf • lif.toContinuousLinearMap))

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

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ (cg • lig.toContinuousLinearMap).comp (cf • lif.toContinuousLinearMap) =
    (cg * cf) • (lig.comp lif).toContinuousLinearMap