awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
h : Eq (α := Circle) ((exp : (a : ℝ) → Circle) Real.pi : Circle) (1 : Circle)
heq : Eq (α := ℂ) (↑((exp : (a : ℝ) → Circle) Real.pi) : ℂ) 1
⊢ Eq (α := ℂ) (-1) 1

Tactic:
rw [Circle.coe_exp, exp_pi_mul_I] at heq

Premises used: Complex.exp_pi_mul_I, Circle.coe_exp
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
h : Eq (α := Circle) ((exp : (a : ℝ) → Circle) Real.pi : Circle) (1 : Circle)
heq : Eq (α := ℂ) (-1) 1
⊢ False

Tactic:
norm_num at heq
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
e : AddChar ℝ Circle
x : ℝ
refine_2 :
  ∀
    (h :
      (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                (↑((e : (a : ℝ) → Circle) x) : ℂ) ⋯)⁻¹ :
          ℂ) =
        (starRingEnd ℂ : (a : ℂ) → ℂ)
          (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
                (↑((e : (a : ℝ) → Circle) x) : ℂ) ⋯) :
            ℂ)),
    Eq (α := ℂ) (star (↑((e : (a : ℝ) → Circle) x) : ℂ)) (↑((e : (a : ℝ) → Circle) (-x)) : ℂ)
refine_1 : Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) (↑((e : (a : ℝ) → Circle) x) : ℂ)
⊢ Eq (α := ℂ) (star (↑((e : (a : ℝ) → Circle) x) : ℂ)) (↑((e : (a : ℝ) → Circle) (-x)) : ℂ)

Tactic:
have h := Circle.coe_inv_eq_conj ⟨e x, ?_⟩
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
e : AddChar ℝ Circle
x : ℝ
h :
  (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
            (↑((e : (a : ℝ) → Circle) x) : ℂ) ⋯)⁻¹ :
      ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ)
      (↑(Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x)
            (↑((e : (a : ℝ) → Circle) x) : ℂ) ⋯) :
        ℂ)
⊢ Eq (α := ℂ) (star (↑((e : (a : ℝ) → Circle) x) : ℂ)) (↑((e : (a : ℝ) → Circle) (-x)) : ℂ)

Tactic:
simp [← h, e.map_neg_eq_inv]

Premises used: AddChar.map_neg_eq_inv
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
e : AddChar ℝ Circle
x : ℝ
⊢ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) (↑((e : (a : ℝ) → Circle) x) : ℂ)

Tactic:
simp only [Submonoid.unitSphere, SetLike.coe_mem]

Premises used: SetLike.coe_mem, Submonoid.unitSphere
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
e : AddChar ℝ Circle
x : ℝ
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑((e : (a : ℝ) → Circle) x) : ℂ) : ℂ)
    ((↑((e : (a : ℝ) → Circle) (-x)) : ℂ) : ℂ)

Tactic:
star_addChar x

Premises used: Circle.star_addChar
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
e : AddChar ℝ Circle
α : Type u_1
β : Type u_2
M : Type u_3
inst : SMul ℂ β
inst_1 : SMul α β
inst_2 : SMulCommClass ℂ α β
⊢ SMulCommClass Circle α β

Tactic:
inferInstanceAs <| SMulCommClass (Submonoid.unitSphere _) α β

Premises used: _private.0.Circle.instSMulCommClass_left._proof_1
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
e : AddChar ℝ Circle
α : Type u_1
β : Type u_2
M : Type u_3
inst : SMul ℂ β
inst_1 : SMul α β
inst_2 : SMulCommClass α ℂ β
⊢ SMulCommClass α Circle β

Tactic:
inferInstanceAs <| SMulCommClass α (Submonoid.unitSphere _) β

Premises used: _private.0.Circle.instSMulCommClass_right._proof_1
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
e : AddChar ℝ Circle
α : Type u_1
β : Type u_2
M : Type u_3
inst : SMul ℂ α
inst_1 : SMul ℂ β
inst_2 : SMul α β
inst_3 : IsScalarTower ℂ α β
⊢ IsScalarTower Circle α β

Tactic:
inferInstanceAs <| IsScalarTower (Submonoid.unitSphere _) α β

Premises used: _private.0.Circle.instIsScalarTower._proof_1
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
α : Type u_1
inst : SMul ℂ α
z : Circle
a : α
⊢ z • a = (↑z : ℂ) • a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x y : Circle
e : AddChar ℝ Circle
α : Type u_1
β : Type u_2
M : Type u_3
inst : TopologicalSpace α
inst_1 : MulAction ℂ α
inst_2 : ContinuousSMul ℂ α
⊢ ContinuousSMul Circle α

Tactic:
inferInstanceAs <| ContinuousSMul (Submonoid.unitSphere _) α

Premises used: _private.0.Circle.instContinuousSMul._proof_1
-- Module: Mathlib.Analysis.Complex.Circle
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‖
rw₃ rw₄ : ‖v‖ = ‖v‖
⊢ ‖u • v‖ = ‖v‖

Tactic:
rw [smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]

Premises used: norm_eq_of_mem_sphere, norm_smul, Circle.smul_def, one_mul
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
rw : Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) 0) 1
rw₁ rw₂ : Eq (α := Circle) 1 1
⊢ Eq (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * 0) : Circle) (1 : Circle)

Tactic:
rw [mul_zero, Circle.exp_zero]

Premises used: MulZeroClass.mul_zero, Circle.exp_zero
-- Module: Mathlib.Analysis.Complex.Circle
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)
rw₁ 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)
⊢ (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)

Tactic:
rw [mul_add, Circle.exp_add]

Premises used: Circle.exp_add, mul_add
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
⊢ Eq (α := Circle) ((𝐞 : (a : ℝ) → Circle) x : Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * x) : Circle)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
⊢ (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ) = cexp ((↑(2 * π * x) : ℂ) * I)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
⊢ Continuous (X := ℝ) (Y := Circle) (⇑𝐞 : (a : ℝ) → Circle)

Tactic:
Circle.exp.continuous.comp (continuous_const_mul _)

Premises used: ContinuousMap.continuous, Continuous.comp, continuous_const_mul, Circle.exp
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
rw : ∃ (a : ℝ), Ne (α := Circle) ((𝐞 : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
⊢ 𝐞 ≠ 1

Tactic:
rw [DFunLike.ne_iff]

Premises used: DFunLike.ne_iff
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
h : Ne (α := Circle) ((𝐞 : (a : ℝ) → Circle) 2⁻¹) ((1 : (a : ℝ) → Circle) 2⁻¹)
⊢ ∃ (a : ℝ), Ne (α := Circle) ((𝐞 : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)

Tactic:
use 2⁻¹
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
⊢ Ne (α := ℝ) 2 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
h : Ne (α := Circle) ((Circle.exp : (a : ℝ) → Circle) π : Circle) (1 : Circle)
⊢ Ne (α := Circle) ((Circle.exp : (a : ℝ) → Circle) (2 * π * 2⁻¹) : Circle) (1 : Circle)

Tactic:
rw [mul_comm, ← mul_assoc, inv_mul_cancel₀ (by positivity), one_mul]

Premises used: mul_assoc, mul_comm, inv_mul_cancel₀, one_mul
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
⊢ Ne (α := Circle) ((Circle.exp : (a : ℝ) → Circle) π : Circle) (1 : Circle)

Tactic:
Circle.exp_pi_ne_one

Premises used: Circle.exp_pi_ne_one
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
⊢ Ne (α := Circle) ((Circle.exp : (a : ℝ) → Circle) π : Circle) (1 : Circle)

Tactic:
exact Circle.exp_pi_ne_one

Premises used: Circle.exp_pi_ne_one
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
⊢ Eq (α := Circle) ((probChar : (a : ℝ) → Circle) x : Circle) ((Circle.exp : (a : ℝ) → Circle) x : Circle)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
x : ℝ
⊢ (↑((probChar : (a : ℝ) → Circle) x) : ℂ) = cexp ((↑x : ℂ) * I)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
⊢ Continuous (X := ℝ) (Y := Circle) (⇑probChar : (a : ℝ) → Circle)

Tactic:
map_continuous Circle.exp

Premises used: Circle.exp, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
rw : ∃ (a : ℝ), Ne (α := Circle) ((probChar : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
⊢ probChar ≠ 1

Tactic:
rw [DFunLike.ne_iff]

Premises used: DFunLike.ne_iff
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
h : Ne (α := Circle) ((probChar : (a : ℝ) → Circle) π : Circle) ((1 : (a : ℝ) → Circle) π : Circle)
⊢ ∃ (a : ℝ), Ne (α := Circle) ((probChar : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)

Tactic:
use Real.pi

Premises used: Real.pi
-- Module: Mathlib.Analysis.Complex.Circle
Goal:
⊢ Ne (α := Circle) ((probChar : (a : ℝ) → Circle) π : Circle) ((1 : (a : ℝ) → Circle) π : Circle)

Tactic:
simpa only [probChar_apply'] using Circle.exp_pi_ne_one

Premises used: Circle.exp_pi_ne_one, Real.probChar_apply'
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
⊢ IsConformalMap (↑(↑conjLIE : ℂ ≃L[ℝ] ℂ) : ℂ →L[ℝ] ℂ)

Tactic:
conjLIE.toLinearIsometry.isConformalMap

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.isConformalMap, Complex.conjLIE, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ norm (E := E) ((map : (a : ℂ) → E) 1 : E) ≠ 0

Tactic:
simpa only [ContinuousLinearMap.ext_ring_iff, Ne, norm_eq_zero] using nonzero

Premises used: norm_eq_zero, Ne, ContinuousLinearMap.ext_ring_iff
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedSpace ℂ E
map : ℂ →L[ℂ] E
nonzero : map ≠ 0
⊢ 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
-- Module: Mathlib.Analysis.Complex.Conformal
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)

Tactic:
⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), ?_⟩, ?_⟩

Premises used: Norm.norm, Real, LinearMap.restrictScalars, LinearIsometry.mk, ContinuousLinearMap.toLinearMap, Inv.inv, And.intro, Exists.intro, HSMul.hSMul, IsConformalMap, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.Conformal
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‖
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' := ⋯ : ℂ →ₗᵢ[ℝ] E }.toContinuousLinearMap
⊢ IsConformalMap.{0, 0, u_1} (R := ℝ) (X := ℂ) (Y := E) (restrictScalars ℝ map)

Tactic:
refine ⟨‖map 1‖, minor₁, ⟨‖map 1‖⁻¹ • ((map : ℂ →ₗ[ℂ] E) : ℂ →ₗ[ℝ] E), ?_⟩, ?_⟩
-- Module: Mathlib.Analysis.Complex.Conformal
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 : ℂ
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‖
⊢ 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:
simp only [LinearMap.smul_apply]

Premises used: LinearMap.smul_apply
-- Module: Mathlib.Analysis.Complex.Conformal
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
rw₁ rw₂ : x = x
⊢ x = HSMul.hSMul (β := ℂ) x 1

Tactic:
rw [smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one
-- Module: Mathlib.Analysis.Complex.Conformal
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

Tactic:
have : x = x • (1 : ℂ) := by rw [smul_eq_mul, mul_one]
-- Module: Mathlib.Analysis.Complex.Conformal
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
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‖
⊢ ‖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:
nth_rw 1 [this]
-- Module: Mathlib.Analysis.Complex.Conformal
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
refine_1 :
  ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
        (((↑map : ℂ →ₗ[ℂ] E) : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) x 1) : E)‖ =
    ‖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)
            (HSMul.hSMul (β := ℂ) x 1) :
          E)‖ =
    ‖x‖

Tactic:
rw [LinearMap.coe_restrictScalars]

Premises used: LinearMap.coe_restrictScalars
-- Module: Mathlib.Analysis.Complex.Conformal
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
refine_1 : (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹ * (‖x‖ * norm (E := E) ((map : (a : ℂ) → E) 1 : E)) = ‖x‖
⊢ ‖HSMul.hSMul (β := E) (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹
        (((↑map : ℂ →ₗ[ℂ] E) : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) x 1) : E)‖ =
    ‖x‖

Tactic:
simp only [map.coe_coe, map.map_smul, norm_smul, norm_inv, norm_norm]

Premises used: norm_smul, ContinuousLinearMap.coe_coe, norm_norm, norm_inv, ContinuousLinearMap.map_smul
-- Module: Mathlib.Analysis.Complex.Conformal
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
⊢ (norm (E := E) ((map : (a : ℂ) → E) 1 : E))⁻¹ * (‖x‖ * norm (E := E) ((map : (a : ℂ) → E) 1 : E)) = ‖x‖

Tactic:
field
-- Module: Mathlib.Analysis.Complex.Conformal
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_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' := ⋯ : ℂ →ₗᵢ[ℝ] E }.toContinuousLinearMap :
            (a : ℂ) → E)
          x :
        E)
⊢ 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

Tactic:
ext1
-- Module: Mathlib.Analysis.Complex.Conformal
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 : ℂ
⊢ 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' := ⋯ : ℂ →ₗᵢ[ℝ] E }.toContinuousLinearMap :
          (a : ℂ) → E)
        x :
      E)

Tactic:
simp [minor₁]
-- Module: Mathlib.Analysis.Complex.Conformal
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 ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))

Tactic:
(isConformalMap_complex_linear nonzero).comp isConformalMap_conj

Premises used: isConformalMap_conj, IsConformalMap.comp, isConformalMap_complex_linear