case mp
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ IsConformalMap f → ∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f u) (↑f v) = c * inner u v

case mpr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ (∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f u) (↑f v) = c * inner u v) → IsConformalMap f
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ IsConformalMap f ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f u) (↑f v) = c * inner u v
constructor
case mp.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ ∃ c,
    0 < c ∧ ∀ (u v : E), inner (↑(c₁ • toContinuousLinearMap li) u) (↑(c₁ • toContinuousLinearMap li) v) = c * inner u v
case mp
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ IsConformalMap f → ∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f u) (↑f v) = c * inner u v
rintro ⟨c₁, hc₁, li, rfl⟩
case mp.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
u v : E
⊢ inner (↑(c₁ • toContinuousLinearMap li) u) (↑(c₁ • toContinuousLinearMap li) v) = c₁ * c₁ * inner u v
case mp.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ ∃ c,
    0 < c ∧ ∀ (u v : E), inner (↑(c₁ • toContinuousLinearMap li) u) (↑(c₁ • toContinuousLinearMap li) v) = c * inner u v
refine' ⟨c₁ * c₁, mul_self_pos.2 hc₁, fun u v => _⟩
no goals
case mp.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
u v : E
⊢ inner (↑(c₁ • toContinuousLinearMap li) u) (↑(c₁ • toContinuousLinearMap li) v) = c₁ * c₁ * inner u v
simp only [real_inner_smul_left, real_inner_smul_right, mul_assoc, coe_smul',
  coe_toContinuousLinearMap, Pi.smul_apply, inner_map_map]
case mpr.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c₁ * inner u v
⊢ IsConformalMap f
case mpr
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
⊢ (∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f u) (↑f v) = c * inner u v) → IsConformalMap f
rintro ⟨c₁, hc₁, huv⟩
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c₁ * inner u v
⊢ ∃ c, 0 < c ∧ c₁ = c * c

case mpr.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ IsConformalMap f
case mpr.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c₁ * inner u v
⊢ IsConformalMap f
obtain ⟨c, hc, rfl⟩ : ∃ c : ℝ, 0 < c ∧ c₁ = c * c
case mpr.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ IsConformalMap f
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c₁ * inner u v
⊢ ∃ c, 0 < c ∧ c₁ = c * c

case mpr.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ IsConformalMap f
exact ⟨Real.sqrt c₁, Real.sqrt_pos.2 hc₁, (Real.mul_self_sqrt hc₁.le).symm⟩
case mpr.intro.intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
u v : E
⊢ inner (↑↑(c⁻¹ • f) u) (↑↑(c⁻¹ • f) v) = inner u v

case mpr.intro.intro.intro.intro.refine'_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ f =
    c •
      toContinuousLinearMap
        (LinearMap.isometryOfInner ↑(c⁻¹ • f) (_ : ∀ (u v : E), inner (↑↑(c⁻¹ • f) u) (↑↑(c⁻¹ • f) v) = inner u v))
case mpr.intro.intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ IsConformalMap f
refine' ⟨c, hc.ne', (c⁻¹ • f : E →ₗ[ℝ] F).isometryOfInner fun u v => _, _⟩
no goals
case mpr.intro.intro.intro.intro.refine'_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
u v : E
⊢ inner (↑↑(c⁻¹ • f) u) (↑↑(c⁻¹ • f) v) = inner u v
simp only [real_inner_smul_left, real_inner_smul_right, huv, mul_assoc, coe_smul,
  inv_mul_cancel_left₀ hc.ne', LinearMap.smul_apply, ContinuousLinearMap.coe_coe]
case mpr.intro.intro.intro.intro.refine'_2.h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
x : E
⊢ ↑f x =
    ↑(c •
          toContinuousLinearMap
            (LinearMap.isometryOfInner ↑(c⁻¹ • f) (_ : ∀ (u v : E), inner (c⁻¹ • ↑f u) (c⁻¹ • ↑f v) = inner u v)))
      x
case mpr.intro.intro.intro.intro.refine'_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
⊢ f =
    c •
      toContinuousLinearMap
        (LinearMap.isometryOfInner ↑(c⁻¹ • f) (_ : ∀ (u v : E), inner (c⁻¹ • ↑f u) (c⁻¹ • ↑f v) = inner u v))
ext1 x
no goals
case mpr.intro.intro.intro.intro.refine'_2.h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner (↑f u) (↑f v) = c * c * inner u v
x : E
⊢ ↑f x =
    ↑(c •
          toContinuousLinearMap
            (LinearMap.isometryOfInner ↑(c⁻¹ • f) (_ : ∀ (u v : E), inner (c⁻¹ • ↑f u) (c⁻¹ • ↑f v) = inner u v)))
      x
exact (smul_inv_smul₀ hc.ne' (f x)).symm