awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
𝕝 : Type u_5
inst_4 : CommSemiring 𝕝
inst_5 : StarRing 𝕝
inst_6 : Algebra 𝕝 𝕜
inst_7 : StarModule 𝕝 𝕜
inst_8 : (i : ι) → Module.{u_5, u_4} 𝕝 (E i)
inst_9 : ∀ (i : ι), IsScalarTower.{u_5, u_3, u_4} 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
simp_rw : ∑ i : ι, w i • ⟪f i, (c • g) i⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₁ : ∑ x : ι, w x • ⟪f x, c • g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
simp_rw₂ : ∑ x : ι, w x • c • ⟪f x, g x⟫_𝕜 = HSMul.hSMul (β := 𝕜) c (∑ i : ι, w i • ⟪f i, g i⟫_𝕜)
⊢ wInner (E := E) w f (c • g) = HSMul.hSMul (β := 𝕜) c (wInner (E := E) w f g)
have simp_rw₃ : Eq.{u_3 + 1} (α := 𝕜) (∑ x : ι, w x • c • ⟪f x, g x⟫_𝕜) (∑ x : ι, c • w x • ⟪f x, g x⟫_𝕜)
Tactic: simp_rw [wInner, Pi.smul_apply, inner_smul_right_eq_smul, smul_sum, smul_comm c]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
c : 𝕜
w : ι → ℝ
f g : (i : ι) → E i
⊢ c * wInner (E := E) w f g = wInner (E := E) w (star c • f) g
have rw : c * wInner (E := E) w f g = HSMul.hSMul (β := 𝕜) (star (star c)) (wInner (E := E) w f g)
Tactic: rw [wInner_smul_left, star_star, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
c : 𝕜
w : ι → ℝ
f g : (i : ι) → E i
rw : c * wInner (E := E) w f g = HSMul.hSMul (β := 𝕜) (star (star c)) (wInner (E := E) w f g)
⊢ c * wInner (E := E) w f g = wInner (E := E) w (star c • f) g
have rw₁ : c * wInner (E := E) w f g = HSMul.hSMul (β := 𝕜) c (wInner (E := E) w f g)
Tactic: rw [wInner_smul_left, star_star, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst : Fintype ι
inst_1 : RCLike 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → InnerProductSpace.{u_3, u_4} 𝕜 (E i)
c : 𝕜
w : ι → ℝ
f g : (i : ι) → E i
rw : c * wInner (E := E) w f g = HSMul.hSMul (β := 𝕜) (star (star c)) (wInner (E := E) w f g)
rw₁ : c * wInner (E := E) w f g = HSMul.hSMul (β := 𝕜) c (wInner (E := E) w f g)
⊢ c * wInner (E := E) w f g = wInner (E := E) w (star c • f) g
have rw₂ : c * wInner (E := E) w f g = c * wInner (E := E) w f g
Tactic: rw [wInner_smul_left, star_star, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) 1 (f k₁) (f k₂)) 0
⊢ LinearIndependent 𝕜 f
have hinner₁ : Pairwise fun (k₁ k₂ : κ) ↦ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 (f k₁)) (toLp 2 (f k₂)) = 0
Tactic: simp_rw [wInner_one_eq_inner] at hinner
Cleared hypotheses: hinner
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 (f k₁)) (toLp 2 (f k₂)) = 0
⊢ LinearIndependent 𝕜 f
have refine_2 : ∀ (this : LinearIndependent 𝕜 (M := WithLp 2 (ι → 𝕜)) fun (i : κ) ↦ toLp 2 (f i)), LinearIndependent 𝕜 f
Tactic: have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ hinner
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ inner 𝕜 (E := WithLp 2 (ι → 𝕜)) (toLp 2 (f k₁)) (toLp 2 (f k₂)) = 0
refine_2 : ∀ (this : LinearIndependent 𝕜 (M := WithLp 2 (ι → 𝕜)) fun (i : κ) ↦ toLp 2 (f i)), LinearIndependent 𝕜 f
⊢ LinearIndependent 𝕜 f
have refine_1 : ∀ (i : κ), Ne (α := WithLp 2 (ι → 𝕜)) (toLp 2 (f i)) 0
Tactic: have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ hinner
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
⊢ LinearIndependent 𝕜 f
have inl : IsEmpty ι → LinearIndependent 𝕜 f
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (goal)
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
inl : IsEmpty ι → LinearIndependent 𝕜 f
⊢ LinearIndependent 𝕜 f
have inr : Nonempty ι → LinearIndependent 𝕜 f
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Inner (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst : Fintype ι
inst_1 : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun (k₁ k₂ : κ) ↦ Eq (α := 𝕜) (wInner (E := fun (i : ι) ↦ 𝕜) cWeight (f k₁) (f k₂)) 0
h : IsEmpty ι
⊢ LinearIndependent 𝕜 f
have this : IsEmpty κ
Tactic: have : IsEmpty κ := ⟨fun k ↦ hf k <| Subsingleton.elim ..⟩
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Lemmas (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := Submodule ℝ K) (Submodule.span ℝ {1, I}) ⊤
have suffices : ∀ (x : K), ∃ (a : ℝ) (b : ℝ), HSMul.hSMul (β := K) a 1 + HSMul.hSMul (β := K) b I = x
Tactic: suffices ∀ x : K, ∃ a b : ℝ, a • 1 + b • I = x by
    simpa [Submodule.eq_top_iff', Submodule.mem_span_pair]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Lemmas (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ Module.rank ℝ K = Module.rank ℝ ↥(Submodule.span ℝ {1, I})
have rw : Module.rank ℝ K = Module.rank ℝ ↥⊤
Tactic: rw [span_one_I]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Lemmas (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
⊢ Module.rank ℝ ↥(Submodule.span ℝ {1, I}) ≤ (↑(Finset.card (α := K) {1, I}) : Cardinal.{u_1})
have this : 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}
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Lemmas (goal)
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
⊢ ProperSpace E
have have : ∀ (this : NormedSpace ℝ E), ProperSpace E
Tactic: have : NormedSpace ℝ E := .restrictScalars ℝ K E
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Lemmas (hypothesis)
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
⊢ ProperSpace E
have this₁ : FiniteDimensional ℝ E
Tactic: have : FiniteDimensional ℝ E := FiniteDimensional.trans ℝ K E
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Lemmas (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ norm.{u_1} (E := StrongDual ℝ K) reCLM = 1
have apply : 1 ≤ norm.{u_1} (E := K →L[ℝ] ℝ) (LinearMap.mkContinuous reLm 1 sorry)
Tactic: apply le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Lemmas (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ 1 ≤ norm.{u_1} (E := K →L[ℝ] ℝ) (LinearMap.mkContinuous reLm 1 ⋯)
have h : 1 = norm (E := ℝ) ((reCLM : (a : K) → ℝ) 1 : ℝ) / norm.{u_1} (E := K) 1
Tactic: convert! ContinuousLinearMap.ratio_le_opNorm (reCLM : StrongDual ℝ K) (1 : K)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
a : ℂ
⊢ a.sqrt = (↑√((‖a‖ + a.re) / 2) : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I
have rw : HPow.hPow (β := ℂ) a 2⁻¹ =
  (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I
Tactic: rw [← cpow_inv_two_re, sqrt]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
a : ℂ
⊢ HPow.hPow (β := ℂ) a 2⁻¹ =
    (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I
have 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
Tactic: by_cases! h : 0 ≤ a.im
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
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
⊢ HPow.hPow (β := ℂ) a 2⁻¹ =
    (↑(HPow.hPow (β := ℂ) a 2⁻¹).re : ℂ) + (if 0 ≤ a.im then 1 else -1) * (↑√((‖a‖ - a.re) / 2) : ℂ) * I
have 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
Tactic: by_cases! h : 0 ≤ a.im
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
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) : 𝕜)
have 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)) : 𝕜)
Tactic: rw [sqrt, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
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)) : 𝕜)
have 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)) : 𝕜)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
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)) : 𝕜)
⊢ 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)) : 𝕜)
have neg : ∀ (h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
  Eq (α := 𝕜) ((↑√((re : (a : 𝕜) → ℝ) a) : 𝕜) : 𝕜)
    ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ Eq (α := 𝕜) ((↑√((re : (a : 𝕜) → ℝ) a) : 𝕜) : 𝕜)
    ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)
have this : Eq.{u_1 + 1} (α := 𝕜) I 0
Tactic: have : (I : 𝕜) = 0 := by grind [I_eq_zero_or_im_I_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
this : Eq.{u_1 + 1} (α := 𝕜) I 0
⊢ Eq (α := 𝕜) ((↑√((re : (a : 𝕜) → ℝ) a) : 𝕜) : 𝕜)
    ((map ℂ 𝕜 : (a : ℂ) → 𝕜) (Complex.sqrt ((map 𝕜 ℂ : (a : 𝕜) → ℂ) a)) : 𝕜)
have 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)
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]
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
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)
have 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)
Tactic: by_cases! ha' : 0 ≤ re a
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
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)
⊢ √((re : (a : 𝕜) → ℝ) a) =
    √((‖(↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I‖ +
          ((↑((re : (a : 𝕜) → ℝ) a) : ℂ) + HMul.hMul (α := ℂ) (↑0 : ℂ) I).re) /
        2)
have 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)
Tactic: by_cases! ha' : 0 ≤ re a
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
⊢ 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
have 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
Tactic: rw [sqrt, Complex.sqrt_eq_real_add_ite]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
⊢ (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
have 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
Tactic: obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
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
⊢ (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
have 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
Tactic: obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
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
have 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
Tactic: rw [← re_add_im a]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
a : ℝ
⊢ (↑a : ℂ).sqrt.re = √a
have simp : √((|a| + a) / 2) = √a
Tactic: simp only [cpow_inv_two_re, norm_real, Real.norm_eq_abs, ofReal_re, Complex.sqrt]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
a : ℂ
ha : 0 ≤ a
⊢ a.sqrt = (↑√a.re : ℂ)
have obtain : ∀ (α : ℝ) (hα : α ≥ 0) (ha : LE.le (α := ℂ) 0 (↑α : ℂ)), sqrt (↑α : ℂ) = (↑√(re (↑α : ℂ)) : ℂ)
Tactic: obtain ⟨α : ℝ, hα, rfl⟩ := RCLike.nonneg_iff_exists_ofReal.mp ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
⊢ sqrt (↑α : ℂ) = (↑√(re (↑α : ℂ)) : ℂ)
have simp : (↑α : ℂ).sqrt = (↑√α : ℂ)
Tactic: simp only [coe_algebraMap, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
⊢ (↑α : ℂ).sqrt = (↑√α : ℂ)
have rw : (↑√α : ℂ) + (↑(↑α : ℂ).sqrt.im : ℂ) * I = (↑√α : ℂ)
Tactic: rw [← re_add_im (α : ℂ).sqrt, re_sqrt_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝕜' : Type u_2
inst_1 : RCLike 𝕜'
a : 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ((im : (a : 𝕜') → ℝ) I : ℝ)
⊢ Eq.{u_2 + 1} (α := 𝕜') (sqrt ((map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a) : 𝕜') ((map 𝕜 𝕜' : (a : 𝕜) → 𝕜') (sqrt a) : 𝕜')
have this : Eq.{u_1 + 1} (α := 𝕜) I 0 ∨ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
Tactic: have := I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝕜' : Type u_2
inst_1 : RCLike 𝕜'
a : 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ((im : (a : 𝕜') → ℝ) I : ℝ)
this : Eq.{u_1 + 1} (α := 𝕜) I 0 ∨ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ Eq.{u_2 + 1} (α := 𝕜') (sqrt ((map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a) : 𝕜') ((map 𝕜 𝕜' : (a : 𝕜) → 𝕜') (sqrt a) : 𝕜')
have this₁ : Eq.{u_2 + 1} (α := 𝕜') I 0 ∨ Eq (α := ℝ) ((im : (a : 𝕜') → ℝ) I : ℝ) (1 : ℝ)
Tactic: have := I_eq_zero_or_im_I_eq_one (K := 𝕜')
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
⊢ sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
have inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0), sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
Tactic: obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0), sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
⊢ sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
have inr : ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)), sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
Tactic: obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)