awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
u : Circle
v : E
rw : ‖(↑u : ℂ) • v‖ = ‖v‖
⊢ ‖u • v‖ = ‖v‖
have rw₁ : ‖(↑u : ℂ)‖ * ‖v‖ = ‖v‖
Tactic: rw [smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
u : Circle
v : E
rw : ‖(↑u : ℂ) • v‖ = ‖v‖
rw₁ : ‖(↑u : ℂ)‖ * ‖v‖ = ‖v‖
⊢ ‖u • v‖ = ‖v‖
have rw₂ : 1 * ‖v‖ = ‖v‖
Tactic: rw [smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
E : Type u_4
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℂ E
u : Circle
v : E
rw : ‖(↑u : ℂ) • v‖ = ‖v‖
rw₁ : ‖(↑u : ℂ)‖ * ‖v‖ = ‖v‖
rw₂ : 1 * ‖v‖ = ‖v‖
⊢ ‖u • v‖ = ‖v‖
have rw₃ : ‖v‖ = ‖v‖
Tactic: rw [smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
⊢ Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * 0) : Circle) (1 : Circle)
have rw : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
Tactic: rw [mul_zero, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
rw : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
⊢ Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * 0) : Circle) (1 : Circle)
have rw₁ : Eq (α := Circle) 1 1
Tactic: rw [mul_zero, Circle.exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x y : ℝ
⊢ (Circle.exp : (a : ℝ) → Circle) (2 * π * (x + y)) =
    HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * x) : Circle)
      ((Circle.exp : (a : ℝ) → Circle) (2 * π * y) : Circle)
have rw : (Circle.exp : (a : ℝ) → Circle) (2 * π * x + 2 * π * y) =
  HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * x) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π * y) : Circle)
Tactic: rw [mul_add, Circle.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
x y : ℝ
rw :
  (Circle.exp : (a : ℝ) → Circle) (2 * π * x + 2 * π * y) =
    HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * x) : Circle)
      ((Circle.exp : (a : ℝ) → Circle) (2 * π * y) : Circle)
⊢ (Circle.exp : (a : ℝ) → Circle) (2 * π * (x + y)) =
    HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * x) : Circle)
      ((Circle.exp : (a : ℝ) → Circle) (2 * π * y) : Circle)
have rw₁ : HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * x) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π * y) : Circle) =
  HMul.hMul (α := Circle) (β := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * x) : Circle)
    ((Circle.exp : (a : ℝ) → Circle) (2 * π * y) : Circle)
Tactic: rw [mul_add, Circle.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
⊢ 𝐞 ≠ 1
have rw : ∃ (a : ℝ), Ne (α := Circle) ((𝐞 : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
Tactic: rw [DFunLike.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
⊢ ∃ (a : ℝ), Ne (α := Circle) ((𝐞 : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
have h : Ne (α := Circle) ((𝐞 : (a : ℝ) → Circle) 2⁻¹) ((1 : (a : ℝ) → Circle) 2⁻¹)
Tactic: use 2⁻¹
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
⊢ Ne (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * 2⁻¹) : Circle) (1 : Circle)
have h : Ne (α := Circle) ((Circle.exp : (a : ℝ) → Circle) π : Circle) (1 : Circle)
Tactic: rw [mul_comm, ← mul_assoc, inv_mul_cancel₀ (by positivity), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
⊢ probChar ≠ 1
have rw : ∃ (a : ℝ), Ne (α := Circle) ((probChar : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
Tactic: rw [DFunLike.ne_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Circle (goal)
Goal:
⊢ ∃ (a : ℝ), Ne (α := Circle) ((probChar : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
have h : Ne (α := Circle) ((probChar : (a : ℝ) → Circle) π : Circle) ((1 : (a : ℝ) → Circle) π : Circle)
Tactic: use Real.pi
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ IsConformalMap.{0, 0, u_1} (R := ℝ) (X := ℂ) (Y := E) (restrictScalars ℝ map)
have minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
Tactic: have minor₁ : ‖map 1‖ ≠ 0 := by
    simpa only [ContinuousLinearMap.ext_ring_iff, Ne, norm_eq_zero] using nonzero
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
⊢ IsConformalMap.{0, 0, u_1} (R := ℝ) (X := ℂ) (Y := E) (restrictScalars ℝ map)
have refine_1 : ∀ (x : ℂ),
  norm (E := E)
      ((HSMul.hSMul (β := ℂ →ₗ[ℝ] E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
              ((↑ℝ :
                  {S M : Type} →
                    {M₂ : Type u_1} →
                      [inst : Semiring ℝ] →
                        [inst_3 : Semiring S] →
                          [inst_4 : AddCommMonoid M] →
                            [inst_5 : AddCommMonoid M₂] →
                              [inst_6 : Module ℝ M] →
                                [inst_7 : Module ℝ M₂] →
                                  [inst_8 : Module S M] →
                                    [inst_9 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                (↑map : ℂ →ₗ[ℂ] E)) :
            (a : ℂ) → E)
          x :
        E) =
    ‖x‖
Tactic: refine ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
refine_1 :
  ∀ (x : ℂ),
    norm (E := E)
        ((HSMul.hSMul (β := ℂ →ₗ[ℝ] E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
                ((↑ℝ :
                    {S M : Type} →
                      {M₂ : Type u_1} →
                        [inst : Semiring ℝ] →
                          [inst_3 : Semiring S] →
                            [inst_4 : AddCommMonoid M] →
                              [inst_5 : AddCommMonoid M₂] →
                                [inst_6 : Module ℝ M] →
                                  [inst_7 : Module ℝ M₂] →
                                    [inst_8 : Module S M] →
                                      [inst_9 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                  (↑map : ℂ →ₗ[ℂ] E)) :
              (a : ℂ) → E)
            x :
          E) =
      ‖x‖
⊢ IsConformalMap.{0, 0, u_1} (R := ℝ) (X := ℂ) (Y := E) (restrictScalars ℝ map)
have refine_2 : restrictScalars ℝ map =
  norm (E := E) ((map : (a : ℂ) → E) 1 : E) •
    {
        toLinearMap :=
          HSMul.hSMul (β := ℂ →ₗ[ℝ] E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
            ((↑ℝ :
                {S M : Type} →
                  {M₂ : Type u_1} →
                    [inst : Semiring ℝ] →
                      [inst_3 : Semiring S] →
                        [inst_4 : AddCommMonoid M] →
                          [inst_5 : AddCommMonoid M₂] →
                            [inst_6 : Module ℝ M] →
                              [inst_7 : Module ℝ M₂] →
                                [inst_8 : Module S M] →
                                  [inst_9 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              (↑map : ℂ →ₗ[ℂ] E)),
        norm_map' := sorry : ℂ →ₗᵢ[ℝ] E }.toContinuousLinearMap
Tactic: refine ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
x : ℂ
⊢ norm (E := E)
      ((HSMul.hSMul (β := ℂ →ₗ[ℝ] E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
              ((↑ℝ :
                  {S M : Type} →
                    {M₂ : Type u_1} →
                      [inst : Semiring ℝ] →
                        [inst_3 : Semiring S] →
                          [inst_4 : AddCommMonoid M] →
                            [inst_5 : AddCommMonoid M₂] →
                              [inst_6 : Module ℝ M] →
                                [inst_7 : Module ℝ M₂] →
                                  [inst_8 : Module S M] →
                                    [inst_9 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                (↑map : ℂ →ₗ[ℂ] E)) :
            (a : ℂ) → E)
          x :
        E) =
    ‖x‖
have refine_1 : ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
      (((↑ℝ :
                {S M : Type} →
                  {M₂ : Type u_1} →
                    [inst : Semiring ℝ] →
                      [inst_3 : Semiring S] →
                        [inst_4 : AddCommMonoid M] →
                          [inst_5 : AddCommMonoid M₂] →
                            [inst_6 : Module ℝ M] →
                              [inst_7 : Module ℝ M₂] →
                                [inst_8 : Module S M] →
                                  [inst_9 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              (↑map : ℂ →ₗ[ℂ] E) :
            (a : ℂ) → E)
          x :
        E)‖ =
  ‖x‖
Tactic: simp only [LinearMap.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
x : ℂ
⊢ x = HSMul.hSMul (β := ℂ) x 1
have rw : x = x * 1
Tactic: rw [smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
x : ℂ
rw : x = x * 1
⊢ x = HSMul.hSMul (β := ℂ) x 1
have rw₁ : x = x
Tactic: rw [smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
x : ℂ
⊢ ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
        (((↑ℝ :
                  {S M : Type} →
                    {M₂ : Type u_1} →
                      [inst : Semiring ℝ] →
                        [inst_3 : Semiring S] →
                          [inst_4 : AddCommMonoid M] →
                            [inst_5 : AddCommMonoid M₂] →
                              [inst_6 : Module ℝ M] →
                                [inst_7 : Module ℝ M₂] →
                                  [inst_8 : Module S M] →
                                    [inst_9 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                (↑map : ℂ →ₗ[ℂ] E) :
              (a : ℂ) → E)
            x :
          E)‖ =
    ‖x‖
have this : x = HSMul.hSMul (β := ℂ) x 1
Tactic: have : x = x • (1 : ℂ) := by rw [smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
x : ℂ
this : x = HSMul.hSMul (β := ℂ) x 1
⊢ ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
        (((↑ℝ :
                  {S M : Type} →
                    {M₂ : Type u_1} →
                      [inst : Semiring ℝ] →
                        [inst_3 : Semiring S] →
                          [inst_4 : AddCommMonoid M] →
                            [inst_5 : AddCommMonoid M₂] →
                              [inst_6 : Module ℝ M] →
                                [inst_7 : Module ℝ M₂] →
                                  [inst_8 : Module S M] →
                                    [inst_9 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                (↑map : ℂ →ₗ[ℂ] E) :
              (a : ℂ) → E)
            x :
          E)‖ =
    ‖x‖
have refine_1 : ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
      (((↑ℝ :
                {S M : Type} →
                  {M₂ : Type u_1} →
                    [inst : Semiring ℝ] →
                      [inst_3 : Semiring S] →
                        [inst_4 : AddCommMonoid M] →
                          [inst_5 : AddCommMonoid M₂] →
                            [inst_6 : Module ℝ M] →
                              [inst_7 : Module ℝ M₂] →
                                [inst_8 : Module S M] →
                                  [inst_9 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
              (↑map : ℂ →ₗ[ℂ] E) :
            (a : ℂ) → E)
          (HSMul.hSMul (β := ℂ) x 1) :
        E)‖ =
  ‖x‖
Tactic: nth_rw 1 [this]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
x : ℂ
this : x = HSMul.hSMul (β := ℂ) x 1
⊢ ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
        (((↑ℝ :
                  {S M : Type} →
                    {M₂ : Type u_1} →
                      [inst : Semiring ℝ] →
                        [inst_3 : Semiring S] →
                          [inst_4 : AddCommMonoid M] →
                            [inst_5 : AddCommMonoid M₂] →
                              [inst_6 : Module ℝ M] →
                                [inst_7 : Module ℝ M₂] →
                                  [inst_8 : Module S M] →
                                    [inst_9 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                (↑map : ℂ →ₗ[ℂ] E) :
              (a : ℂ) → E)
            (HSMul.hSMul (β := ℂ) x 1) :
          E)‖ =
    ‖x‖
have refine_1 : ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
      (((↑map : ℂ →ₗ[ℂ] E) : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) x 1) : E)‖ =
  ‖x‖
Tactic: rw [LinearMap.coe_restrictScalars]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
x : ℂ
this : x = HSMul.hSMul (β := ℂ) x 1
⊢ ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
        (((↑map : ℂ →ₗ[ℂ] E) : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) x 1) : E)‖ =
    ‖x‖
have refine_1 : (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹ * (‖x‖ * norm (E := E) ((map : (a : ℂ) → E) 1 : E)) = ‖x‖
Tactic: simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
minor₁ : norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0
⊢ restrictScalars ℝ map =
    norm (E := E) ((map : (a : ℂ) → E) 1 : E) •
      {
          toLinearMap :=
            HSMul.hSMul (β := ℂ →ₗ[ℝ] E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
              ((↑ℝ :
                  {S M : Type} →
                    {M₂ : Type u_1} →
                      [inst : Semiring ℝ] →
                        [inst_3 : Semiring S] →
                          [inst_4 : AddCommMonoid M] →
                            [inst_5 : AddCommMonoid M₂] →
                              [inst_6 : Module ℝ M] →
                                [inst_7 : Module ℝ M₂] →
                                  [inst_8 : Module S M] →
                                    [inst_9 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                (↑map : ℂ →ₗ[ℂ] E)),
          norm_map' := ⋯ : ℂ →ₗᵢ[ℝ] E }.toContinuousLinearMap
have refine_2 : ∀ (x : ℂ),
  Eq (α := E) ((restrictScalars ℝ map : (a : ℂ) → E) x : E)
    ((norm (E := E) ((map : (a : ℂ) → E) 1 : E) •
            {
                toLinearMap :=
                  HSMul.hSMul (β := ℂ →ₗ[ℝ] E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
                    ((↑ℝ :
                        {S M : Type} →
                          {M₂ : Type u_1} →
                            [inst : Semiring ℝ] →
                              [inst_3 : Semiring S] →
                                [inst_4 : AddCommMonoid M] →
                                  [inst_5 : AddCommMonoid M₂] →
                                    [inst_6 : Module ℝ M] →
                                      [inst_7 : Module ℝ M₂] →
                                        [inst_8 : Module S M] →
                                          [inst_9 : Module S M₂] →
                                            [LinearMap.CompatibleSMul M M₂ ℝ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℝ] M₂)
                      (↑map : ℂ →ₗ[ℂ] E)),
                norm_map' := sorry : ℂ →ₗᵢ[ℝ] E }.toContinuousLinearMap :
          (a : ℂ) → E)
        x :
      E)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
g : ℂ →L[ℝ] ℂ
h : IsConformalMap g
⊢ (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
    ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
have rcases : ∀ (c : ℝ) (li : ℂ →ₗᵢ[ℝ] ℂ),
  (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toContinuousLinearMap) ∨
    ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = (c • li.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
Tactic: rcases h with ⟨c, -, li, rfl⟩
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (li.toLinearIsometryEquiv ⋯).toLinearIsometry = li
have h : ∀ (x : ℂ), Eq (α := ℂ) (((li.toLinearIsometryEquiv sorry).toLinearIsometry : (a : ℂ) → ℂ) x : ℂ) ((li : (a : ℂ) → ℂ) x : ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toContinuousLinearMap) ∨
    ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = (c • li.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
have obtain : ∀ (li : ℂ ≃ₗᵢ[ℝ] ℂ),
  (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
Tactic: obtain ⟨li, rfl⟩ : ∃ li' : ℂ ≃ₗᵢ[ℝ] ℂ, li'.toLinearIsometry = li :=
    ⟨li.toLinearIsometryEquiv rfl, by ext1; rfl⟩
Cleared hypotheses: li
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
have inl : ∀ (a : Circle),
  (∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
          (LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) ∘SL
          (↑conjCLE : ℂ →L[ℝ] ℂ)
Tactic: rcases linear_isometry_complex li with ⟨a, rfl | rfl⟩
Cleared hypotheses: li
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
inl :
  ∀ (a : Circle),
    (∃ (map : ℂ →L[ℂ] ℂ),
        restrictScalars ℝ map =
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∨
      ∃ (map : ℂ →L[ℂ] ℂ),
        restrictScalars ℝ map =
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
              (LinearIsometry.toContinuousLinearMap
                (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) ∘SL
            (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
have inr : ∀ (a : Circle),
  (∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
          (LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry (conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))))) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry (conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∘SL
          (↑conjCLE : ℂ →L[ℝ] ℂ)
Tactic: rcases linear_isometry_complex li with ⟨a, rfl | rfl⟩
Cleared hypotheses: li
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
c : ℝ
a : Circle
⊢ (∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
          (LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) ∘SL
          (↑conjCLE : ℂ →L[ℝ] ℂ)
have inl : restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) =
  HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
    (LinearIsometry.toContinuousLinearMap
      (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))
Tactic: refine Or.inl ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
c : ℝ
a : Circle
⊢ restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) =
    HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
      (LinearIsometry.toContinuousLinearMap
        (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))
have inl : ∀ (x : ℂ),
  Eq (α := ℂ)
    ((restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) : (a : ℂ) → ℂ) x : ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) :
          (a : ℂ) → ℂ)
        x :
      ℂ)
Tactic: ext1