awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℝ
simp : √((|a| + a) / 2) = √a
⊢ (↑a : ℂ).sqrt.re = √a

Tactic:
simp only [cpow_inv_two_re, norm_real, Real.norm_eq_abs, ofReal_re, Complex.sqrt]

Premises used: Complex.sqrt, Complex.norm_real, Complex.cpow_inv_two_re, Complex.ofReal_re, Real.norm_eq_abs
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℝ
⊢ √((|a| + a) / 2) = √a

Tactic:
grind
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : ℝ
⊢ (re : (a : 𝕜) → ℝ) (sqrt (↑a : 𝕜)) = √a

Tactic:
aesop (add simp [sqrt, Complex.re_sqrt_ofReal])

Premises used: Complex.re_sqrt_ofReal, RCLike.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℝ
⊢ sqrt a = √a

Tactic:
simp [← re_sqrt_ofReal (𝕜 := ℝ)]

Premises used: RCLike.re_sqrt_ofReal
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℂ
⊢ sqrt a = a.sqrt

Tactic:
simp [sqrt]

Premises used: RCLike.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℂ
ha : 0 ≤ a
obtain : ∀ (α : ℝ) (hα : α ≥ 0) (ha : LE.le (α := ℂ) 0 (↑α : ℂ)), sqrt (↑α : ℂ) = (↑√(re (↑α : ℂ)) : ℂ)
⊢ a.sqrt = (↑√a.re : ℂ)

Tactic:
obtain ⟨α : ℝ, hα, rfl⟩ := RCLike.nonneg_iff_exists_ofReal.mp ha

Premises used: RCLike.nonneg_iff_exists_ofReal, Iff.mp, rfl
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
simp : (↑α : ℂ).sqrt = (↑√α : ℂ)
⊢ sqrt (↑α : ℂ) = (↑√(re (↑α : ℂ)) : ℂ)

Tactic:
simp only [coe_algebraMap, ofReal_re]

Premises used: Complex.coe_algebraMap, Complex.ofReal_re
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
rw : (↑√α : ℂ) + (↑(↑α : ℂ).sqrt.im : ℂ) * I = (↑√α : ℂ)
⊢ (↑α : ℂ).sqrt = (↑√α : ℂ)

Tactic:
rw [← re_add_im (α : ℂ).sqrt, re_sqrt_ofReal]

Premises used: Complex.re_sqrt_ofReal, Complex.sqrt, Complex.ofReal, Complex.re_add_im
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
⊢ (↑√α : ℂ) + (↑(↑α : ℂ).sqrt.im : ℂ) * I = (↑√α : ℂ)

Tactic:
simp [sqrt, cpow_inv_two_im_eq_sqrt, abs_of_nonneg hα]

Premises used: Complex.sqrt, Complex.cpow_inv_two_im_eq_sqrt, abs_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝕜' : Type u_2
inst_1 : RCLike 𝕜'
a : 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ((im : (a : 𝕜') → ℝ) I : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜) I 0 ∨ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)

Tactic:
have := I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Module: Mathlib.Analysis.RCLike.Sqrt
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} (α := 𝕜') I 0 ∨ Eq (α := ℝ) ((im : (a : 𝕜') → ℝ) I : ℝ) (1 : ℝ)

Tactic:
have := I_eq_zero_or_im_I_eq_one (K := 𝕜')
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝕜' : Type u_2
inst_1 : RCLike 𝕜'
a : 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) ((im : (a : 𝕜') → ℝ) I : ℝ)
this_1 : Eq.{u_1 + 1} (α := 𝕜) I 0 ∨ Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
this : Eq.{u_2 + 1} (α := 𝕜') I 0 ∨ Eq (α := ℝ) ((im : (a : 𝕜') → ℝ) I : ℝ) (1 : ℝ)
⊢ Eq.{u_2 + 1} (α := 𝕜') (sqrt ((map 𝕜 𝕜' : (a : 𝕜) → 𝕜') a) : 𝕜') ((map 𝕜 𝕜' : (a : 𝕜) → 𝕜') (sqrt a) : 𝕜')

Tactic:
aesop (add simp [RCLike.sqrt, im_eq_zero])

Premises used: RCLike.sqrt, RCLike.im_eq_zero
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
h : Eq (α := ℝ) ((RCLike.im : (a : 𝕜) → ℝ) RCLike.I : ℝ) (1 : ℝ)
⊢ sqrt ((RCLike.map 𝕜 ℂ : (a : 𝕜) → ℂ) a) = (RCLike.map 𝕜 ℂ : (a : 𝕜) → ℂ) (RCLike.sqrt a)

Tactic:
aesop (add simp [RCLike.sqrt])

Premises used: RCLike.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0), sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
inr : ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)), sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
⊢ sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)

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 : 𝕜
ha : 0 ≤ a
h : Eq.{u_1 + 1} (α := 𝕜) I 0
⊢ sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)

Tactic:
simp [h, sqrt_eq_ite]

Premises used: RCLike.sqrt_eq_ite
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ LE.le (α := ℂ) (0 : ℂ) ((complexRingEquiv h : (a : 𝕜) → ℂ) a : ℂ)

Tactic:
simpa
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
inr :
  (↑√(Complex.re ((complexRingEquiv h : (a : 𝕜) → ℂ) a)) : ℂ) =
    (complexRingEquiv h : (a : 𝕜) → ℂ) (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
⊢ sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)

Tactic:
rw [sqrt_eq_ite, dif_pos h, RingEquiv.symm_apply_eq, Complex.sqrt_of_nonneg (by simpa)]

Premises used: RCLike.sqrt_eq_ite, RingEquiv.symm_apply_eq, dif_pos, Complex.sqrt_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ (↑√(Complex.re ((complexRingEquiv h : (a : 𝕜) → ℂ) a)) : ℂ) =
    (complexRingEquiv h : (a : 𝕜) → ℂ) (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
a : ℂ
ha : 0 ≤ a
obtain : ∀ (α : ℝ) (hα : α ≥ 0) (ha : LE.le (α := ℂ) 0 (↑α : ℂ)), sqrt (-(↑α : ℂ)) = I * sqrt (↑α : ℂ)
⊢ (-a).sqrt = I * a.sqrt

Tactic:
obtain ⟨α, hα, rfl⟩ := RCLike.nonneg_iff_exists_ofReal.mp ha

Premises used: RCLike.nonneg_iff_exists_ofReal, Iff.mp, rfl
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
rw : sqrt (-(↑α : ℂ)) = I * (↑√(re (↑α : ℂ)) : ℂ)
⊢ sqrt (-(↑α : ℂ)) = I * sqrt (↑α : ℂ)

Tactic:
rw [Complex.sqrt_of_nonneg ha]

Premises used: Complex.sqrt_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
simp : (-(↑α : ℂ)).sqrt = I * (↑√α : ℂ)
⊢ sqrt (-(↑α : ℂ)) = I * (↑√(re (↑α : ℂ)) : ℂ)

Tactic:
simp only [coe_algebraMap, ofReal_re]

Premises used: Complex.coe_algebraMap, Complex.ofReal_re
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
rw : (↑(-(↑α : ℂ)).sqrt.re : ℂ) + (↑(-(↑α : ℂ)).sqrt.im : ℂ) * I = I * (↑√α : ℂ)
⊢ (-(↑α : ℂ)).sqrt = I * (↑√α : ℂ)

Tactic:
rw [← re_add_im (-(α : ℂ)).sqrt]

Premises used: Complex.sqrt, Complex.ofReal, Complex.re_add_im, Neg.neg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
⊢ (↑(-(↑α : ℂ)).sqrt.re : ℂ) + (↑(-(↑α : ℂ)).sqrt.im : ℂ) * I = I * (↑√α : ℂ)

Tactic:
simp [sqrt, cpow_inv_two_im_eq_sqrt, abs_of_nonneg hα, cpow_inv_two_re, mul_comm]

Premises used: Complex.sqrt, Complex.cpow_inv_two_im_eq_sqrt, Complex.cpow_inv_two_re, mul_comm, abs_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0), sqrt (-a) = I * sqrt a
inr : ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)), sqrt (-a) = I * sqrt a
⊢ sqrt (-a) = I * sqrt a

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 : 𝕜
ha : 0 ≤ a
h : Eq.{u_1 + 1} (α := 𝕜) I 0
⊢ sqrt (-a) = I * sqrt a

Tactic:
simp [h, sqrt_eq_ite, Real.sqrt_eq_zero', nonneg_iff.mp ha]

Premises used: RCLike.sqrt_eq_ite, RCLike.nonneg_iff, Iff.mp, Real.sqrt_eq_zero'
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
inr : Complex.I * Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) a) = (complexRingEquiv h : (a : 𝕜) → ℂ) (I * sqrt a)
⊢ sqrt (-a) = I * sqrt a

Tactic:
rw [sqrt_eq_ite, dif_pos h, RingEquiv.symm_apply_eq, map_neg,
    Complex.sqrt_neg_of_nonneg (by simpa)]

Premises used: RCLike.sqrt_eq_ite, RingEquiv.symm_apply_eq, Complex.sqrt_neg_of_nonneg, dif_pos, map_neg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ Complex.I * Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) a) = (complexRingEquiv h : (a : 𝕜) → ℂ) (I * sqrt a)

Tactic:
simp [h, sqrt, map_mul]

Premises used: map_mul, RCLike.sqrt
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
⊢ LE.le (α := ℂ) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
⊢ sqrt (-1) = I

Tactic:
simp [sqrt_neg_of_nonneg (a := 1) (by simp)]

Premises used: Complex.sqrt_neg_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ LE.le.{u_1} (α := 𝕜) 0 1

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

Tactic:
simp [sqrt_neg_of_nonneg (a := (1 : 𝕜)) (by simp)]

Premises used: RCLike.sqrt_neg_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
⊢ 0 ≤ I.im

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
rw : (↑√((‖I‖ + I.re) / 2) : ℂ) + (↑√((‖I‖ - I.re) / 2) : ℂ) * I = (↑√2⁻¹ : ℂ) * (1 + I)
⊢ I.sqrt = (↑√2⁻¹ : ℂ) * (1 + I)

Tactic:
rw [sqrt, ← re_add_im (I ^ 2⁻¹), cpow_inv_two_im_eq_sqrt (by simp), cpow_inv_two_re]

Premises used: Complex.sqrt, Complex.cpow_inv_two_im_eq_sqrt, Complex.cpow_inv_two_re, Inv.inv, HPow.hPow, Complex.re_add_im, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
⊢ (↑√((‖I‖ + I.re) / 2) : ℂ) + (↑√((‖I‖ - I.re) / 2) : ℂ) * I = (↑√2⁻¹ : ℂ) * (1 + I)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
⊢ (-I).im < 0

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
rw : (↑√((‖-I‖ + (-I).re) / 2) : ℂ) + (↑(-√((‖-I‖ - (-I).re) / 2)) : ℂ) * I = (↑√2⁻¹ : ℂ) * (1 - I)
⊢ (-I).sqrt = (↑√2⁻¹ : ℂ) * (1 - I)

Tactic:
rw [sqrt, ← re_add_im ((-I) ^ 2⁻¹), cpow_inv_two_im_eq_neg_sqrt (by simp), cpow_inv_two_re]

Premises used: Complex.sqrt, Complex.cpow_inv_two_re, Inv.inv, HPow.hPow, Complex.cpow_inv_two_im_eq_neg_sqrt, Complex.re_add_im, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
⊢ (↑√((‖-I‖ + (-I).re) / 2) : ℂ) + (↑(-√((‖-I‖ - (-I).re) / 2)) : ℂ) * I = (↑√2⁻¹ : ℂ) * (1 - I)

Tactic:
simp [mul_sub, ← sub_eq_add_neg]

Premises used: mul_sub, sub_eq_add_neg
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
rw :
  (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
      ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I))
    else (↑√((re : (a : 𝕜) → ℝ) I) : 𝕜)) =
    (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
⊢ sqrt I = (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I

Tactic:
rw [sqrt_eq_ite]

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

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
pos :
  Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I) =
    HMul.hMul (β := ℂ)
      (HMul.hMul (α := ℂ) (β := ℂ) ((complexRingEquiv h : (a : 𝕜) → ℂ) (↑√2⁻¹ : 𝕜) : ℂ)
        ((complexRingEquiv h : (a : 𝕜) → ℂ) (HSub.hSub (α := 𝕜) 1 I) : ℂ))
      ((complexRingEquiv h : (a : 𝕜) → ℂ) I : ℂ)
⊢ ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I)) =
    (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I

Tactic:
simp_rw [RingEquiv.symm_apply_eq, map_mul]

Premises used: RingEquiv.symm_apply_eq, map_mul
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I) =
    HMul.hMul (β := ℂ)
      (HMul.hMul (α := ℂ) (β := ℂ) ((complexRingEquiv h : (a : 𝕜) → ℂ) (↑√2⁻¹ : 𝕜) : ℂ)
        ((complexRingEquiv h : (a : 𝕜) → ℂ) (HSub.hSub (α := 𝕜) 1 I) : ℂ))
      ((complexRingEquiv h : (a : 𝕜) → ℂ) I : ℂ)

Tactic:
simp [h, mul_assoc, mul_add, add_comm, Complex.sqrt_I, add_mul]

Premises used: add_mul, Complex.sqrt_I, mul_assoc, add_comm, mul_add
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ (↑√((re : (a : 𝕜) → ℝ) I) : 𝕜) = (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I

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 𝕜
rw :
  (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
      ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I)))
    else (↑√((re : (a : 𝕜) → ℝ) (-I)) : 𝕜)) =
    (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
⊢ sqrt (-I) = (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I

Tactic:
rw [sqrt_eq_ite]

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

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
pos :
  Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I)) =
    HMul.hMul (β := ℂ)
      (HMul.hMul (α := ℂ) (β := ℂ) ((complexRingEquiv h : (a : 𝕜) → ℂ) (↑√2⁻¹ : 𝕜) : ℂ)
        ((complexRingEquiv h : (a : 𝕜) → ℂ) (HAdd.hAdd (α := 𝕜) 1 I) : ℂ))
      ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I) : ℂ)
⊢ ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I))) =
    (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I

Tactic:
simp_rw [RingEquiv.symm_apply_eq, map_mul]

Premises used: RingEquiv.symm_apply_eq, map_mul
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I)) =
    HMul.hMul (β := ℂ)
      (HMul.hMul (α := ℂ) (β := ℂ) ((complexRingEquiv h : (a : 𝕜) → ℂ) (↑√2⁻¹ : 𝕜) : ℂ)
        ((complexRingEquiv h : (a : 𝕜) → ℂ) (HAdd.hAdd (α := 𝕜) 1 I) : ℂ))
      ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I) : ℂ)

Tactic:
simp [h, mul_assoc, add_comm, Complex.sqrt_neg_I, neg_mul, mul_add, add_mul, mul_sub,
      mul_comm Complex.I, ← sub_eq_add_neg]

Premises used: add_mul, mul_sub, mul_assoc, sub_eq_add_neg, add_comm, Complex.sqrt_neg_I, mul_comm, mul_add, neg_mul, Complex.I
-- Module: Mathlib.Analysis.RCLike.Sqrt
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ (↑√((re : (a : 𝕜) → ℝ) (-I)) : 𝕜) = (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I

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.TangentCone
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h𝕜 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
s : Set E
x : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ tangentConeAt ℝ s x ⊆ tangentConeAt 𝕜 s x

Tactic:
tangentConeAt_mono_field

Premises used: tangentConeAt_mono_field
-- Module: Mathlib.Analysis.RCLike.TangentCone
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h𝕜 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
s : Set E
x : E
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ tangentConeAt ℝ s x ⊆ tangentConeAt 𝕜 s x

Tactic:
exact tangentConeAt_mono_field

Premises used: tangentConeAt_mono_field
-- Module: Mathlib.Analysis.RCLike.TangentCone
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h𝕜 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
s : Set E
x : E
hs : UniqueDiffWithinAt ℝ s x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
hs.mono_field

Premises used: UniqueDiffWithinAt.mono_field
-- Module: Mathlib.Analysis.RCLike.TangentCone
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h𝕜 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
s : Set E
x : E
hs : UniqueDiffWithinAt ℝ s x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
exact hs.mono_field

Premises used: UniqueDiffWithinAt.mono_field
-- Module: Mathlib.Analysis.RCLike.TangentCone
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h𝕜 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
s : Set E
hs : UniqueDiffOn ℝ s
⊢ UniqueDiffOn 𝕜 s

Tactic:
fun x hx ↦ (hs x hx).of_real

Premises used: UniqueDiffOn, UniqueDiffWithinAt.of_real
-- Module: Mathlib.Analysis.RCLike.TangentCone
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h𝕜 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
s : Set E
x : E
conv : Convex ℝ s
hs : (interior s).Nonempty
hx : x ∈ closure s
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
UniqueDiffWithinAt.of_real (uniqueDiffWithinAt_convex conv hs hx)

Premises used: uniqueDiffWithinAt_convex, UniqueDiffWithinAt.of_real
-- Module: Mathlib.Analysis.RCLike.TangentCone
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h𝕜 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
s : Set E
conv : Convex ℝ s
hs : (interior s).Nonempty
⊢ UniqueDiffOn 𝕜 s

Tactic:
UniqueDiffOn.of_real (uniqueDiffOn_convex conv hs)

Premises used: UniqueDiffOn.of_real, uniqueDiffOn_convex
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = c ^ n

Tactic:
simp [cantorFunctionAux, h]

Premises used: Cardinal.cantorFunctionAux
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0

Tactic:
simp [cantorFunctionAux, h]

Premises used: Cardinal.cantorFunctionAux
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
false : ∀ (h' : f n = Bool.false), 0 ≤ cantorFunctionAux c f n
true : ∀ (h' : f n = Bool.true), 0 ≤ cantorFunctionAux c f n
⊢ 0 ≤ cantorFunctionAux c f n

Tactic:
cases h' : f n
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = false
⊢ 0 ≤ cantorFunctionAux c f n

Tactic:
simp [h']
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ cantorFunctionAux c f n

Tactic:
simpa [h'] using pow_nonneg h _

Premises used: pow_nonneg
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = g n
⊢ cantorFunctionAux c f n = cantorFunctionAux c g n

Tactic:
simp [cantorFunctionAux, h]

Premises used: Cardinal.cantorFunctionAux
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
false : ∀ (h : f 0 = Bool.false), cantorFunctionAux c f 0 = bif Bool.false then 1 else 0
true : ∀ (h : f 0 = Bool.true), cantorFunctionAux c f 0 = bif Bool.true then 1 else 0
⊢ cantorFunctionAux c f 0 = bif f 0 then 1 else 0

Tactic:
cases h : f 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h : f 0 = false
⊢ cantorFunctionAux c f 0 = bif false then 1 else 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h : f 0 = true
⊢ cantorFunctionAux c f 0 = bif true then 1 else 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h : ∀ (n : ℕ), cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ cantorFunctionAux c f (n + 1)) fun (n : ℕ) ↦
    c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n

Tactic:
ext n
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : ∀ (h : f (n + 1) = false), cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
h₁ : ∀ (h : f (n + 1) = true), cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n

Tactic:
cases h : f (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = false
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n

Tactic:
simp [h, _root_.pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = true
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n

Tactic:
simp [h, _root_.pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
apply : ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b
⊢ Summable (cantorFunctionAux c f)

Tactic:
apply (summable_geometric_of_lt_one h1 h2).summable_of_eq_zero_or_self

Premises used: Summable.summable_of_eq_zero_or_self, summable_geometric_of_lt_one
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
false : ∀ (h : f n = Bool.false), cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
true : ∀ (h : f n = Bool.true), cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n

Tactic:
cases h : f n
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
apply : ∀ (i : ℕ), cantorFunctionAux c f i ≤ cantorFunctionAux c g i
⊢ cantorFunction c f ≤ cantorFunction c g

Tactic:
apply (summable_cantor_function f h1 h2).tsum_le_tsum _ (summable_cantor_function g h1 h2)

Premises used: Summable.tsum_le_tsum, Cardinal.summable_cantor_function
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = Bool.true → g n = Bool.true
n : ℕ
false : ∀ (h : f n = Bool.false), cantorFunctionAux c f n ≤ cantorFunctionAux c g n
true : ∀ (h : f n = Bool.true), cantorFunctionAux c f n ≤ cantorFunctionAux c g n
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
cases h : f n
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
simp [h, cantorFunctionAux_nonneg h1]

Premises used: Cardinal.cantorFunctionAux_nonneg