awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
m : ℕ
s : Bool
e : ℕ
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(ofScientific m s e) : K) : ℝ) (ofScientific m s e : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (ofScientific m s e) (ofScientific m s e)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (ofScientific m s e) : ℝ) (ofScientific m s e : ℝ)

Tactic:
rw [← ofReal_ofScientific, ofReal_re]

Premises used: RCLike.ofReal_re, RCLike.ofReal_ofScientific
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
m : ℕ
s : Bool
e : ℕ
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(ofScientific m s e) : K) : ℝ) (0 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (ofScientific m s e) : ℝ) (0 : ℝ)

Tactic:
rw [← ofReal_ofScientific, ofReal_im]

Premises used: RCLike.ofReal_im, RCLike.ofReal_ofScientific
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
r : ℝ
h : 0 ≤ r
⊢ norm.{u_1} (E := K) (↑r : K) = r

Tactic:
(norm_ofReal _).trans (abs_of_nonneg h)

Premises used: RCLike.norm_ofReal, abs_of_nonneg, Eq.trans
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
rw : norm.{u_1} (E := K) (↑(↑n : ℝ) : K) = (↑n : ℝ)
⊢ norm.{u_1} (E := K) (↑n : K) = (↑n : ℝ)

Tactic:
rw [← ofReal_natCast]

Premises used: RCLike.ofReal_natCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
⊢ norm.{u_1} (E := K) (↑(↑n : ℝ) : K) = (↑n : ℝ)

Tactic:
norm_of_nonneg (Nat.cast_nonneg n)

Premises used: Nat.cast_nonneg, RCLike.norm_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
⊢ norm.{u_1} (E := K) (↑(↑n : ℝ) : K) = (↑n : ℝ)

Tactic:
exact norm_of_nonneg (Nat.cast_nonneg n)

Premises used: Nat.cast_nonneg, RCLike.norm_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
⊢ nnnorm.{u_1} (E := K) (↑n : K) = (↑n : NNReal)

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
⊢ norm.{u_1} (E := K) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
norm_natCast n

Premises used: RCLike.norm_natCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
⊢ nnnorm.{u_1} (E := K) (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
nnnorm_natCast n

Premises used: RCLike.nnnorm_natCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ norm.{u_1} (E := K) 2 = 2

Tactic:
norm_ofNat 2

Premises used: RCLike.norm_ofNat, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ nnnorm.{u_1} (E := K) 2 = 2

Tactic:
nnnorm_ofNat 2

Premises used: RCLike.nnnorm_ofNat, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
rw : norm.{u_1} (E := K) (↑(↑q : ℝ) : K) = (↑q : ℝ)
⊢ norm.{u_1} (E := K) (↑q : K) = (↑q : ℝ)

Tactic:
rw [← ofReal_nnratCast]

Premises used: RCLike.ofReal_nnratCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
⊢ norm.{u_1} (E := K) (↑(↑q : ℝ) : K) = (↑q : ℝ)

Tactic:
norm_of_nonneg q.cast_nonneg

Premises used: NNRat.cast_nonneg, RCLike.norm_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
⊢ norm.{u_1} (E := K) (↑(↑q : ℝ) : K) = (↑q : ℝ)

Tactic:
exact norm_of_nonneg q.cast_nonneg

Premises used: NNRat.cast_nonneg, RCLike.norm_of_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
simp : NNReal.mk (↑q : ℝ) ⋯ = (↑q : NNReal)
⊢ nnnorm.{u_1} (E := K) (↑q : K) = (↑q : NNReal)

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
q : ℚ≥0
⊢ NNReal.mk (↑q : ℝ) ⋯ = (↑q : NNReal)

Tactic:
rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖ = n • ‖x‖

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using norm_smul (n : K) x

Premises used: norm_smul, Nat.cast, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
n : ℕ
x : E
⊢ ‖n • x‖₊ = n • ‖x‖₊

Tactic:
simpa [Nat.cast_smul_eq_nsmul] using nnnorm_smul (n : K) x

Premises used: nnnorm_smul, Nat.cast, Nat.cast_smul_eq_nsmul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : ‖z‖ * ‖z‖ = HPow.hPow (β := ℕ) ‖z‖ 2
rw₁ rw₂ : ‖z‖ * ‖z‖ = ‖z‖ * ‖z‖
⊢ ‖z‖ * ‖z‖ = (normSq : (a : K) → ℝ) z

Tactic:
rw [normSq_eq_def', sq]

Premises used: sq, RCLike.normSq_eq_def'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) ≤ (normSq : (a : K) → ℝ) z
⊢ |(re : (a : K) → ℝ) z| ≤ ‖z‖

Tactic:
rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]

Premises used: mul_self_le_mul_self_iff, RCLike.mul_self_norm, abs_mul_abs_self, norm_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) ≤ (normSq : (a : K) → ℝ) z

Tactic:
apply re_sq_le_normSq

Premises used: RCLike.re_sq_le_normSq
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ) ≤ (normSq : (a : K) → ℝ) z
⊢ |(im : (a : K) → ℝ) z| ≤ ‖z‖

Tactic:
rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]

Premises used: mul_self_le_mul_self_iff, RCLike.mul_self_norm, abs_mul_abs_self, norm_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ) ≤ (normSq : (a : K) → ℝ) z

Tactic:
apply im_sq_le_normSq

Premises used: RCLike.im_sq_le_normSq
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ norm (E := ℝ) ((re : (a : K) → ℝ) z : ℝ) ≤ ‖z‖

Tactic:
abs_re_le_norm z

Premises used: RCLike.abs_re_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ norm (E := ℝ) ((im : (a : K) → ℝ) z : ℝ) ≤ ‖z‖

Tactic:
abs_im_le_norm z

Premises used: RCLike.abs_im_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (re : (a : K) → ℝ) z ≤ ‖z‖

Tactic:
(abs_le.1 (abs_re_le_norm z)).2

Premises used: RCLike.abs_re_le_norm, abs_le, And.right, Iff.mp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (im : (a : K) → ℝ) z ≤ ‖z‖

Tactic:
(abs_le.1 (abs_im_le_norm _)).2

Premises used: abs_le, RCLike.abs_im_le_norm, And.right, Iff.mp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : K
h : ‖a‖ ≤ (re : (a : K) → ℝ) a
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) a : ℝ) (0 : ℝ)

Tactic:
simpa only [mul_self_norm a, normSq_apply, left_eq_add, mul_self_eq_zero]
    using congr_arg (fun z => z * z) ((re_le_norm a).antisymm h)

Premises used: mul_self_eq_zero, left_eq_add, HMul.hMul, LE.le.antisymm, congr_arg, RCLike.re_le_norm, RCLike.mul_self_norm, RCLike.normSq_apply
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : K
h : ‖a‖ ≤ (re : (a : K) → ℝ) a
rw : (starRingEnd K : (a : K) → K) a = a
rw₁ : Eq (α := ℝ) ((im : (a : K) → ℝ) a : ℝ) (0 : ℝ)
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ (↑((re : (a : K) → ℝ) a) : K) = a

Tactic:
rw [← conj_eq_iff_re, conj_eq_iff_im, im_eq_zero_of_le h]

Premises used: RCLike.conj_eq_iff_re, RCLike.im_eq_zero_of_le, RCLike.conj_eq_iff_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : HDiv.hDiv (α := ℝ) (|(re : (a : K) → ℝ) z| : ℝ) ‖z‖ ≤ 1
⊢ |HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ‖z‖| ≤ 1

Tactic:
rw [abs_div, abs_norm]

Premises used: abs_div, abs_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HDiv.hDiv (α := ℝ) (|(re : (a : K) → ℝ) z| : ℝ) ‖z‖ ≤ 1

Tactic:
div_le_one_of_le₀ (abs_re_le_norm _) (norm_nonneg _)

Premises used: div_le_one_of_le₀, RCLike.abs_re_le_norm, norm_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HDiv.hDiv (α := ℝ) (|(re : (a : K) → ℝ) z| : ℝ) ‖z‖ ≤ 1

Tactic:
exact div_le_one_of_le₀ (abs_re_le_norm _) (norm_nonneg _)

Premises used: div_le_one_of_le₀, RCLike.abs_re_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : HDiv.hDiv (α := ℝ) (|(im : (a : K) → ℝ) z| : ℝ) ‖z‖ ≤ 1
⊢ |HDiv.hDiv (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ‖z‖| ≤ 1

Tactic:
rw [abs_div, abs_norm]

Premises used: abs_div, abs_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HDiv.hDiv (α := ℝ) (|(im : (a : K) → ℝ) z| : ℝ) ‖z‖ ≤ 1

Tactic:
div_le_one_of_le₀ (abs_im_le_norm _) (norm_nonneg _)

Premises used: div_le_one_of_le₀, RCLike.abs_im_le_norm, norm_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HDiv.hDiv (α := ℝ) (|(im : (a : K) → ℝ) z| : ℝ) ‖z‖ ≤ 1

Tactic:
exact div_le_one_of_le₀ (abs_im_le_norm _) (norm_nonneg _)

Premises used: div_le_one_of_le₀, RCLike.abs_im_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
hI : Ne.{u_1 + 1} (α := K) I 0
rw : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = HMul.hMul (α := ℝ) 1 1
rw₁ : norm.{u_1} (E := K) I * norm.{u_1} (E := K) I = 1
rw₂ : ‖HMul.hMul (α := K) I I‖ = 1
rw₃ : norm.{u_1} (E := K) (-1) = 1
rw₄ : norm.{u_1} (E := K) 1 = 1
rw₅ rw₆ : Eq (α := ℝ) 1 1
⊢ norm.{u_1} (E := K) I = 1

Tactic:
rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
    I_mul_I_of_nonzero hI, norm_neg, norm_one]

Premises used: mul_self_inj_of_nonneg, NormOneClass.norm_one, norm_mul, zero_le_one, RCLike.I, norm_neg, norm_nonneg, RCLike.I_mul_I_of_nonzero, one_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
rw : (re : (a : K) → ℝ) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : K) = norm.{u_1} (E := K) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : K)
⊢ (re : (a : K) → ℝ) (HMul.hMul (β := K) x ((starRingEnd K : (a : K) → K) x : K)) =
    ‖HMul.hMul (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖

Tactic:
rw [mul_conj, ← ofReal_pow]

Premises used: RCLike.mul_conj, RCLike.ofReal_pow
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ (re : (a : K) → ℝ) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : K) = norm.{u_1} (E := K) (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : K)

Tactic:
simp [-map_pow]

Premises used: map_pow
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) 2 (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₁ :
  HPow.hPow (β := ℕ) ‖HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HMul.hMul (α := K) (↑2 : K) (↑((re : (a : K) → ℝ) x) : K)) : ℝ) 2
rw₂ :
  HPow.hPow (β := ℕ) (norm.{u_1} (E := K) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K)) 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
rw₃ :
  HPow.hPow (β := ℕ) |HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)| 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
rw₄ :
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) 2 =
    HPow.hPow (α := ℝ) (β := ℕ)
      ((re : (a : K) → ℝ) (↑(HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) : K) : ℝ) 2
rw₅ rw₆ :
  HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) 2 =
    HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : K) → ℝ) x : ℝ)) 2
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2

Tactic:
rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]

Premises used: RCLike.ofReal_re, RCLike.norm_ofReal, RCLike.ofReal_mul, RCLike.add_conj, sq_abs, RCLike.ofReal_ofNat
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
rw :
  HPow.hPow (β := ℕ) ‖HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
rw₁ rw₂ :
  HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (β := K) x ((starRingEnd K : (a : K) → K) x : K)) : ℝ) 2
⊢ HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := K) ((starRingEnd K : (a : K) → K) x : K) x‖ 2 =
    HPow.hPow (α := ℝ) (β := ℕ) ((re : (a : K) → ℝ) (HAdd.hAdd (α := K) ((starRingEnd K : (a : K) → K) x : K) x) : ℝ) 2

Tactic:
rw [add_comm, norm_sq_re_add_conj]

Premises used: add_comm, RCLike.norm_sq_re_add_conj
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℤ
x : K
rw : ‖(↑r : K) * x‖ = ‖r‖ * ‖x‖
rw₁ : norm.{u_1} (E := K) (↑r : K) * ‖x‖ = ‖r‖ * ‖x‖
rw₂ : norm.{u_1} (E := K) (↑(↑r : ℝ) : K) * ‖x‖ = ‖r‖ * ‖x‖
rw₃ : |(↑r : ℝ)| * ‖x‖ = ‖r‖ * ‖x‖
rw₄ rw₅ : |(↑r : ℝ)| * ‖x‖ = |(↑r : ℝ)| * ‖x‖
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

Tactic:
rw [zsmul_eq_mul, norm_mul, ← ofReal_intCast, norm_ofReal, Int.norm_eq_abs]

Premises used: zsmul_eq_mul, RCLike.norm_ofReal, Int.norm_eq_abs, norm_mul, RCLike.ofReal_intCast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
f : CauSeq K norm
x : ℝ
ε0 : x > 0
i : ℕ
H : ∀ j ≥ i, ‖(↑f : ℕ → K) j - (↑f : ℕ → K) i‖ < x
j : ℕ
ij : j ≥ i
⊢ |HSub.hSub (α := ℝ) ((fun (n : ℕ) ↦ ((re : (a : K) → ℝ) ((↑f : ℕ → K) n) : ℝ)) j)
        ((fun (n : ℕ) ↦ ((re : (a : K) → ℝ) ((↑f : ℕ → K) n) : ℝ)) i)| ≤
    ‖(↑f : ℕ → K) j - (↑f : ℕ → K) i‖

Tactic:
simpa only [map_sub] using abs_re_le_norm (f j - f i)

Premises used: map_sub, RCLike.abs_re_le_norm, HSub.hSub, Subtype.val
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
f : CauSeq K norm
x : ℝ
ε0 : x > 0
i : ℕ
H : ∀ j ≥ i, ‖(↑f : ℕ → K) j - (↑f : ℕ → K) i‖ < x
j : ℕ
ij : j ≥ i
⊢ |HSub.hSub (α := ℝ) ((fun (n : ℕ) ↦ ((im : (a : K) → ℝ) ((↑f : ℕ → K) n) : ℝ)) j)
        ((fun (n : ℕ) ↦ ((im : (a : K) → ℝ) ((↑f : ℕ → K) n) : ℝ)) i)| ≤
    ‖(↑f : ℕ → K) j - (↑f : ℕ → K) i‖

Tactic:
simpa only [map_sub] using abs_im_le_norm (f j - f i)

Premises used: map_sub, HSub.hSub, RCLike.abs_im_le_norm, Subtype.val
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
f : ℕ → K
hf : IsCauSeq norm f
⊢ IsCauSeq abs (norm ∘ f)

Tactic:
fun ε ε0 =>
  let ⟨i, hi⟩ := hf ε ε0
  ⟨i, fun j hj => lt_of_le_of_lt (abs_norm_sub_norm_le _ _) (hi j hj)⟩

Premises used: lt_of_le_of_lt, Exists, _private.0.RCLike.isCauSeq_norm.match_1, abs_norm_sub_norm_le, Exists.intro, IsCauSeq
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
⊢ Eq (α := ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : ℝ
⊢ HAdd.hAdd (α := ℝ) ((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) z : ℝ) : ℝ)
      (HMul.hMul (α := ℝ) (β := ℝ) ((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((0 : (a : ℝ) → ℝ) z : ℝ) : ℝ) (0 : ℝ)) =
    z

Tactic:
simp only [add_zero, mul_zero, Algebra.algebraMap_self, RingHom.id_apply, AddMonoidHom.id_apply]

Premises used: RingHom.id_apply, Algebra.algebraMap_self, AddMonoidHom.id_apply, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z w : ℝ
⊢ (AddMonoidHom.id ℝ : (a : ℝ) → ℝ) (z * w) =
    HMul.hMul (α := ℝ) (β := ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) z : ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) w : ℝ) -
      HMul.hMul (α := ℝ) (β := ℝ) ((0 : (a : ℝ) → ℝ) z : ℝ) ((0 : (a : ℝ) → ℝ) w : ℝ)

Tactic:
simp only [sub_zero, mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply]

Premises used: sub_zero, AddMonoidHom.id_apply, AddMonoidHom.zero_apply, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z w : ℝ
⊢ (0 : (a : ℝ) → ℝ) (z * w) =
    HMul.hMul (α := ℝ) (β := ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) z : ℝ) ((0 : (a : ℝ) → ℝ) w : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((0 : (a : ℝ) → ℝ) z : ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) w : ℝ)

Tactic:
simp only [add_zero, zero_mul, mul_zero, AddMonoidHom.zero_apply]

Premises used: MulZeroClass.zero_mul, AddMonoidHom.zero_apply, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : ℝ
⊢ Eq (α := ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) z : ℝ) : ℝ)
    ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) z : ℝ)

Tactic:
simp only [starRingEnd_apply, star_id_of_comm]

Premises used: starRingEnd_apply, star_id_of_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : ℝ
⊢ Eq (α := ℝ) ((0 : (a : ℝ) → ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) x : ℝ) : ℝ) (-(0 : (a : ℝ) → ℝ) x : ℝ)

Tactic:
simp only [neg_zero, AddMonoidHom.zero_apply]

Premises used: AddMonoidHom.zero_apply, neg_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
⊢ Eq (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) 0 : ℝ) (-0 : ℝ)

Tactic:
simp only [map_zero, neg_zero]

Premises used: map_zero, neg_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : ℝ
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 =
    HMul.hMul (α := ℝ) (β := ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) z : ℝ) ((AddMonoidHom.id ℝ : (a : ℝ) → ℝ) z : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((0 : (a : ℝ) → ℝ) z : ℝ) ((0 : (a : ℝ) → ℝ) z : ℝ)

Tactic:
simp only [sq, Real.norm_eq_abs, ← abs_mul, abs_mul_self z, add_zero,
    mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply]

Premises used: AddMonoidHom.id_apply, AddMonoidHom.zero_apply, abs_mul, abs_mul_self, sq, MulZeroClass.mul_zero, add_zero, Real.norm_eq_abs
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : ℝ
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((0 : (a : ℝ) → ℝ) x : ℝ) ((0 : (a : ℝ) → ℝ) 0 : ℝ) = (0 : (a : ℝ) → ℝ) x

Tactic:
simp only [mul_zero, AddMonoidHom.zero_apply]

Premises used: AddMonoidHom.zero_apply, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedField E
inst_2 : CharZero E
inst_3 : NormedSpace K E
q : ℚ≥0
x : E
⊢ ‖q • x‖ = q • ‖x‖

Tactic:
simpa [NNRat.cast_smul_eq_nnqsmul] using norm_smul (q : K) x

Premises used: norm_smul, NNRat.cast_smul_eq_nnqsmul, NNRat.cast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedField E
inst_2 : CharZero E
inst_3 : NormedSpace K E
q : ℚ≥0
x : E
⊢ ‖q • x‖₊ = q • ‖x‖₊

Tactic:
simpa [NNRat.cast_smul_eq_nnqsmul] using nnnorm_smul (q : K) x

Premises used: nnnorm_smul, NNRat.cast_smul_eq_nnqsmul, NNRat.cast
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
inst_1 : NormedField E
inst_2 : CharZero E
inst_3 : NormedSpace K E
ι : Type u_3
s : Finset ι
f : ι → E
x : ℕ
x_1 : E
rw rw₁ : HSMul.hSMul (α := ℚ≥0) (↑x : ℚ≥0)⁻¹ ‖x_1‖ = HSMul.hSMul (α := ℚ≥0) (↑x : ℚ≥0)⁻¹ ‖x_1‖
⊢ ‖HSMul.hSMul (α := ℚ≥0) (↑x : ℚ≥0)⁻¹ x_1‖ = HSMul.hSMul (α := ℚ≥0) (↑x : ℚ≥0)⁻¹ ‖x_1‖

Tactic:
rw [norm_nnqsmul K]

Premises used: RCLike.norm_nnqsmul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
simp_rw :
  (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
      z ≠ w ↔
    (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
⊢ z < w ↔
    LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)

Tactic:
simp_rw [lt_iff_le_and_ne, @RCLike.le_iff_re_im K]

Premises used: lt_iff_le_and_ne, RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
mp :
  (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
      z ≠ w →
    (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
mpr :
  (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) →
    (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
      z ≠ w
⊢ (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
      z ≠ w ↔
    (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
        Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)

Tactic:
constructor
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
heq : z ≠ w
hr : LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)
hi : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
⊢ (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)

Tactic:
⟨⟨hr, mt (fun hreq => ext hreq hi) heq⟩, hi⟩

Premises used: mt, RCLike.ext, And.intro
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
heq : z ≠ w
hr : LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)
hi : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
⊢ (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)

Tactic:
exact ⟨⟨hr, mt (fun hreq => ext hreq hi) heq⟩, hi⟩
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
hi : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
hr : LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)
hrn : Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)
⊢ (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
    z ≠ w

Tactic:
⟨⟨hr, hi⟩, ne_of_apply_ne _ hrn⟩

Premises used: ne_of_apply_ne, And.intro
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
hi : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)
hr : LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)
hrn : Ne (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)
⊢ (LE.le (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) ∧
    z ≠ w

Tactic:
exact ⟨⟨hr, hi⟩, ne_of_apply_ne _ hrn⟩