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
hz : ‖z‖ = 1
⊢ HMul.hMul (α := K) ((starRingEnd K : (a : K) → K) z : K) z = 1
have simp_rw : HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 = 1
Tactic: simp_rw [conj_mul, hz, algebraMap.coe_one, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
hz : ‖z‖ = 1
simp_rw : HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 = 1
⊢ HMul.hMul (α := K) ((starRingEnd K : (a : K) → K) z : K) z = 1
have simp_rw₁ : HPow.hPow (α := K) (β := ℕ) (↑1 : K) 2 = 1
Tactic: simp_rw [conj_mul, hz, algebraMap.coe_one, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
hz : ‖z‖ = 1
simp_rw : HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 = 1
simp_rw₁ : HPow.hPow (α := K) (β := ℕ) (↑1 : K) 2 = 1
⊢ HMul.hMul (α := K) ((starRingEnd K : (a : K) → K) z : K) z = 1
have simp_rw₂ : HPow.hPow (α := K) (β := ℕ) 1 2 = 1
Tactic: simp_rw [conj_mul, hz, algebraMap.coe_one, one_pow]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ √((normSq : (a : K) → ℝ) z) = ‖z‖
have rw : √(HPow.hPow (β := ℕ) ‖z‖ 2) = ‖z‖
Tactic: rw [normSq_eq_def', Real.sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : √(HPow.hPow (β := ℕ) ‖z‖ 2) = ‖z‖
⊢ √((normSq : (a : K) → ℝ) z) = ‖z‖
have rw₁ : ‖z‖ = ‖z‖
Tactic: rw [normSq_eq_def', Real.sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ z⁻¹ = HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)
have inl : 0⁻¹ =
  HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) 0 : K)
    ((↑(HPow.hPow (β := ℕ) (norm.{u_1} (E := K) 0) 2)⁻¹ : K) : K)
Tactic: rcases eq_or_ne z 0 with (rfl | h₀)
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
inl :
  0⁻¹ =
    HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) 0 : K)
      ((↑(HPow.hPow (β := ℕ) (norm.{u_1} (E := K) 0) 2)⁻¹ : K) : K)
⊢ z⁻¹ = HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)
have inr : ∀ (h₀ : z ≠ 0),
  z⁻¹ = HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)
Tactic: rcases eq_or_ne z 0 with (rfl | h₀)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)
have inr : z * HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) = 1
Tactic: apply inv_eq_of_mul_eq_one_right
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
h₀ : z ≠ 0
⊢ z * HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) = 1
have inr : HPow.hPow (α := K) (β := ℕ) (↑‖z‖ : K) 2 ≠ 0
Tactic: rw [← mul_assoc, mul_conj, ofReal_inv, ofReal_pow, mul_inv_cancel₀]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (re : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw : (re : (a : K) → ℝ)
    (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
  HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
⊢ (re : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₁ : (re : (a : K) → ℝ)
    (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
  HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
⊢ (re : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₂ : (re : (a : K) → ℝ)
    (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
  HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₂ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
⊢ (re : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₃ : HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) =
  HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₂ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
⊢ (re : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₄ : HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) z : ℝ) =
  HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₂ :
  (re : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₄ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) z : ℝ) =
    HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
⊢ (re : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₅ : HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) z : ℝ) =
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((re : (a : K) → ℝ) z : ℝ)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (im : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw : (im : (a : K) → ℝ)
    (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
  HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
⊢ (im : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₁ : (im : (a : K) → ℝ)
    (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
  HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
⊢ (im : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₂ : (im : (a : K) → ℝ)
    (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
  HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₂ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
⊢ (im : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₃ : HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((im : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) =
  HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₂ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((im : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
⊢ (im : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₄ : HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ (-(im : (a : K) → ℝ) z : ℝ) =
  HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
rw₁ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((starRingEnd K : (a : K) → K) z : K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₂ :
  (im : (a : K) → ℝ)
      (HMul.hMul (α := K) (β := K) ((↑(HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ : K) : K) ((starRingEnd K : (a : K) → K) z : K)) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₃ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ ((im : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
rw₄ :
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ (-(im : (a : K) → ℝ) z : ℝ) =
    HDiv.hDiv (α := ℝ) (-(im : (a : K) → ℝ) z : ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)
⊢ (im : (a : K) → ℝ) z⁻¹ = HDiv.hDiv (α := ℝ) (β := ℝ) (-(im : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)
have rw₅ : HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ (-(im : (a : K) → ℝ) z : ℝ) =
  HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ‖z‖ 2)⁻¹ (-(im : (a : K) → ℝ) z : ℝ)
Tactic: rw [inv_def, normSq_eq_def', mul_comm, im_ofReal_mul, conj_im, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ ∃ (c : K), ‖c‖ = 1 ∧ (↑‖x‖ : K) = c * x
have inl : ∃ (c : K), ‖c‖ = 1 ∧ (↑(norm.{u_1} (E := K) 0) : K) = c * 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
inl : ∃ (c : K), ‖c‖ = 1 ∧ (↑(norm.{u_1} (E := K) 0) : K) = c * 0
⊢ ∃ (c : K), ‖c‖ = 1 ∧ (↑‖x‖ : K) = c * x
have inr : ∀ (hx : x ≠ 0), ∃ (c : K), ‖c‖ = 1 ∧ (↑‖x‖ : K) = c * x
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
⊢ ∃ (c : K), ‖c‖ = 1 ∧ c * (↑‖x‖ : K) = x
have inl : ∃ (c : K), ‖c‖ = 1 ∧ c * (↑(norm.{u_1} (E := K) 0) : K) = 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
x : K
inl : ∃ (c : K), ‖c‖ = 1 ∧ c * (↑(norm.{u_1} (E := K) 0) : K) = 0
⊢ ∃ (c : K), ‖c‖ = 1 ∧ c * (↑‖x‖ : K) = x
have inr : ∀ (hx : x ≠ 0), ∃ (c : K), ‖c‖ = 1 ∧ c * (↑‖x‖ : K) = x
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
r : ℝ
⊢ (re : (a : K) → ℝ) (z / (↑r : K)) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
have rw : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
r : ℝ
rw : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
⊢ (re : (a : K) → ℝ) (z / (↑r : K)) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
have rw₁ : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HMul.hMul (β := ℝ) r⁻¹ ((re : (a : K) → ℝ) z : ℝ)
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
r : ℝ
rw : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
rw₁ : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HMul.hMul (β := ℝ) r⁻¹ ((re : (a : K) → ℝ) z : ℝ)
⊢ (re : (a : K) → ℝ) (z / (↑r : K)) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
have rw₂ : (re : (a : K) → ℝ) ((↑r⁻¹ : K) * z) = HMul.hMul (β := ℝ) r⁻¹ ((re : (a : K) → ℝ) z : ℝ)
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
r : ℝ
rw : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
rw₁ : (re : (a : K) → ℝ) ((↑r : K)⁻¹ * z) = HMul.hMul (β := ℝ) r⁻¹ ((re : (a : K) → ℝ) z : ℝ)
rw₂ : (re : (a : K) → ℝ) ((↑r⁻¹ : K) * z) = HMul.hMul (β := ℝ) r⁻¹ ((re : (a : K) → ℝ) z : ℝ)
⊢ (re : (a : K) → ℝ) (z / (↑r : K)) = HDiv.hDiv (α := ℝ) ((re : (a : K) → ℝ) z : ℝ) r
have rw₃ : HMul.hMul (β := ℝ) r⁻¹ ((re : (a : K) → ℝ) z : ℝ) = HMul.hMul (β := ℝ) r⁻¹ ((re : (a : K) → ℝ) z : ℝ)
Tactic: rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq.{u_1 + 1} (α := K) I⁻¹ (-I)
have pos : ∀ (h : Eq.{u_1 + 1} (α := K) I 0), Eq.{u_1 + 1} (α := K) I⁻¹ (-I)
Tactic: by_cases h : (I : K) = 0
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
pos : ∀ (h : Eq.{u_1 + 1} (α := K) I 0), Eq.{u_1 + 1} (α := K) I⁻¹ (-I)
⊢ Eq.{u_1 + 1} (α := K) I⁻¹ (-I)
have neg : ∀ (h : ¬Eq.{u_1 + 1} (α := K) I 0), Eq.{u_1 + 1} (α := K) I⁻¹ (-I)
Tactic: by_cases h : (I : K) = 0
-- 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
⊢ Eq.{u_1 + 1} (α := K) I⁻¹ (-I)
have neg : 1 = -HPow.hPow (α := K) (β := ℕ) I 2
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ z / I = -(z * I)
have rw : z * I⁻¹ = -(z * I)
Tactic: rw [div_eq_mul_inv, inv_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : z * I⁻¹ = -(z * I)
⊢ z / I = -(z * I)
have rw₁ : z * -I = -(z * I)
Tactic: rw [div_eq_mul_inv, inv_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : z * I⁻¹ = -(z * I)
rw₁ : z * -I = -(z * I)
⊢ z / I = -(z * I)
have rw₂ : -(z * I) = -(z * I)
Tactic: rw [div_eq_mul_inv, inv_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℝ
a : K
⊢ star (r • a) = star r • star a
have hre : Eq (α := ℝ) ((re : (a : K) → ℝ) (star (r • a)) : ℝ) ((re : (a : K) → ℝ) (star r • star a) : ℝ)
Tactic: apply RCLike.ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
r : ℝ
a : K
hre : Eq (α := ℝ) ((re : (a : K) → ℝ) (star (r • a)) : ℝ) ((re : (a : K) → ℝ) (star r • star a) : ℝ)
⊢ star (r • a) = star r • star a
have him : Eq (α := ℝ) ((im : (a : K) → ℝ) (star (r • a)) : ℝ) ((im : (a : K) → ℝ) (star r • star a) : ℝ)
Tactic: apply RCLike.ext
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑n : K) : ℝ) ((↑n : ℝ) : ℝ)
have rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) ((↑n : ℝ) : ℝ)
Tactic: rw [← ofReal_natCast, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
rw : Eq (α := ℝ) ((re : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) ((↑n : ℝ) : ℝ)
⊢ Eq (α := ℝ) ((re : (a : K) → ℝ) (↑n : K) : ℝ) ((↑n : ℝ) : ℝ)
have rw₁ : Eq (α := ℝ) (↑n : ℝ) (↑n : ℝ)
Tactic: rw [← ofReal_natCast, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑n : K) : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) (0 : ℝ)
Tactic: rw [← ofReal_natCast, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
rw : Eq (α := ℝ) ((im : (a : K) → ℝ) (↑(↑n : ℝ) : K) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) (↑n : K) : ℝ) (0 : ℝ)
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_natCast, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
z : K
⊢ (re : (a : K) → ℝ) (OfNat.ofNat n * z) = HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ)
have rw : (re : (a : K) → ℝ) ((↑(OfNat.ofNat n) : K) * z) =
  HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ)
Tactic: rw [← ofReal_ofNat, re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
z : K
rw :
  (re : (a : K) → ℝ) ((↑(OfNat.ofNat n) : K) * z) =
    HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ)
⊢ (re : (a : K) → ℝ) (OfNat.ofNat n * z) = HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ)
have rw₁ : HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ) =
  HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((re : (a : K) → ℝ) z : ℝ)
Tactic: rw [← ofReal_ofNat, re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Basic (goal)
Goal:
K : Type u_1
inst : RCLike K
n : ℕ
inst_1 : n.AtLeastTwo
z : K
⊢ (im : (a : K) → ℝ) (OfNat.ofNat n * z) = HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((im : (a : K) → ℝ) z : ℝ)
have rw : (im : (a : K) → ℝ) ((↑(OfNat.ofNat n) : K) * z) =
  HMul.hMul (α := ℝ) (β := ℝ) (OfNat.ofNat n : ℝ) ((im : (a : K) → ℝ) z : ℝ)
Tactic: rw [← ofReal_ofNat, im_ofReal_mul]