awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous (Y := ℝ) fun (a : K × K) ↦ (im : (a : K) → ℝ) a.2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
z : K
rw :
  Eq (α := ℝ)
    ((im : (a : K) → ℝ) ((↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) 0) : ℝ)
    (0 : ℝ)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
rw [← re_add_im z, h]

Premises used: RCLike.re_add_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
z : K
⊢ Eq (α := ℝ)
    ((im : (a : K) → ℝ) ((↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) 0) : ℝ)
    (0 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
x : K
nth_rw :
  (↑((re : (a : K) → ℝ) x) : K) = (↑((re : (a : K) → ℝ) x) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) x) : K) I
⊢ (↑((re : (a : K) → ℝ) x) : K) = x

Tactic:
nth_rw 2 [← re_add_im x]

Premises used: RCLike.re_add_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
x : K
⊢ (↑((re : (a : K) → ℝ) x) : K) = (↑((re : (a : K) → ℝ) x) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) x) : K) I

Tactic:
simp [h]
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
⊢ ∀ (x y : K),
    (re : (a : K) → ℝ) (x * y) = HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)

Tactic:
simp [im_eq_zero h]

Premises used: RCLike.im_eq_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
z : K
rw :
  norm (E := ℝ)
      (({ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun,
              left_inv := ⋯, right_inv := ⋯ : K ≃ₗ[ℝ] ℝ } :
            (a : K) → ℝ)
          ((↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I) :
        ℝ) =
    ‖(↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I‖
⊢ norm (E := ℝ)
      (({ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun,
              left_inv := ⋯, right_inv := ⋯ : K ≃ₗ[ℝ] ℝ } :
            (a : K) → ℝ)
          z :
        ℝ) =
    ‖z‖

Tactic:
rw [← re_add_im z]

Premises used: RCLike.re_add_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
z : K
⊢ norm (E := ℝ)
      (({ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun,
              left_inv := ⋯, right_inv := ⋯ : K ≃ₗ[ℝ] ℝ } :
            (a : K) → ℝ)
          ((↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I) :
        ℝ) =
    ‖(↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) I‖

Tactic:
simp [-re_add_im, h]

Premises used: RCLike.re_add_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
inl : ∀ (h : Eq.{u_1 + 1} (α := K) I 0), ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)
inr :
  ∀ (h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)),
    ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)

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

Premises used: RCLike.I_eq_zero_or_im_I_eq_one
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq.{u_1 + 1} (α := K) I 0
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)

Tactic:
simp [h, im_eq_zero]

Premises used: RCLike.im_eq_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
h_1 : Eq.{u_1 + 1} (α := K) I 0
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
⊢ Ne.{u_1 + 1} (α := K) I 0

Tactic:
have : (I : K) ≠ 0 := fun _ ↦ by simp_all
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
this : Ne.{u_1 + 1} (α := K) I 0
inr : ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ -I * z = -I * HMul.hMul (α := K) I (↑‖z‖ : K)
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)

Tactic:
rw [← mul_right_inj' (neg_ne_zero.mpr this)]

Premises used: Iff.mpr, neg_ne_zero, mul_right_inj'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
this : Ne.{u_1 + 1} (α := K) I 0
⊢ ‖-I * z‖ ≤ (re : (a : K) → ℝ) (-I * z) ↔ -I * z = (↑‖-I * z‖ : K)

Tactic:
norm_le_re_iff_eq_norm (z := -I * z)

Premises used: RCLike.norm_le_re_iff_eq_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
this : Ne.{u_1 + 1} (α := K) I 0
h₁ : ‖z‖ = ‖-I * z‖
h₂ : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) (-I * z) : ℝ)
h₃ : -I * HMul.hMul (α := K) I (↑‖z‖ : K) = (↑‖-I * z‖ : K)
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ -I * z = -I * HMul.hMul (α := K) I (↑‖z‖ : K)

Tactic:
convert! norm_le_re_iff_eq_norm (z := -I * z) using 2

Premises used: RCLike.norm_le_re_iff_eq_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
this : Ne.{u_1 + 1} (α := K) I 0
⊢ ‖z‖ = ‖-I * z‖

Tactic:
simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

Premises used: RCLike.norm_I_of_ne_zero, mul_assoc, neg_mul, RCLike.I_mul_I_of_nonzero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
this : Ne.{u_1 + 1} (α := K) I 0
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) (-I * z) : ℝ)

Tactic:
simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

Premises used: RCLike.norm_I_of_ne_zero, mul_assoc, neg_mul, RCLike.I_mul_I_of_nonzero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
this : Ne.{u_1 + 1} (α := K) I 0
⊢ -I * HMul.hMul (α := K) I (↑‖z‖ : K) = (↑‖-I * z‖ : K)

Tactic:
simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

Premises used: RCLike.norm_I_of_ne_zero, mul_assoc, neg_mul, RCLike.I_mul_I_of_nonzero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (im : (a : K) → ℝ) z ≤ -‖z‖ ↔ z = -HMul.hMul (α := K) I (↑‖z‖ : K)

Tactic:
simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_im_iff_eq_I_mul_norm (z := -z)

Premises used: le_neg, neg_eq_iff_eq_neg, RCLike.norm_le_im_iff_eq_I_mul_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
G : Type u_3
inst_1 : Finite G
inst_2 : AddLeftCancelMonoid G
ψ : AddChar G K
x : G
⊢ Eq.{u_1 + 1} (α := K) (((ψ : (a : G) → K) x)⁻¹ : K) ((starRingEnd K : (a : K) → K) ((ψ : (a : G) → K) x : K) : K)

Tactic:
RCLike.inv_eq_conj <| norm_apply _ _

Premises used: AddChar.norm_apply, RCLike.inv_eq_conj
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
G : Type u_3
inst_1 : Finite G
inst_2 : AddCommGroup G
ψ : AddChar G K
x : G
rw : Eq.{u_1 + 1} (α := K) (((ψ : (a : G) → K) x)⁻¹ : K) ((starRingEnd K : (a : K) → K) ((ψ : (a : G) → K) x : K) : K)
rw₁ rw₂ :
  Eq (α := K) ((starRingEnd K : (a : K) → K) ((ψ : (a : G) → K) x : K) : K)
    ((starRingEnd K : (a : K) → K) ((ψ : (a : G) → K) x : K) : K)
⊢ Eq.{u_1 + 1} (α := K) ((ψ : (a : G) → K) (-x) : K) ((starRingEnd K : (a : K) → K) ((ψ : (a : G) → K) x : K) : K)

Tactic:
rw [map_neg_eq_inv, inv_apply_eq_conj]

Premises used: AddChar.map_neg_eq_inv, AddChar.inv_apply_eq_conj
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
⊢ IsRCLikeNormedField 𝕜

Tactic:
⟨⟨h, rfl⟩⟩

Premises used: IsRCLikeNormedField.mk, Exists.intro, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst : ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ (a : 𝕜), x < ‖a‖ ∧ ‖a‖ < y
⊢ ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ (a : 𝕜), x < ‖a‖ ∧ ‖a‖ < y

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ (a : 𝕜), x < ‖a‖ ∧ ‖a‖ < y

Tactic:
h.lt_norm_lt

Premises used: DenselyNormedField.lt_norm_lt
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ (a : 𝕜), x < ‖a‖ ∧ ‖a‖ < y

Tactic:
exact h.lt_norm_lt

Premises used: DenselyNormedField.lt_norm_lt
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Function.Involutive.{u_3 + 1} (α := 𝕜) star

Tactic:
h.star_involutive

Premises used: InvolutiveStar.star_involutive
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Function.Involutive.{u_3 + 1} (α := 𝕜) star

Tactic:
exact h.star_involutive

Premises used: InvolutiveStar.star_involutive
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst : ∀ (r s : 𝕜), star (r * s) = star s * star r
⊢ ∀ (r s : 𝕜), star (r * s) = star s * star r

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r s : 𝕜), star (r * s) = star s * star r

Tactic:
h.star_mul

Premises used: StarMul.star_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r s : 𝕜), star (r * s) = star s * star r

Tactic:
exact h.star_mul

Premises used: StarMul.star_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst : ∀ (r s : 𝕜), star (r + s) = star r + star s
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s

Tactic:
h.star_add

Premises used: StarRing.star_add
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s

Tactic:
exact h.star_add

Premises used: StarRing.star_add
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst : Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 1 : 𝕜) (1 : 𝕜)
⊢ Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 1 : 𝕜) (1 : 𝕜)

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 1 : 𝕜) (1 : 𝕜)

Tactic:
h.algebraMap.map_one'

Premises used: Algebra.algebraMap, OneHom.map_one', MonoidHom.toOneHom, RingHom.toMonoidHom
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 1 : 𝕜) (1 : 𝕜)

Tactic:
exact h.algebraMap.map_one'

Premises used: Algebra.algebraMap, OneHom.map_one', MonoidHom.toOneHom, RingHom.toMonoidHom
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x * y) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)
⊢ ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x * y) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x * y) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)

Tactic:
h.algebraMap.map_mul'

Premises used: Algebra.algebraMap, MonoidHom.map_mul', RingHom.toMonoidHom
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x * y) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)

Tactic:
exact h.algebraMap.map_mul'

Premises used: Algebra.algebraMap, MonoidHom.map_mul', RingHom.toMonoidHom
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst : Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 0 : 𝕜) (0 : 𝕜)
⊢ Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 0 : 𝕜) (0 : 𝕜)

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 0 : 𝕜) (0 : 𝕜)

Tactic:
h.algebraMap.map_zero'

Premises used: Algebra.algebraMap, RingHom.map_zero'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 0 : 𝕜) (0 : 𝕜)

Tactic:
exact h.algebraMap.map_zero'

Premises used: Algebra.algebraMap, RingHom.map_zero'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x + y) =
      HAdd.hAdd (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)
⊢ ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x + y) =
      HAdd.hAdd (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x + y) =
      HAdd.hAdd (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)

Tactic:
h.algebraMap.map_add'

Premises used: RingHom.map_add', Algebra.algebraMap
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x + y) =
      HAdd.hAdd (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)

Tactic:
exact h.algebraMap.map_add'

Premises used: RingHom.map_add', Algebra.algebraMap
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  ∀ (r : ℝ) (x : 𝕜),
    HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x =
      HMul.hMul (β := 𝕜) x
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
⊢ ∀ (r : ℝ) (x : 𝕜),
    HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x =
      HMul.hMul (β := 𝕜) x
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x =
      HMul.hMul (β := 𝕜) x
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)

Tactic:
h.commutes'

Premises used: Algebra.commutes'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x =
      HMul.hMul (β := 𝕜) x
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)

Tactic:
exact h.commutes'

Premises used: Algebra.commutes'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  ∀ (r : ℝ) (x : 𝕜),
    r • x =
      HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x
⊢ ∀ (r : ℝ) (x : 𝕜),
    r • x =
      HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    r • x =
      HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x

Tactic:
h.smul_def'

Premises used: Algebra.smul_def'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    r • x =
      HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x

Tactic:
exact h.smul_def'

Premises used: Algebra.smul_def'
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst : ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖
⊢ ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
h.norm_smul_le

Premises used: NormedAlgebra.norm_smul_le
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
exact h.norm_smul_le

Premises used: NormedAlgebra.norm_smul_le
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst : ∀ {f : Filter 𝕜}, Cauchy f → ∃ (x : 𝕜), f ≤ nhds x
⊢ ∀ {f : Filter 𝕜}, Cauchy f → ∃ (x : 𝕜), f ≤ nhds x

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
f : Filter 𝕜
⊢ Cauchy f → ∃ (x : 𝕜), f ≤ nhds x

Tactic:
h.complete

Premises used: CompleteSpace.complete
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ ∀ {f : Filter 𝕜}, Cauchy f → ∃ (x : 𝕜), f ≤ nhds x

Tactic:
exact h.complete

Premises used: CompleteSpace.complete
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
  𝕜 →+ ℝ
⊢ 𝕜 →+ ℝ

Tactic:
subst h''
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ 𝕜 →+ ℝ

Tactic:
exact h.re

Premises used: RCLike.re
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField
⊢ 𝕜 →+ ℝ

Tactic:
exact h.im

Premises used: RCLike.im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
subst :
  Eq (α := ℝ)
    (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        I :
      ℝ)
    (0 : ℝ)
⊢ Eq (α := ℝ)
    (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
              let __spread.0 := hk;
              𝕜 →+ ℝ)
              (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
              re)
              ⋯ :
            let __spread.0 := hk;
            𝕜 →+ ℝ) :
          (a : 𝕜) → ℝ)
        I :
      ℝ)
    (0 : ℝ)

Tactic:
subst h''