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
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₃ :
  HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₄ :
  (I * z + HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) I : K) ((starRingEnd K : (a : K) → K) z : K)) /
      2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₅ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₆ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z) / 2
rw₇ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    I * -HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₈ : (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
  I * HSub.hSub (β := K) z ((starRingEnd K : (a : K) → K) z : K) / 2
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₃ :
  HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₄ :
  (I * z + HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) I : K) ((starRingEnd K : (a : K) → K) z : K)) /
      2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₅ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₆ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z) / 2
rw₇ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    I * -HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
rw₈ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    I * HSub.hSub (β := K) z ((starRingEnd K : (a : K) → K) z : K) / 2
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₉ : (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
  (I * z - HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₃ :
  HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₄ :
  (I * z + HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) I : K) ((starRingEnd K : (a : K) → K) z : K)) /
      2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₅ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₆ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z) / 2
rw₇ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    I * -HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
rw₈ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    I * HSub.hSub (β := K) z ((starRingEnd K : (a : K) → K) z : K) / 2
rw₉ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    (I * z - HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₁₀ : (I * z + -HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
  (I * z - HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : -(↑((im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₁ : (↑(-(im : (a : K) → ℝ) z) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₂ : (↑((re : (a : K) → ℝ) (I * z)) : K) = -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₃ :
  HAdd.hAdd (β := K) (I * z) ((starRingEnd K : (a : K) → K) (I * z) : K) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₄ :
  (I * z + HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) I : K) ((starRingEnd K : (a : K) → K) z : K)) /
      2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₅ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2)
rw₆ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    -(I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z) / 2
rw₇ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    I * -HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
rw₈ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    I * HSub.hSub (β := K) z ((starRingEnd K : (a : K) → K) z : K) / 2
rw₉ :
  (I * z + HMul.hMul (α := K) (β := K) (-I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    (I * z - HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
rw₁₀ :
  (I * z + -HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
    (I * z - HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
⊢ (↑((im : (a : K) → ℝ) z) : K) = I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2
have rw₁₁ : (I * z + -HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2 =
  (I * z + -HMul.hMul (α := K) (β := K) (I : K) ((starRingEnd K : (a : K) → K) z : K)) / 2
Tactic: rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
    neg_sub, mul_sub, neg_mul, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h_1 : (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z := h_1
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
have rw : Eq.{u_1 + 1} (α := K) (↑((im : (a : K) → ℝ) z) : K) (↑0 : K)
Tactic: rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h_1 : (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z := h_1
rw : Eq.{u_1 + 1} (α := K) (↑((im : (a : K) → ℝ) z) : K) (↑0 : K)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
have rw₁ : I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2 = (↑0 : K)
Tactic: rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h_1 : (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z := h_1
rw : Eq.{u_1 + 1} (α := K) (↑((im : (a : K) → ℝ) z) : K) (↑0 : K)
rw₁ : I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2 = (↑0 : K)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
have rw₂ : I * (z - z) / 2 = (↑0 : K)
Tactic: rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h_1 : (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z := h_1
rw : Eq.{u_1 + 1} (α := K) (↑((im : (a : K) → ℝ) z) : K) (↑0 : K)
rw₁ : I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2 = (↑0 : K)
rw₂ : I * (z - z) / 2 = (↑0 : K)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
have rw₃ : HMul.hMul (α := K) I 0 / 2 = (↑0 : K)
Tactic: rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h_1 : (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z := h_1
rw : Eq.{u_1 + 1} (α := K) (↑((im : (a : K) → ℝ) z) : K) (↑0 : K)
rw₁ : I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2 = (↑0 : K)
rw₂ : I * (z - z) / 2 = (↑0 : K)
rw₃ : HMul.hMul (α := K) I 0 / 2 = (↑0 : K)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
have rw₄ : 0 / 2 = (↑0 : K)
Tactic: rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h_1 : (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z := h_1
rw : Eq.{u_1 + 1} (α := K) (↑((im : (a : K) → ℝ) z) : K) (↑0 : K)
rw₁ : I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2 = (↑0 : K)
rw₂ : I * (z - z) / 2 = (↑0 : K)
rw₃ : HMul.hMul (α := K) I 0 / 2 = (↑0 : K)
rw₄ : 0 / 2 = (↑0 : K)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
have rw₅ : Eq.{u_1 + 1} (α := K) 0 (↑0 : K)
Tactic: rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h_1 : (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z := h_1
rw : Eq.{u_1 + 1} (α := K) (↑((im : (a : K) → ℝ) z) : K) (↑0 : K)
rw₁ : I * HSub.hSub (α := K) ((starRingEnd K : (a : K) → K) z : K) z / 2 = (↑0 : K)
rw₂ : I * (z - z) / 2 = (↑0 : K)
rw₃ : HMul.hMul (α := K) I 0 / 2 = (↑0 : K)
rw₄ : 0 / 2 = (↑0 : K)
rw₅ : Eq.{u_1 + 1} (α := K) 0 (↑0 : K)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
have rw₆ : Eq.{u_1 + 1} (α := K) 0 0
Tactic: rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ [(starRingEnd K : (a : K) → K) z = z, ∃ (r : ℝ), (↑r : K) = z, (↑((re : (a : K) → ℝ) z) : K) = z,
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ), IsSelfAdjoint z].TFAE
have tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
Tactic: tfae_have 1 → 4
  | h => by
    rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
      ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
h_1 : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
h : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) := h_1
| z
have rw : (↑((re : (a : K) → ℝ) z) : K)
Tactic: rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
h_1 : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
h : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) := h_1
⊢ (↑((re : (a : K) → ℝ) z) : K) = z
have conv_rhs : (↑((re : (a : K) → ℝ) z) : K) = z
Tactic: conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
h_1 : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
h : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ) := h_1
conv_rhs : (↑((re : (a : K) → ℝ) z) : K) = z
⊢ (↑((re : (a : K) → ℝ) z) : K) = z
have conv_rhs₁ : Eq.{u_1 + 1} (α := K) (↑((re : (a : K) → ℝ) z) : K) (↑((re : (a : K) → ℝ) z) : K)
Tactic: conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
⊢ [(starRingEnd K : (a : K) → K) z = z, ∃ (r : ℝ), (↑r : K) = z, (↑((re : (a : K) → ℝ) z) : K) = z,
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ), IsSelfAdjoint z].TFAE
have tfae_4_to_3 : ∀ (a : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)), (↑((re : (a : K) → ℝ) z) : K) = z
Tactic: tfae_have 4 → 3
  | h => by
    conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
tfae_4_to_3 : ∀ (a : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)), (↑((re : (a : K) → ℝ) z) : K) = z
⊢ [(starRingEnd K : (a : K) → K) z = z, ∃ (r : ℝ), (↑r : K) = z, (↑((re : (a : K) → ℝ) z) : K) = z,
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ), IsSelfAdjoint z].TFAE
have tfae_3_to_2 : ∀ (a : (↑((re : (a : K) → ℝ) z) : K) = z), ∃ (r : ℝ), (↑r : K) = z
Tactic: tfae_have 3 → 2 := fun h => ⟨_, h⟩
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
tfae_4_to_3 : ∀ (a : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)), (↑((re : (a : K) → ℝ) z) : K) = z
tfae_3_to_2 : ∀ (a : (↑((re : (a : K) → ℝ) z) : K) = z), ∃ (r : ℝ), (↑r : K) = z
⊢ [(starRingEnd K : (a : K) → K) z = z, ∃ (r : ℝ), (↑r : K) = z, (↑((re : (a : K) → ℝ) z) : K) = z,
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ), IsSelfAdjoint z].TFAE
have tfae_2_to_1 : ∀ (a : ∃ (r : ℝ), (↑r : K) = z), (starRingEnd K : (a : K) → K) z = z
Tactic: tfae_have 2 → 1 := fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
tfae_4_to_3 : ∀ (a : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)), (↑((re : (a : K) → ℝ) z) : K) = z
tfae_3_to_2 : ∀ (a : (↑((re : (a : K) → ℝ) z) : K) = z), ∃ (r : ℝ), (↑r : K) = z
tfae_2_to_1 : ∀ (a : ∃ (r : ℝ), (↑r : K) = z), (starRingEnd K : (a : K) → K) z = z
h : (starRingEnd K : (a : K) → K) z = z
⊢ IsSelfAdjoint z
have rwa : star z = z
Tactic: rwa [isSelfAdjoint_iff]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
tfae_4_to_3 : ∀ (a : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)), (↑((re : (a : K) → ℝ) z) : K) = z
tfae_3_to_2 : ∀ (a : (↑((re : (a : K) → ℝ) z) : K) = z), ∃ (r : ℝ), (↑r : K) = z
tfae_2_to_1 : ∀ (a : ∃ (r : ℝ), (↑r : K) = z), (starRingEnd K : (a : K) → K) z = z
⊢ [(starRingEnd K : (a : K) → K) z = z, ∃ (r : ℝ), (↑r : K) = z, (↑((re : (a : K) → ℝ) z) : K) = z,
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ), IsSelfAdjoint z].TFAE
have tfae_1_to_5 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), IsSelfAdjoint z
Tactic: tfae_have 1 → 5 := fun _ => by rwa [isSelfAdjoint_iff]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
tfae_4_to_3 : ∀ (a : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)), (↑((re : (a : K) → ℝ) z) : K) = z
tfae_3_to_2 : ∀ (a : (↑((re : (a : K) → ℝ) z) : K) = z), ∃ (r : ℝ), (↑r : K) = z
tfae_2_to_1 : ∀ (a : ∃ (r : ℝ), (↑r : K) = z), (starRingEnd K : (a : K) → K) z = z
tfae_1_to_5 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), IsSelfAdjoint z
hz : IsSelfAdjoint z
⊢ (starRingEnd K : (a : K) → K) z = z
have rwa : ∀ (hz : star z = z), (starRingEnd K : (a : K) → K) z = z
Tactic: rwa [isSelfAdjoint_iff] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (hypothesis)
Goal:
K : Type u_1
inst : RCLike K
z : K
tfae_1_to_4 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)
tfae_4_to_3 : ∀ (a : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)), (↑((re : (a : K) → ℝ) z) : K) = z
tfae_3_to_2 : ∀ (a : (↑((re : (a : K) → ℝ) z) : K) = z), ∃ (r : ℝ), (↑r : K) = z
tfae_2_to_1 : ∀ (a : ∃ (r : ℝ), (↑r : K) = z), (starRingEnd K : (a : K) → K) z = z
tfae_1_to_5 : ∀ (a : (starRingEnd K : (a : K) → K) z = z), IsSelfAdjoint z
⊢ [(starRingEnd K : (a : K) → K) z = z, ∃ (r : ℝ), (↑r : K) = z, (↑((re : (a : K) → ℝ) z) : K) = z,
      Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ), IsSelfAdjoint z].TFAE
have tfae_5_to_1 : ∀ (a : IsSelfAdjoint z), (starRingEnd K : (a : K) → K) z = z
Tactic: tfae_have 5 → 1 := fun hz => by rwa [isSelfAdjoint_iff] at hz
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z_1 z w : K
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) (z * w) : ℝ) ((re : (a : K) → ℝ) (z * w) : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) (z * w) : ℝ) ((im : (a : K) → ℝ) (z * w) : ℝ) =
    (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ)) *
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) w : ℝ) ((re : (a : K) → ℝ) w : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) w : ℝ) ((im : (a : K) → ℝ) w : ℝ))
have simp : (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) *
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ)) +
    (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) *
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ)) =
  (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ)) *
    (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) w : ℝ) ((re : (a : K) → ℝ) w : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) w : ℝ) ((im : (a : K) → ℝ) w : ℝ))
Tactic: simp only [mul_im, mul_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ↔ z ≠ 0
have rw : LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ∧ ¬Eq (α := ℝ) ((normSq : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔ z ≠ 0
Tactic: rw [lt_iff_le_and_ne, Ne, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ (normSq : (a : K) → ℝ) (z + w) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) w : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
        ((re : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) w : K)) : ℝ)
have simp : HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) +
    HAdd.hAdd (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) w : ℝ) =
  HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ) +
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) w : ℝ) ((re : (a : K) → ℝ) w : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) w : ℝ) ((im : (a : K) → ℝ) w : ℝ)) +
    2 *
      (HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) w : ℝ) -
        HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) (-(im : (a : K) → ℝ) w : ℝ))
Tactic: simp only [normSq_apply, map_add, rclike_simps]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K) = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
have hre : Eq (α := ℝ) ((re : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K)) : ℝ)
  ((re : (a : K) → ℝ) (HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2) : ℝ)
Tactic: apply ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
hre :
  Eq (α := ℝ) ((re : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K)) : ℝ)
    ((re : (a : K) → ℝ) (HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2) : ℝ)
⊢ HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K) = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
have him : Eq (α := ℝ) ((im : (a : K) → ℝ) (HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K)) : ℝ)
  ((im : (a : K) → ℝ) (HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2) : ℝ)
Tactic: apply ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HMul.hMul (α := K) ((starRingEnd K : (a : K) → K) z : K) z = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
have rw : HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K) = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
Tactic: rw [mul_comm, mul_conj]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : HMul.hMul (β := K) z ((starRingEnd K : (a : K) → K) z : K) = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
⊢ HMul.hMul (α := K) ((starRingEnd K : (a : K) → K) z : K) z = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
have rw₁ : HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 = HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2
Tactic: rw [mul_comm, mul_conj]