awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : AddCommMonoid E
inst_2 : Module K E
inst_3 : Module ℝ E
inst_4 : IsScalarTower ℝ K E
s : Set E
⊢ Convex K s ↔ Convex ℝ s

Tactic:
⟨Convex.lift ℝ,
  fun hs => convex_of_nonneg_surjective_algebraMap _ (fun _ => nonneg_iff_exists_ofReal.mp) hs⟩

Premises used: Real, RCLike.nonneg_iff_exists_ofReal, Iff.intro, Iff.mp, convex_of_nonneg_surjective_algebraMap, Convex.lift
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
p : ℝ[X]
x : ℝ
⊢ Eq.{u_1 + 1} (α := K) ((↑(eval x p) : K) : K) ((aeval (↑x : K) : (a : ℝ[X]) → K) p : K)

Tactic:
(@aeval_algebraMap_apply_eq_algebraMap_eval ℝ K _ _ _ x p).symm

Premises used: Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, Eq.symm
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
this : ∀ (x : K), ∃ (a : ℝ) (b : ℝ), HSMul.hSMul (β := K) a 1 + HSMul.hSMul (β := K) b I = x
⊢ Eq (α := Submodule ℝ K) (Submodule.span ℝ {1, I}) ⊤

Tactic:
simpa [Submodule.eq_top_iff', Submodule.mem_span_pair]

Premises used: Submodule.eq_top_iff', Submodule.mem_span_pair
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
suffices : ∀ (x : K), ∃ (a : ℝ) (b : ℝ), HSMul.hSMul (β := K) a 1 + HSMul.hSMul (β := K) b I = x
⊢ Eq (α := Submodule ℝ K) (Submodule.span ℝ {1, I}) ⊤

Tactic:
suffices ∀ x : K, ∃ a b : ℝ, a • 1 + b • I = x by
    simpa [Submodule.eq_top_iff', Submodule.mem_span_pair]
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ HSMul.hSMul (α := ℝ) (β := K) ((re : (a : K) → ℝ) x : ℝ) 1 +
      HSMul.hSMul (α := ℝ) (β := K) ((im : (a : K) → ℝ) x : ℝ) I =
    x

Tactic:
simp [real_smul_eq_coe_mul]

Premises used: RCLike.real_smul_eq_coe_mul
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
⊢ ∀ (x : K), ∃ (a : ℝ) (b : ℝ), HSMul.hSMul (β := K) a 1 + HSMul.hSMul (β := K) b I = x

Tactic:
exact fun x ↦ ⟨re x, im x, by simp [real_smul_eq_coe_mul]⟩
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
rw : Module.rank ℝ K = Module.rank ℝ ↥⊤
⊢ Module.rank ℝ K = Module.rank ℝ ↥(Submodule.span ℝ {1, I})

Tactic:
rw [span_one_I]

Premises used: RCLike.span_one_I
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
⊢ Module.rank ℝ K = Module.rank ℝ ↥⊤

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
⊢ Module.rank ℝ ↥(Submodule.span ℝ (↑{1, I} : Set K)) ≤ (↑(Finset.card (α := K) {1, I}) : Cardinal.{u_1})

Tactic:
have := rank_span_finset_le (R := ℝ) (M := K) {1, I}
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
this : Module.rank ℝ ↥(Submodule.span ℝ (↑{1, I} : Set K)) ≤ (↑(Finset.card (α := K) {1, I}) : Cardinal.{u_1})
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ (↑(Finset.card (α := K) {1, I}) : Cardinal.{u_1})

Tactic:
rw [Finset.coe_pair] at this

Premises used: Finset.coe_pair
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
this : Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ (↑(Finset.card (α := K) {1, I}) : Cardinal.{u_1})
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ (↑(Finset.card (α := K) {1, I}) : Cardinal.{u_1})

Tactic:
simpa [span_one_I] using this

Premises used: RCLike.span_one_I
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
⊢ Module.finrank ℝ K ≤ 2

Tactic:
Module.finrank_le_of_rank_le <| rank_le_two _

Premises used: RCLike.rank_le_two, Module.finrank_le_of_rank_le
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
⊢ Eq (α := Submodule ℝ K) (Submodule.span ℝ (↑{1, I} : Set K)) ⊤

Tactic:
simp [span_one_I]

Premises used: RCLike.span_one_I
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : FiniteDimensional K E
have : ∀ (this : NormedSpace ℝ E), ProperSpace E
⊢ ProperSpace E

Tactic:
have : NormedSpace ℝ E := .restrictScalars ℝ K E
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : FiniteDimensional K E
this : NormedSpace ℝ E
⊢ FiniteDimensional ℝ E

Tactic:
have : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
inst_3 : FiniteDimensional K E
this_1 : NormedSpace ℝ E
this : FiniteDimensional ℝ E
⊢ ProperSpace E

Tactic:
infer_instance
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
S : Submodule K E
inst_3 : FiniteDimensional.{u_1, u_2} K ↥S
⊢ ProperSpace.{u_2} ↥S

Tactic:
proper_rclike K S

Premises used: FiniteDimensional.proper_rclike, Set.Mem, Membership.mem, Subtype
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
apply : 1 ≤ norm.{u_1} (E := K →L[ℝ] ℝ) (LinearMap.mkContinuous reLm 1 ⋯)
⊢ norm.{u_1} (E := StrongDual ℝ K) reCLM = 1

Tactic:
apply le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _)

Premises used: zero_le_one, le_antisymm, LinearMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
⊢ norm (E := ℝ) ((reCLM : (a : K) → ℝ) 1 : ℝ) / norm.{u_1} (E := K) 1 ≤ norm.{u_1} (E := K →L[ℝ] ℝ) reCLM

Tactic:
ContinuousLinearMap.ratio_le_opNorm (reCLM : StrongDual ℝ K) (1 : K)

Premises used: RCLike.reCLM, ContinuousLinearMap.ratio_le_opNorm, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
h : 1 = norm (E := ℝ) ((reCLM : (a : K) → ℝ) 1 : ℝ) / norm.{u_1} (E := K) 1
⊢ 1 ≤ norm.{u_1} (E := K →L[ℝ] ℝ) (LinearMap.mkContinuous reLm 1 ⋯)

Tactic:
convert! ContinuousLinearMap.ratio_le_opNorm (reCLM : StrongDual ℝ K) (1 : K)

Premises used: RCLike.reCLM, ContinuousLinearMap.ratio_le_opNorm, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
⊢ 1 = norm (E := ℝ) ((reCLM : (a : K) → ℝ) 1 : ℝ) / norm.{u_1} (E := K) 1

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
⊢ norm.{u_1} (E := K →L[ℝ] K) (↑conjCLE : K →L[ℝ] K) = 1

Tactic:
(@conjLIE K _).toLinearIsometry.norm_toContinuousLinearMap

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometry.norm_toContinuousLinearMap, RCLike.conjLIE, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
⊢ norm.{u_1} (E := ℝ →L[ℝ] K) ofRealCLM = 1

Tactic:
LinearIsometry.norm_toContinuousLinearMap _

Premises used: RCLike.ofRealCLM, LinearIsometry.norm_toContinuousLinearMap
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
p : ℝ[X]
z : K
⊢ Eq (α := K) (((aeval ((starRingEnd K : (a : K) → K) z) : ℝ[X] →ₐ[ℝ] K) : (a : ℝ[X]) → K) p : K)
    ((starRingEnd K : (a : K) → K) ((aeval z : (a : ℝ[X]) → K) p : K) : K)

Tactic:
aeval_algHom_apply (RCLike.conjAe (K := K)) z p

Premises used: RCLike.conjAe, Polynomial.aeval_algHom_apply
-- Module: Mathlib.Analysis.RCLike.Lemmas
Goal:
K : Type u_1
inst : RCLike K
p : ℝ[X]
x : ℝ
⊢ Eq.{u_1 + 1} (α := K) ((aeval (↑x : K) : (a : ℝ[X]) → K) p : K) ((↑(eval x p) : K) : K)

Tactic:
aeval_algHom_apply RCLike.ofRealAm x p

Premises used: Polynomial.eval, RCLike.ofRealAm, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.aeval_algHom_apply
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
⊢ sqrt 0 = 0

Tactic:
simp [sqrt]

Premises used: Complex.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
⊢ sqrt 1 = 1

Tactic:
simp [sqrt]

Premises used: Complex.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℂ
rw :
  HPow.hPow (β := ℂ) a 2⁻¹ =
    (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I
⊢ a.sqrt = (↑√((‖a‖ + a.re) / 2) : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I

Tactic:
rw [← cpow_inv_two_re, sqrt]

Premises used: Complex.sqrt, Complex.cpow_inv_two_re
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℂ
pos :
  ∀ (h : 0 ≤ a.im),
    HPow.hPow (β := ℂ) a 2⁻¹ =
      (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I
neg :
  ∀ (h : a.im < 0),
    HPow.hPow (β := ℂ) a 2⁻¹ =
      (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I
⊢ HPow.hPow (β := ℂ) a 2⁻¹ =
    (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I

Tactic:
by_cases! h : 0 ≤ a.im

Premises used: Complex.im
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℂ
h : 0 ≤ a.im
⊢ HPow.hPow (β := ℂ) a 2⁻¹ =
    (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I

Tactic:
simp [← cpow_inv_two_im_eq_sqrt h, h]

Premises used: Complex.cpow_inv_two_im_eq_sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℂ
h : a.im < 0
⊢ HPow.hPow (β := ℂ) a 2⁻¹ =
    (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I

Tactic:
simp only [re_add_im, ↓reduceIte, h.not_ge, neg_one_mul, ← ofReal_neg,
    ← cpow_inv_two_im_eq_neg_sqrt h]

Premises used: Complex.ofReal_neg, neg_one_mul, reduceIte, Complex.cpow_inv_two_im_eq_neg_sqrt, Complex.re_add_im, LT.lt.not_ge
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
z : ℂ
hz : z ≠ 0
⊢ z.sqrt = cexp (log z / 2)

Tactic:
simp [sqrt, cpow_def, hz, div_eq_mul_inv]

Premises used: Complex.sqrt, div_eq_mul_inv, Complex.cpow_def
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
rw :
  Eq (α := 𝕜)
    (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
        ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) a))
      else (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜) :
      𝕜)
    ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)
⊢ sqrt a =
    if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
      ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) a))
    else (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)

Tactic:
rw [sqrt, eq_comm]

Premises used: eq_comm, RCLike.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
pos :
  ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
    Eq (α := 𝕜) (((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) a)) : 𝕜)
      ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)
neg :
  ∀ (h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
    Eq (α := 𝕜) ((↑√((re : (a : 𝕜) → ℝ) a) : 𝕜) : 𝕜)
      ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)
⊢ Eq (α := 𝕜)
    (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
        ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) a))
      else (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜) :
      𝕜)
    ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ Eq (α := 𝕜) (((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) a)) : 𝕜)
    ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜) I 0

Tactic:
grind [I_eq_zero_or_im_I_eq_one]

Premises used: RCLike.I_eq_zero_or_im_I_eq_one
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜) I 0

Tactic:
have : (I : 𝕜) = 0 := by grind [I_eq_zero_or_im_I_eq_one]
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
this : Eq.{u_1 + 1} (α := 𝕜) I 0
neg :
  ∀ (h : ¬Eq (α := ℝ) 0 1) (this : Eq.{u_1 + 1} (α := 𝕜) I 0),
    √((re : (a : 𝕜) → ℝ) a) =
      √((‖(↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I‖ +
            ((↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I).re) /
          2)
⊢ Eq (α := 𝕜) ((↑√((re : (a : 𝕜) → ℝ) a) : 𝕜) : 𝕜)
    ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)

Tactic:
simp_all only [Complex.sqrt, im_eq_zero this, map_apply, add_zero, re_to_complex, im_to_complex,
    mul_zero, algebraMap.coe_inj, Complex.cpow_inv_two_re]

Premises used: RCLike.map_apply, algebraMap.coe_inj, Complex.sqrt, MulZeroClass.mul_zero, Complex.cpow_inv_two_re, RCLike.im_to_complex, add_zero, RCLike.re_to_complex, RCLike.im_eq_zero
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : ¬Eq (α := ℝ) 0 1
this : Eq.{u_1 + 1} (α := 𝕜) I 0
pos :
  ∀ (ha' : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) a : ℝ)),
    √((re : (a : 𝕜) → ℝ) a) =
      √((‖(↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I‖ +
            ((↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I).re) /
          2)
neg :
  ∀ (ha' : LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) a : ℝ) (0 : ℝ)),
    √((re : (a : 𝕜) → ℝ) a) =
      √((‖(↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I‖ +
            ((↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I).re) /
          2)
⊢ √((re : (a : 𝕜) → ℝ) a) =
    √((‖(↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I‖ +
          ((↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I).re) /
        2)

Tactic:
by_cases! ha' : 0 ≤ re a

Premises used: RCLike.re, DFunLike.coe
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : ¬Eq (α := ℝ) 0 1
this : Eq.{u_1 + 1} (α := 𝕜) I 0
ha' : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) a : ℝ)
⊢ √((re : (a : 𝕜) → ℝ) a) =
    √((‖(↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I‖ +
          ((↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I).re) /
        2)

Tactic:
simp [abs_of_nonneg ha', ← two_mul]

Premises used: two_mul, abs_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : ¬Eq (α := ℝ) 0 1
this : Eq.{u_1 + 1} (α := 𝕜) I 0
ha' : LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) a : ℝ) (0 : ℝ)
⊢ √((re : (a : 𝕜) → ℝ) a) =
    √((‖(↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I‖ +
          ((↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I).re) /
        2)

Tactic:
simp [abs_of_nonpos ha'.le, Real.sqrt_eq_zero', ha'.le]

Premises used: LT.lt.le, abs_of_nonpos, Real.sqrt_eq_zero'
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
rw :
  (map ℂ 𝕜 : (a : ℂ) → 𝕜)
      ((↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) + Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) +
        (if 0 ≤ Complex.im ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a) then 1 else -1) *
            (↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) - Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) *
          Complex.I) =
    (↑√(HAdd.hAdd (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) +
      HMul.hMul (α := 𝕜) (if LE.le (α := ℝ) (0 : ℝ) ((im : (a : 𝕜) → ℝ) a : ℝ) then 1 else -1)
          (↑√(HSub.hSub (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) *
        I
⊢ sqrt a =
    (↑√(HAdd.hAdd (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) +
      HMul.hMul (α := 𝕜) (if LE.le (α := ℝ) (0 : ℝ) ((im : (a : 𝕜) → ℝ) a : ℝ) then 1 else -1)
          (↑√(HSub.hSub (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) *
        I

Tactic:
rw [sqrt, Complex.sqrt_eq_real_add_ite]

Premises used: Complex.sqrt_eq_real_add_ite, RCLike.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
inl :
  ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0),
    (map ℂ 𝕜 : (a : ℂ) → 𝕜)
        ((↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) + Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) +
          (if 0 ≤ Complex.im ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a) then 1 else -1) *
              (↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) - Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) *
            Complex.I) =
      (↑√(HAdd.hAdd (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) +
        HMul.hMul (α := 𝕜) (if LE.le (α := ℝ) (0 : ℝ) ((im : (a : 𝕜) → ℝ) a : ℝ) then 1 else -1)
            (↑√(HSub.hSub (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) *
          I
inr :
  ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
    (map ℂ 𝕜 : (a : ℂ) → 𝕜)
        ((↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) + Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) +
          (if 0 ≤ Complex.im ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a) then 1 else -1) *
              (↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) - Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) *
            Complex.I) =
      (↑√(HAdd.hAdd (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) +
        HMul.hMul (α := 𝕜) (if LE.le (α := ℝ) (0 : ℝ) ((im : (a : 𝕜) → ℝ) a : ℝ) then 1 else -1)
            (↑√(HSub.hSub (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) *
          I
⊢ (map ℂ 𝕜 : (a : ℂ) → 𝕜)
      ((↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) + Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) +
        (if 0 ≤ Complex.im ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a) then 1 else -1) *
            (↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) - Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) *
          Complex.I) =
    (↑√(HAdd.hAdd (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) +
      HMul.hMul (α := 𝕜) (if LE.le (α := ℝ) (0 : ℝ) ((im : (a : 𝕜) → ℝ) a : ℝ) then 1 else -1)
          (↑√(HSub.hSub (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) *
        I

Tactic:
obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)

Premises used: RCLike.I_eq_zero_or_im_I_eq_one
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : Eq.{u_1 + 1} (α := 𝕜) I 0
inl :
  (map ℂ 𝕜 : (a : ℂ) → 𝕜)
      ((↑√((norm (E := ℂ)
                    ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                        ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                      ℂ) +
                  Complex.re
                    ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                      ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I))) /
                2) :
          ℂ) +
        (if
                0 ≤
                  Complex.im
                    ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                      ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I)) then
              1
            else -1) *
            (↑√((norm (E := ℂ)
                        ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                            ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                          ℂ) -
                      Complex.re
                        ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                          ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I))) /
                    2) :
              ℂ) *
          Complex.I) =
    (↑√(HAdd.hAdd (β := ℝ) ‖(↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I‖
                ((re : (a : 𝕜) → ℝ)
                    ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                  ℝ) /
              2) :
        𝕜) +
      HMul.hMul (α := 𝕜)
          (if
              LE.le (α := ℝ) (0 : ℝ)
                ((im : (a : 𝕜) → ℝ)
                    ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                  ℝ) then
            1
          else -1)
          (↑√(HSub.hSub (β := ℝ) ‖(↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I‖
                    ((re : (a : 𝕜) → ℝ)
                        ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                      ℝ) /
                  2) :
            𝕜) *
        I
⊢ (map ℂ 𝕜 : (a : ℂ) → 𝕜)
      ((↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) + Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) +
        (if 0 ≤ Complex.im ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a) then 1 else -1) *
            (↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) - Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) *
          Complex.I) =
    (↑√(HAdd.hAdd (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) +
      HMul.hMul (α := 𝕜) (if LE.le (α := ℝ) (0 : ℝ) ((im : (a : 𝕜) → ℝ) a : ℝ) then 1 else -1)
          (↑√(HSub.hSub (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) *
        I

Tactic:
rw [← re_add_im a]

Premises used: RCLike.re_add_im
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : Eq.{u_1 + 1} (α := 𝕜) I 0
⊢ (map ℂ 𝕜 : (a : ℂ) → 𝕜)
      ((↑√((norm (E := ℂ)
                    ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                        ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                      ℂ) +
                  Complex.re
                    ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                      ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I))) /
                2) :
          ℂ) +
        (if
                0 ≤
                  Complex.im
                    ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                      ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I)) then
              1
            else -1) *
            (↑√((norm (E := ℂ)
                        ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                            ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                          ℂ) -
                      Complex.re
                        ((map 𝕜 ℂ : (a : 𝕜) → ℂ)
                          ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I))) /
                    2) :
              ℂ) *
          Complex.I) =
    (↑√(HAdd.hAdd (β := ℝ) ‖(↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I‖
                ((re : (a : 𝕜) → ℝ)
                    ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                  ℝ) /
              2) :
        𝕜) +
      HMul.hMul (α := 𝕜)
          (if
              LE.le (α := ℝ) (0 : ℝ)
                ((im : (a : 𝕜) → ℝ)
                    ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                  ℝ) then
            1
          else -1)
          (↑√(HSub.hSub (β := ℝ) ‖(↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I‖
                    ((re : (a : 𝕜) → ℝ)
                        ((↑((re : (a : 𝕜) → ℝ) a) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) a) : 𝕜) I) :
                      ℝ) /
                  2) :
            𝕜) *
        I

Tactic:
simp [h, im_eq_zero]

Premises used: RCLike.im_eq_zero
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ (map ℂ 𝕜 : (a : ℂ) → 𝕜)
      ((↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) + Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) +
        (if 0 ≤ Complex.im ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a) then 1 else -1) *
            (↑√((norm (E := ℂ) ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a : ℂ) - Complex.re ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) / 2) : ℂ) *
          Complex.I) =
    (↑√(HAdd.hAdd (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) +
      HMul.hMul (α := 𝕜) (if LE.le (α := ℝ) (0 : ℝ) ((im : (a : 𝕜) → ℝ) a : ℝ) then 1 else -1)
          (↑√(HSub.hSub (β := ℝ) ‖a‖ ((re : (a : 𝕜) → ℝ) a : ℝ) / 2) : 𝕜) *
        I

Tactic:
aesop
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (sqrt 0) 0

Tactic:
simp [sqrt]

Premises used: RCLike.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (sqrt 1) 1

Tactic:
simp [sqrt]

Premises used: RCLike.sqrt