awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ edist (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ) ≤ (↑1 : ENNReal) * edist x y
have simp : ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ
Tactic: simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ =
    enorm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ)
have rw : ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ =
  ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ
Tactic: rw [map_sub im x y]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ enorm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖ₑ
have rw : norm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖
Tactic: rw [enorm_le_iff_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ
have calc : ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ =
  enorm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ)
Tactic: calc ‖im x - im y‖ₑ
  _ = ‖im (x - y)‖ₑ := by rw [map_sub im x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_im_le_norm (x - y)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x y : K
calc :
  ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ =
    enorm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ)
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ
have calc₁ : enorm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖ₑ
Tactic: calc ‖im x - im y‖ₑ
  _ = ‖im (x - y)‖ₑ := by rw [map_sub im x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_im_le_norm (x - y)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
𝕜' : Type u_4
inst_1 : RCLike 𝕜
inst_2 : RCLike 𝕜'
x x_1 : 𝕜
⊢ (↑((re : (a : 𝕜) → ℝ) (x + x_1)) : 𝕜') + HMul.hMul (α := 𝕜') (↑((im : (a : 𝕜) → ℝ) (x + x_1)) : 𝕜') I =
    (↑((re : (a : 𝕜) → ℝ) x) : 𝕜') + HMul.hMul (α := 𝕜') (↑((im : (a : 𝕜) → ℝ) x) : 𝕜') I +
      ((↑((re : (a : 𝕜) → ℝ) x_1) : 𝕜') + HMul.hMul (α := 𝕜') (↑((im : (a : 𝕜) → ℝ) x_1) : 𝕜') I)
have simp : HAdd.hAdd (α := 𝕜') (β := 𝕜') ((algebraMap ℝ 𝕜' : (a : ℝ) → 𝕜') ((re : (a : 𝕜) → ℝ) x : ℝ) : 𝕜')
      ((algebraMap ℝ 𝕜' : (a : ℝ) → 𝕜') ((re : (a : 𝕜) → ℝ) x_1 : ℝ) : 𝕜') +
    (HMul.hMul (α := 𝕜') (β := 𝕜') ((algebraMap ℝ 𝕜' : (a : ℝ) → 𝕜') ((im : (a : 𝕜) → ℝ) x : ℝ) : 𝕜') (I : 𝕜') +
      HMul.hMul (α := 𝕜') (β := 𝕜') ((algebraMap ℝ 𝕜' : (a : ℝ) → 𝕜') ((im : (a : 𝕜) → ℝ) x_1 : ℝ) : 𝕜') (I : 𝕜')) =
  (↑((re : (a : 𝕜) → ℝ) x) : 𝕜') + HMul.hMul (α := 𝕜') (↑((im : (a : 𝕜) → ℝ) x) : 𝕜') I +
    ((↑((re : (a : 𝕜) → ℝ) x_1) : 𝕜') + HMul.hMul (α := 𝕜') (↑((im : (a : 𝕜) → ℝ) x_1) : 𝕜') I)
Tactic: simp only [map_add, add_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := K →L[ℝ] K) (map K K) (ContinuousLinearMap.id ℝ K)
have h : ∀ (x : K), Eq (α := K) ((map K K : (a : K) → K) x : K) ((ContinuousLinearMap.id ℝ K : (a : K) → K) x : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := K →L[ℝ] ℝ) (map K ℝ) reCLM
have h : ∀ (x : K), Eq (α := ℝ) ((map K ℝ : (a : K) → ℝ) x : ℝ) ((reCLM : (a : K) → ℝ) x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ Eq (α := ℝ) ((map K ℝ : (a : K) → ℝ) x : ℝ) ((reCLM : (a : K) → ℝ) x : ℝ)
have h : Eq (α := ℝ) ((↑((re : (a : K) → ℝ) x) : ℝ) : ℝ) ((reCLM : (a : K) → ℝ) x : ℝ)
Tactic: simp only [map_apply, I, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := ℝ →L[ℝ] K) (map ℝ K) ofRealCLM
have h : Eq (α := K) ((map ℝ K : (a : ℝ) → K) 1 : K) ((ofRealCLM : (a : ℝ) → K) 1 : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
p : K × K
| p.1 ≤ p.2
have rw : LE.le (α := ℝ) ((re : (a : K) → ℝ) p.1 : ℝ) ((re : (a : K) → ℝ) p.2 : ℝ) ∧
  Eq (α := ℝ) ((im : (a : K) → ℝ) p.1 : ℝ) ((im : (a : K) → ℝ) p.2 : ℝ)
Tactic: rw [RCLike.le_iff_re_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ IsClosed.{u_1} (X := K × K) {p : K × K | p.1 ≤ p.2}
have conv : IsClosed.{u_1} (X := K × K)
  {p : K × K |
    LE.le (α := ℝ) ((re : (a : K) → ℝ) p.1 : ℝ) ((re : (a : K) → ℝ) p.2 : ℝ) ∧
      Eq (α := ℝ) ((im : (a : K) → ℝ) p.1 : ℝ) ((im : (a : K) → ℝ) p.2 : ℝ)}
Tactic: conv in _ ≤ _ => rw [RCLike.le_iff_re_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ IsClosed.{u_1} (X := K × K)
    ({a : K × K | LE.le (α := ℝ) ((re : (a : K) → ℝ) a.1 : ℝ) ((re : (a : K) → ℝ) a.2 : ℝ)} ∩
      {a : K × K | Eq (α := ℝ) ((im : (a : K) → ℝ) a.1 : ℝ) ((im : (a : K) → ℝ) a.2 : ℝ)})
have refine_1 : Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.1
Tactic: refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
refine_1 : Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.1
⊢ IsClosed.{u_1} (X := K × K)
    ({a : K × K | LE.le (α := ℝ) ((re : (a : K) → ℝ) a.1 : ℝ) ((re : (a : K) → ℝ) a.2 : ℝ)} ∩
      {a : K × K | Eq (α := ℝ) ((im : (a : K) → ℝ) a.1 : ℝ) ((im : (a : K) → ℝ) a.2 : ℝ)})
have refine_2 : Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.2
Tactic: refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
refine_1 : Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.1
refine_2 : Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.2
⊢ IsClosed.{u_1} (X := K × K)
    ({a : K × K | LE.le (α := ℝ) ((re : (a : K) → ℝ) a.1 : ℝ) ((re : (a : K) → ℝ) a.2 : ℝ)} ∩
      {a : K × K | Eq (α := ℝ) ((im : (a : K) → ℝ) a.1 : ℝ) ((im : (a : K) → ℝ) a.2 : ℝ)})
have refine_3 : Continuous (Y := ℝ) fun (a : K × K) ↦ (im : (a : K) → ℝ) a.1
Tactic: refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
refine_1 : Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.1
refine_2 : Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.2
refine_3 : Continuous (Y := ℝ) fun (a : K × K) ↦ (im : (a : K) → ℝ) a.1
⊢ IsClosed.{u_1} (X := K × K)
    ({a : K × K | LE.le (α := ℝ) ((re : (a : K) → ℝ) a.1 : ℝ) ((re : (a : K) → ℝ) a.2 : ℝ)} ∩
      {a : K × K | Eq (α := ℝ) ((im : (a : K) → ℝ) a.1 : ℝ) ((im : (a : K) → ℝ) a.2 : ℝ)})
have refine_4 : Continuous (Y := ℝ) fun (a : K × K) ↦ (im : (a : K) → ℝ) a.2
Tactic: refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
h : Eq.{u_1 + 1} (α := K) I 0
z : K
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ)
  ((im : (a : K) → ℝ) ((↑((re : (a : K) → ℝ) z) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) z) : K) 0) : ℝ) (0 : ℝ)
Tactic: rw [← re_add_im z, h]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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) = x
have nth_rw : (↑((re : (a : K) → ℝ) x) : K) = (↑((re : (a : K) → ℝ) x) : K) + HMul.hMul (α := K) (↑((im : (a : K) → ℝ) x) : K) I
Tactic: nth_rw 2 [← re_add_im x]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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) → ℝ)
          z :
        ℝ) =
    ‖z‖
have rw : norm (E := ℝ)
    (({ toFun := (realRingEquiv h).toFun, map_add' := sorry, map_smul' := sorry, invFun := (realRingEquiv h).invFun,
            left_inv := sorry, right_inv := sorry : 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: rw [← re_add_im z]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)
have inl : ∀ (h : Eq.{u_1 + 1} (α := K) I 0), ‖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)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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)
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)
have inr : ∀ (h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)), ‖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)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
h : Eq (α := ℝ) ((im : (a : K) → ℝ) I : ℝ) (1 : ℝ)
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)
have this : Ne.{u_1 + 1} (α := K) I 0
Tactic: have : (I : K) ≠ 0 := fun _ ↦ by simp_all
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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‖ ≤ (im : (a : K) → ℝ) z ↔ z = HMul.hMul (α := K) I (↑‖z‖ : K)
have inr : ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ -I * z = -I * HMul.hMul (α := K) I (↑‖z‖ : K)
Tactic: rw [← mul_right_inj' (neg_ne_zero.mpr this)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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‖ ≤ (im : (a : K) → ℝ) z ↔ -I * z = -I * HMul.hMul (α := K) I (↑‖z‖ : K)
have h₁ : ‖z‖ = ‖-I * z‖
Tactic: convert! norm_le_re_iff_eq_norm (z := -I * z) using 2
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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‖
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ -I * z = -I * HMul.hMul (α := K) I (↑‖z‖ : K)
have h₂ : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) (-I * z) : ℝ)
Tactic: convert! norm_le_re_iff_eq_norm (z := -I * z) using 2
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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) : ℝ)
⊢ ‖z‖ ≤ (im : (a : K) → ℝ) z ↔ -I * z = -I * HMul.hMul (α := K) I (↑‖z‖ : K)
have h₃ : -I * HMul.hMul (α := K) I (↑‖z‖ : K) = (↑‖-I * z‖ : K)
Tactic: convert! norm_le_re_iff_eq_norm (z := -I * z) using 2
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := K) ((ψ : (a : G) → K) (-x) : K) ((starRingEnd K : (a : K) → K) ((ψ : (a : G) → K) x : K) : K)
have rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := K) ((ψ : (a : G) → K) (-x) : K) ((starRingEnd K : (a : K) → K) ((ψ : (a : G) → K) x : K) : K)
have 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)
Tactic: rw [map_neg_eq_inv, inv_apply_eq_conj]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ (a : 𝕜), x < ‖a‖ ∧ ‖a‖ < y
have subst : ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ (a : 𝕜), x < ‖a‖ ∧ ‖a‖ < y
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (r s : 𝕜), star (r * s) = star s * star r
have subst : ∀ (r s : 𝕜), star (r * s) = star s * star r
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s
have subst : ∀ (r s : 𝕜), star (r + s) = star r + star s
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 1 : 𝕜) (1 : 𝕜)
have subst : Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 1 : 𝕜) (1 : 𝕜)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x * y) =
      HMul.hMul (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)
have subst : ∀ (x y : ℝ),
  (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x * y) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 0 : 𝕜) (0 : 𝕜)
have subst : Eq (α := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) 0 : 𝕜) (0 : 𝕜)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (x y : ℝ),
    (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x + y) =
      HAdd.hAdd (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)
have subst : ∀ (x y : ℝ),
  (algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (x + y) =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) x : 𝕜) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) y : 𝕜)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = 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 :
          𝕜)
have subst : ∀ (r : ℝ) (x : 𝕜),
  HMul.hMul (α := 𝕜)
      (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
              ℝ →+* 𝕜 } :
            (a : ℝ) → 𝕜)
          r :
        𝕜)
      x =
    HMul.hMul (β := 𝕜) x
      (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
              ℝ →+* 𝕜 } :
            (a : ℝ) → 𝕜)
          r :
        𝕜)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    r • x =
      HMul.hMul (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            r :
          𝕜)
        x
have subst : ∀ (r : ℝ) (x : 𝕜),
  r • x =
    HMul.hMul (α := 𝕜)
      (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
              ℝ →+* 𝕜 } :
            (a : ℝ) → 𝕜)
          r :
        𝕜)
      x
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖
have subst : ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ {f : Filter 𝕜}, Cauchy f → ∃ (x : 𝕜), f ≤ nhds x
have subst : ∀ {f : Filter 𝕜}, Cauchy f → ∃ (x : 𝕜), f ≤ nhds x
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ 𝕜 →+ ℝ
have subst : let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
𝕜 →+ ℝ
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ 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 : ℝ)
have subst : Eq (α := ℝ)
  (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
            let __spread.0 := hk;
            𝕜 →+ ℝ)
            (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
            re)
            sorry :
          let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
          𝕜 →+ ℝ) :
        (a : 𝕜) → ℝ)
      I :
    ℝ)
  (0 : ℝ)
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ Eq.{u_3 + 1} (α := 𝕜) I 0 ∨ HMul.hMul (α := 𝕜) I I = -1
have subst : Eq.{u_3 + 1} (α := 𝕜) I 0 ∨ HMul.hMul (α := 𝕜) I I = -1
Tactic: subst h''
Cleared hypotheses: hk, h''
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = DenselyNormedField.toNormedField
⊢ ∀ (z : 𝕜),
    HAdd.hAdd (α := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                      let __spread.0 := hk;
                      𝕜 →+ ℝ)
                      (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      re)
                      ⋯ :
                    let __spread.0 := hk;
                    𝕜 →+ ℝ) :
                  (a : 𝕜) → ℝ)
                z :
              ℝ) :
          𝕜)
        (HMul.hMul (α := 𝕜) (β := 𝕜)
          (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ :
                  ℝ →+* 𝕜 } :
                (a : ℝ) → 𝕜)
              (((Eq.ndrec (motive := fun (hk : NormedField 𝕜) ↦
                        let __spread.0 := hk;
                        𝕜 →+ ℝ)
                        (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                        im)
                        ⋯ :
                      let __spread.0 := hk;
                      𝕜 →+ ℝ) :
                    (a : 𝕜) → ℝ)
                  z :
                ℝ) :
            𝕜)
          (I : 𝕜)) =
      z
have subst : ∀ (z : 𝕜),
  HAdd.hAdd (α := 𝕜)
      (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
              ℝ →+* 𝕜 } :
            (a : ℝ) → 𝕜)
          (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                    let __spread.0 := hk;
                    𝕜 →+ ℝ)
                    (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    re)
                    sorry :
                  let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                  𝕜 →+ ℝ) :
                (a : 𝕜) → ℝ)
              z :
            ℝ) :
        𝕜)
      (HMul.hMul (α := 𝕜) (β := 𝕜)
        (({ toFun := (⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry :
                ℝ →+* 𝕜 } :
              (a : ℝ) → 𝕜)
            (((Eq.ndrec (a := DenselyNormedField.toNormedField) (motive := fun (hk : NormedField 𝕜) ↦
                      let __spread.0 := hk;
                      𝕜 →+ ℝ)
                      (let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                      im)
                      sorry :
                    let __spread.0 : NormedField 𝕜 := DenselyNormedField.toNormedField;
                    𝕜 →+ ℝ) :
                  (a : 𝕜) → ℝ)
                z :
              ℝ) :
          𝕜)
        (I : 𝕜)) =
    z
Tactic: subst h''
Cleared hypotheses: hk, h''