E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)
have minor₁ : ‖map 1‖ ≠ 0 := by simpa only [ext_ring_iff, Ne.def, norm_eq_zero] using nonzero
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ ∀ (x : ℂ), ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖

case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ restrictScalars ℝ map =
    ‖↑map 1‖ • LinearIsometry.toContinuousLinearMap { toLinearMap := ‖↑map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := ?refine'_1 }
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)
refine' ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), _⟩, _⟩
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ ‖↑map 1‖ ≠ 0
simpa only [ext_ring_iff, Ne.def, norm_eq_zero] using nonzero
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
⊢ ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ ∀ (x : ℂ), ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖
intro x
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) x‖ = ‖x‖
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
⊢ ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖
simp only [LinearMap.smul_apply]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) x‖ = ‖x‖
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) x‖ = ‖x‖
have : x = x • (1 : ℂ) := by rw [smul_eq_mul, mul_one]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) (x • 1)‖ = ‖x‖
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) x‖ = ‖x‖
nth_rw 1 [this]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑↑map (x • 1)‖ = ‖x‖
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑(↑ℝ ↑map) (x • 1)‖ = ‖x‖
rw [LinearMap.coe_restrictScalars]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖↑map 1‖⁻¹ * (‖x‖ * ‖↑map 1‖) = ‖x‖
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖‖↑map 1‖⁻¹ • ↑↑map (x • 1)‖ = ‖x‖
simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]
no goals
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
this : x = x • 1
⊢ ‖↑map 1‖⁻¹ * (‖x‖ * ‖↑map 1‖) = ‖x‖
field_simp only [one_mul]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x : ℂ
⊢ x = x • 1
rw [smul_eq_mul, mul_one]
case refine'_2.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x✝ : ℂ
⊢ ↑(restrictScalars ℝ map) x✝ =
    ↑(‖↑map 1‖ •
          LinearIsometry.toContinuousLinearMap
            { toLinearMap := ‖↑map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := (_ : ∀ (x : ℂ), ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖) })
      x✝
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
⊢ restrictScalars ℝ map =
    ‖↑map 1‖ •
      LinearIsometry.toContinuousLinearMap
        { toLinearMap := ‖↑map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := (_ : ∀ (x : ℂ), ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖) }
ext1
no goals
case refine'_2.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ E
z : ℂ
g : ℂ →L[ℝ] E
f : ℂ → E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : ‖↑map 1‖ ≠ 0
x✝ : ℂ
⊢ ↑(restrictScalars ℝ map) x✝ =
    ↑(‖↑map 1‖ •
          LinearIsometry.toContinuousLinearMap
            { toLinearMap := ‖↑map 1‖⁻¹ • ↑ℝ ↑map, norm_map' := (_ : ∀ (x : ℂ), ‖↑(‖↑map 1‖⁻¹ • ↑ℝ ↑map) x‖ = ‖x‖) })
      x✝
rw [coe_restrictScalars', coe_smul', LinearIsometry.coe_toContinuousLinearMap,
  LinearIsometry.coe_mk, Pi.smul_apply, LinearMap.smul_apply, LinearMap.coe_restrictScalars,
  coe_coe, smul_inv_smul₀ minor₁]