awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
z : K
hx : x < 0
⊢ 0 < HMul.hMul (β := ℝ) x ((re : (a : K) → ℝ) z : ℝ) ∧ HMul.hMul (β := ℝ) x ((im : (a : K) → ℝ) z : ℝ) = 0 ↔
    x < 0 ∧ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∨
      0 < x ∧ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
simp only [mul_pos_iff, not_lt_of_gt hx, false_and, hx, true_and, false_or, mul_eq_zero, hx.ne,
      or_false]

Premises used: false_and, false_or, mul_pos_iff, mul_eq_zero, not_lt_of_gt, or_false, true_and, LT.lt.ne
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
z : K
hx : x = 0
⊢ 0 < HMul.hMul (β := ℝ) x ((re : (a : K) → ℝ) z : ℝ) ∧ HMul.hMul (β := ℝ) x ((im : (a : K) → ℝ) z : ℝ) = 0 ↔
    x < 0 ∧ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∨
      0 < x ∧ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
simp only [hx, zero_mul, lt_self_iff_false, false_and, false_or]

Premises used: MulZeroClass.zero_mul, false_and, false_or, lt_self_iff_false
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
z : K
hx : 0 < x
⊢ 0 < HMul.hMul (β := ℝ) x ((re : (a : K) → ℝ) z : ℝ) ∧ HMul.hMul (β := ℝ) x ((im : (a : K) → ℝ) z : ℝ) = 0 ↔
    x < 0 ∧ LT.lt (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) ∨
      0 < x ∧ LT.lt (α := ℝ) (0 : ℝ) ((re : (a : K) → ℝ) z : ℝ) ∧ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
simp only [mul_pos_iff, hx, true_and, not_lt_of_gt hx, false_and, or_false, mul_eq_zero,
      hx.ne', false_or]

Premises used: false_and, false_or, mul_pos_iff, mul_eq_zero, LT.lt.ne', not_lt_of_gt, or_false, true_and
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : ℝ
z : K
⊢ (↑x : K) * z < 0 ↔ x < 0 ∧ 0 < z ∨ 0 < x ∧ z < 0

Tactic:
simpa only [mul_neg, neg_pos, neg_neg_iff_pos] using ofReal_mul_pos_iff x (-z)

Premises used: neg_neg_iff_pos, neg_pos, RCLike.ofReal_mul_pos_iff, Neg.neg, mul_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h :
  (fun (x1 x2 : K) ↦ x1 ≤ x2) ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a b)
    ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a c)
obtain : ∀ (a' : ℝ) (ha1 : a' > 0) (ha2 : (↑a' : K) = (↑a : K)), b ≤ c
⊢ b ≤ c

Tactic:
obtain ⟨a', ha1, ha2⟩ := pos_iff_exists_ofReal.mp a.2

Premises used: RCLike.pos_iff_exists_ofReal, Iff.mp, Subtype.property
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h :
  (fun (x1 x2 : K) ↦ x1 ≤ x2) ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a b)
    ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a c)
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
rw : 0 ≤ c - b
⊢ b ≤ c

Tactic:
rw [← sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h :
  (fun (x1 x2 : K) ↦ x1 ≤ x2) ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a b)
    ((fun (x : { x : K // 0 < x }) (y : K) ↦ (↑x : K) * y) a c)
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
beta_reduce : ∀ (h : (↑a : K) * b ≤ (↑a : K) * c) (a' : ℝ) (ha1 : a' > 0) (ha2 : (↑a' : K) = (↑a : K)), 0 ≤ c - b
⊢ 0 ≤ c - b

Tactic:
beta_reduce at h
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h : (↑a : K) * b ≤ (↑a : K) * c
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
⊢ 0 < (↑a' : K) * (c - b) ∨ 0 = (↑a' : K) * (c - b)

Tactic:
rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h

Premises used: mul_sub, le_iff_lt_or_eq, sub_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h : (↑a : K) * b ≤ (↑a : K) * c
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
h₁ : 0 < (↑a' : K) * (c - b) ∨ 0 = (↑a' : K) * (c - b)
⊢ a' > 0

Tactic:
rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h

Premises used: mul_sub, le_iff_lt_or_eq, sub_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
h : (↑a : K) * b ≤ (↑a : K) * c
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
h₁ : 0 < (↑a' : K) * (c - b) ∨ 0 = (↑a' : K) * (c - b)
ha1₁ : a' > 0
⊢ (↑a' : K) = (↑a : K)

Tactic:
rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h

Premises used: mul_sub, le_iff_lt_or_eq, sub_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
h : 0 < (↑a' : K) * (c - b) ∨ 0 = (↑a' : K) * (c - b)
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
inl : ∀ (h : 0 < (↑a' : K) * (c - b)), 0 ≤ c - b
inr : ∀ (h : 0 = (↑a' : K) * (c - b)), 0 ≤ c - b
⊢ 0 ≤ c - b

Tactic:
rcases h with h | h
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
h : 0 < (↑a' : K) * (c - b)
⊢ a' < 0 ∧ c - b < 0 ∨ 0 < a' ∧ 0 < c - b

Tactic:
rw [ofReal_mul_pos_iff] at h

Premises used: RCLike.ofReal_mul_pos_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
h : a' < 0 ∧ c - b < 0 ∨ 0 < a' ∧ 0 < c - b
⊢ 0 ≤ c - b

Tactic:
le_of_lt <| h.rec (False.elim <| not_lt_of_gt ·.1 ha1) (·.2)

Premises used: Or.rec, le_of_lt
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
h : a' < 0 ∧ c - b < 0 ∨ 0 < a' ∧ 0 < c - b
⊢ 0 ≤ c - b

Tactic:
exact le_of_lt <| h.rec (False.elim <| not_lt_of_gt ·.1 ha1) (·.2)

Premises used: le_of_lt
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
h : 0 = (↑a' : K) * (c - b)
⊢ 0 ≤ c - b

Tactic:
((mul_eq_zero_iff_left <| ofReal_ne_zero.mpr ha1.ne').mp h.symm).ge

Premises used: Iff.mpr, Eq.ge, RCLike.ofReal_ne_zero, mul_eq_zero_iff_left, LT.lt.ne', Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
a : { x : K // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : (↑a' : K) = (↑a : K)
h : 0 = (↑a' : K) * (c - b)
⊢ 0 ≤ c - b

Tactic:
exact ((mul_eq_zero_iff_left <| ofReal_ne_zero.mpr ha1.ne').mp h.symm).ge

Premises used: Iff.mpr, Eq.ge, RCLike.ofReal_ne_zero, mul_eq_zero_iff_left, LT.lt.ne', Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ MulPosReflectLE K

Tactic:
PosMulReflectLE.toMulPosReflectLE

Premises used: PosMulReflectLE.toMulPosReflectLE
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
x : ℝ
⊢ (re : (a : ℝ) → ℝ) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
x : ℝ
⊢ Eq (α := ℝ) ((im : (a : ℝ) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
x : ℝ
⊢ (starRingEnd ℝ : (a : ℝ) → ℝ) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
⊢ Eq (α := ℝ) I 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
x : ℝ
⊢ (normSq : (a : ℝ) → ℝ) x = x * x

Tactic:
simp [RCLike.normSq]

Premises used: RCLike.normSq
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
⊢ ofReal = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := (a : K) → ℝ) (⇑reLm : (a : K) → ℝ) (⇑re : (a : K) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : K
rw : norm (E := ℝ) ((reLm : (a : K) → ℝ) x : ℝ) ≤ ‖x‖
⊢ norm (E := ℝ) ((reLm : (a : K) → ℝ) x : ℝ) ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : K
⊢ norm (E := ℝ) ((reLm : (a : K) → ℝ) x : ℝ) ≤ ‖x‖

Tactic:
abs_re_le_norm x

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

Tactic:
exact abs_re_le_norm x

Premises used: RCLike.abs_re_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := K →ₗ[ℝ] ℝ) (↑reCLM : K →ₗ[ℝ] ℝ) reLm

Tactic:
rfl

Premises used: RCLike.reLm, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := (a : K) → ℝ) (⇑reCLM : (a : K) → ℝ) (⇑re : (a : K) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous.{u_1, 0} (X := K) (Y := ℝ) (⇑re : (a : K) → ℝ)

Tactic:
reCLM.continuous

Premises used: RCLike.reCLM, ContinuousLinearMap.continuous
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := (a : K) → ℝ) (⇑imLm : (a : K) → ℝ) (⇑im : (a : K) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : K
rw : norm (E := ℝ) ((imLm : (a : K) → ℝ) x : ℝ) ≤ ‖x‖
⊢ norm (E := ℝ) ((imLm : (a : K) → ℝ) x : ℝ) ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : K
⊢ norm (E := ℝ) ((imLm : (a : K) → ℝ) x : ℝ) ≤ ‖x‖

Tactic:
abs_im_le_norm x

Premises used: RCLike.abs_im_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
x : K
⊢ norm (E := ℝ) ((imLm : (a : K) → ℝ) x : ℝ) ≤ ‖x‖

Tactic:
exact abs_im_le_norm x

Premises used: RCLike.abs_im_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := K →ₗ[ℝ] ℝ) (↑imCLM : K →ₗ[ℝ] ℝ) imLm

Tactic:
rfl

Premises used: RCLike.imLm, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := (a : K) → ℝ) (⇑imCLM : (a : K) → ℝ) (⇑im : (a : K) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous.{u_1, 0} (X := K) (Y := ℝ) (⇑im : (a : K) → ℝ)

Tactic:
imCLM.continuous

Premises used: ContinuousLinearMap.continuous, RCLike.imCLM
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := (a : K) → K) (⇑conjAe : (a : K) → K) (⇑(starRingEnd K) : (a : K) → K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := (a : K) → K) (⇑conjLIE : (a : K) → K) (⇑(starRingEnd K) : (a : K) → K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := K ≃ₗ[ℝ] K) (↑conjCLE : K ≃ₗ[ℝ] K) (↑conjAe : K ≃ₗ[ℝ] K)

Tactic:
rfl

Premises used: AlgEquiv.toLinearEquiv, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := (a : K) → K) (⇑conjCLE : (a : K) → K) (⇑(starRingEnd K) : (a : K) → K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
⊢ ContinuousStar K

Tactic:
⟨conjLIE.continuous⟩

Premises used: ContinuousStar.mk, LinearIsometryEquiv.continuous, RCLike.conjLIE
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous (X := K) (Y := K) (⇑(starRingEnd K) : (a : K) → K)

Tactic:
continuous_star

Premises used: ContinuousStar.continuous_star
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := (a : ℝ) → K) (⇑ofRealAm : (a : ℝ) → K) ofReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := (a : ℝ) → K) (⇑(ofRealStarAlgHom K) : (a : ℝ) → K) ofReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := ℝ →ₐ[ℝ] K) (↑(ofRealStarAlgHom K) : ℝ →ₐ[ℝ] K) ofRealAm

Tactic:
rfl

Premises used: RCLike.ofRealAm, Algebra.ofId, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := (a : ℝ) → K) (⇑ofRealLI : (a : ℝ) → K) ofReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := ℝ →ₗ[ℝ] K) (↑ofRealCLM : ℝ →ₗ[ℝ] K) (AlgHom.toLinearMap ofRealAm)

Tactic:
rfl

Premises used: AlgHom.toLinearMap, rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := (a : ℝ) → K) (⇑ofRealCLM : (a : ℝ) → K) ofReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous.{0, u_1} (Y := K) ofReal

Tactic:
ofRealLI.continuous

Premises used: LinearIsometry.continuous, RCLike.ofRealLI
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous.{u_1, 0} (X := K) (Y := ℝ) (⇑normSq : (a : K) → ℝ)

Tactic:
(continuous_re.mul continuous_re).add (continuous_im.mul continuous_im)

Premises used: RCLike.continuous_re, Continuous.mul, RCLike.continuous_im, Continuous.add
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ LipschitzWith.{0, u_1} (β := K) 1 ofReal

Tactic:
ofRealLI.lipschitz

Premises used: LinearIsometry.lipschitz, RCLike.ofRealLI
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
simp : ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ
⊢ edist (α := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ) ≤ (↑1 : ENNReal) * edist x y

Tactic:
simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub, ENNReal.coe_one, one_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
rw rw₁ :
  ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ =
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ =
    enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ)

Tactic:
rw [map_sub re x y]

Premises used: map_sub, RCLike.re
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
rw : norm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖
⊢ enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖ₑ

Tactic:
rw [enorm_le_iff_norm_le]

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

Tactic:
norm_re_le_norm (x - y)

Premises used: HSub.hSub, RCLike.norm_re_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ norm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖

Tactic:
exact norm_re_le_norm (x - y)

Premises used: HSub.hSub, RCLike.norm_re_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
calc :
  ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ =
    enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ)
calc₁ : enorm (E := ℝ) ((re : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖ₑ
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) x : ℝ) ((re : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ

Tactic:
calc ‖re x - re y‖ₑ
  _ = ‖re (x - y)‖ₑ := by rw [map_sub re x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_re_le_norm (x - y)

Premises used: HSub.hSub, RCLike.re, DFunLike.coe
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
simp : ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ ≤ ‖x - y‖ₑ
⊢ edist (α := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ) ≤ (↑1 : ENNReal) * edist x y

Tactic:
simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub, ENNReal.coe_one, one_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
rw rw₁ :
  ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ =
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) y : ℝ)‖ₑ =
    enorm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ)

Tactic:
rw [map_sub im x y]

Premises used: map_sub, RCLike.im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
rw : norm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖
⊢ enorm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖ₑ

Tactic:
rw [enorm_le_iff_norm_le]

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

Tactic:
norm_im_le_norm (x - y)

Premises used: HSub.hSub, RCLike.norm_im_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x y : K
⊢ norm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖

Tactic:
exact norm_im_le_norm (x - y)

Premises used: HSub.hSub, RCLike.norm_im_le_norm
-- Module: Mathlib.Analysis.RCLike.Basic
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) : ℝ)
calc₁ : enorm (E := ℝ) ((im : (a : K) → ℝ) (x - y) : ℝ) ≤ ‖x - y‖ₑ
⊢ ‖HSub.hSub (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) x : ℝ) ((im : (a : K) → ℝ) 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)

Premises used: HSub.hSub, RCLike.im, DFunLike.coe
-- Module: Mathlib.Analysis.RCLike.Basic
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 : 𝕜
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)
⊢ (↑((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)

Tactic:
simp only [map_add, add_mul]

Premises used: add_mul, map_add
-- Module: Mathlib.Analysis.RCLike.Basic
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 : 𝕜
⊢ 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:
ring
-- Module: Mathlib.Analysis.RCLike.Basic
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 =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) x : ℝ)
      ((↑((re : (a : 𝕜) → ℝ) x_1) : 𝕜') + HMul.hMul (α := 𝕜') (↑((im : (a : 𝕜) → ℝ) x_1) : 𝕜') I)

Tactic:
simp [real_smul_eq_coe_mul, mul_assoc]

Premises used: mul_assoc, RCLike.real_smul_eq_coe_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : ∀ (x : K), Eq (α := K) ((map K K : (a : K) → K) x : K) ((ContinuousLinearMap.id ℝ K : (a : K) → K) x : K)
⊢ Eq (α := K →L[ℝ] K) (map K K) (ContinuousLinearMap.id ℝ K)

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ Eq (α := K) ((map K K : (a : K) → K) x : K) ((ContinuousLinearMap.id ℝ K : (a : K) → K) x : K)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : ∀ (x : K), Eq (α := ℝ) ((map K ℝ : (a : K) → ℝ) x : ℝ) ((reCLM : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := K →L[ℝ] ℝ) (map K ℝ) reCLM

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
h : Eq (α := ℝ) ((↑((re : (a : K) → ℝ) x) : ℝ) : ℝ) ((reCLM : (a : K) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((map K ℝ : (a : K) → ℝ) x : ℝ) ((reCLM : (a : K) → ℝ) x : ℝ)

Tactic:
simp only [map_apply, I, mul_zero, add_zero]

Premises used: RCLike.map_apply, MulZeroClass.mul_zero, RCLike.I, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ Eq (α := ℝ) ((↑((re : (a : K) → ℝ) x) : ℝ) : ℝ) ((reCLM : (a : K) → ℝ) x : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
h : Eq (α := K) ((map ℝ K : (a : ℝ) → K) 1 : K) ((ofRealCLM : (a : ℝ) → K) 1 : K)
⊢ Eq (α := ℝ →L[ℝ] K) (map ℝ K) ofRealCLM

Tactic:
ext
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := K) ((map ℝ K : (a : ℝ) → K) 1 : K) ((ofRealCLM : (a : ℝ) → K) 1 : K)

Tactic:
simp
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
p : K × K
rw :
  LE.le (α := ℝ) ((re : (a : K) → ℝ) p.1 : ℝ) ((re : (a : K) → ℝ) p.2 : ℝ) ∧
    Eq (α := ℝ) ((im : (a : K) → ℝ) p.1 : ℝ) ((im : (a : K) → ℝ) p.2 : ℝ)
| p.1 ≤ p.2

Tactic:
rw [RCLike.le_iff_re_im]

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
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 : ℝ)}
⊢ IsClosed.{u_1} (X := K × K) {p : K × K | p.1 ≤ p.2}

Tactic:
conv in _ ≤ _ => rw [RCLike.le_iff_re_im]

Premises used: RCLike.le_iff_re_im
-- Module: Mathlib.Analysis.RCLike.Basic
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 : ℝ)})

Tactic:
IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_)

Premises used: isClosed_le, isClosed_eq, IsClosed.inter
-- Module: Mathlib.Analysis.RCLike.Basic
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
refine_4 : Continuous (Y := ℝ) fun (a : K × K) ↦ (im : (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 : ℝ)})

Tactic:
refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_)

Premises used: isClosed_le, isClosed_eq, IsClosed.inter
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.1

Tactic:
fun_prop
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous (Y := ℝ) fun (a : K × K) ↦ (re : (a : K) → ℝ) a.2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Continuous (Y := ℝ) fun (a : K × K) ↦ (im : (a : K) → ℝ) a.1

Tactic:
fun_prop