awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.IsIntegral (goal)
Goal:
rw :
  eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
⊢ eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
have rw₁ : HPow.hPow (β := ℕ) I 2 + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
Tactic: rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.IsIntegral (goal)
Goal:
rw :
  eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₁ : HPow.hPow (β := ℕ) I 2 + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
⊢ eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
have rw₂ : HAdd.hAdd (β := ℂ) (HPow.hPow (β := ℕ) I 2) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
Tactic: rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.IsIntegral (goal)
Goal:
rw :
  eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₁ : HPow.hPow (β := ℕ) I 2 + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₂ : HAdd.hAdd (β := ℂ) (HPow.hPow (β := ℕ) I 2) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
⊢ eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
have rw₃ : HAdd.hAdd (α := ℂ) (β := ℂ) (-1 : ℂ) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
Tactic: rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.IsIntegral (goal)
Goal:
rw :
  eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₁ : HPow.hPow (β := ℕ) I 2 + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₂ : HAdd.hAdd (β := ℂ) (HPow.hPow (β := ℕ) I 2) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
rw₃ : HAdd.hAdd (α := ℂ) (β := ℂ) (-1 : ℂ) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
⊢ eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
have rw₄ : HAdd.hAdd (α := ℂ) (-1) (↑1 : ℂ) = 0
Tactic: rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.IsIntegral (goal)
Goal:
rw :
  eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₁ : HPow.hPow (β := ℕ) I 2 + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₂ : HAdd.hAdd (β := ℂ) (HPow.hPow (β := ℕ) I 2) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
rw₃ : HAdd.hAdd (α := ℂ) (β := ℂ) (-1 : ℂ) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
rw₄ : HAdd.hAdd (α := ℂ) (-1) (↑1 : ℂ) = 0
⊢ eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
have rw₅ : HAdd.hAdd (α := ℂ) (-1) 1 = 0
Tactic: rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.IsIntegral (goal)
Goal:
rw :
  eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2) + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₁ : HPow.hPow (β := ℕ) I 2 + eval₂ (algebraMap ℤ ℂ) I ((C : (a : ℤ) → ℤ[X]) 1) = 0
rw₂ : HAdd.hAdd (β := ℂ) (HPow.hPow (β := ℕ) I 2) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
rw₃ : HAdd.hAdd (α := ℂ) (β := ℂ) (-1 : ℂ) ((algebraMap ℤ ℂ : (a : ℤ) → ℂ) 1 : ℂ) = 0
rw₄ : HAdd.hAdd (α := ℂ) (-1) (↑1 : ℂ) = 0
rw₅ : HAdd.hAdd (α := ℂ) (-1) 1 = 0
⊢ eval₂ (algebraMap ℤ ℂ) I (HPow.hPow (α := ℤ[X]) (β := ℕ) X 2 + (C : (a : ℤ) → ℤ[X]) 1) = 0
have rw₆ : Eq (α := ℂ) 0 0
Tactic: rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
x : ℂ
⊢ ‖(↑a : ℂ) * x‖ = ‖x‖
have rw : ‖(↑a : ℂ)‖ * ‖x‖ = ‖x‖
Tactic: rw [norm_mul, Circle.norm_coe, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
x : ℂ
rw : ‖(↑a : ℂ)‖ * ‖x‖ = ‖x‖
⊢ ‖(↑a : ℂ) * x‖ = ‖x‖
have rw₁ : 1 * ‖x‖ = ‖x‖
Tactic: rw [norm_mul, Circle.norm_coe, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a : Circle
x : ℂ
rw : ‖(↑a : ℂ)‖ * ‖x‖ = ‖x‖
rw₁ : 1 * ‖x‖ = ‖x‖
⊢ ‖(↑a : ℂ) * x‖ = ‖x‖
have rw₂ : ‖x‖ = ‖x‖
Tactic: rw [norm_mul, Circle.norm_coe, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
a b : Circle
⊢ Eq (α := ℂ ≃ₗᵢ[ℝ] ℂ)
    (LinearIsometryEquiv.trans (E₂ := ℂ) ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)
      ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) b))
    ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) (b * a))
have h : ∀ (x : ℂ),
  Eq (α := ℂ)
    ((LinearIsometryEquiv.trans (E₂ := ℂ) ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)
            ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) b) :
          (a : ℂ) → ℂ)
        x :
      ℂ)
    ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) (b * a) : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) x : ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
⊢ False
have h1 : Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) 1 : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
Tactic: have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) 1 : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
⊢ False
have hI : Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
  ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
Tactic: have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) 1 : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
hI :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
⊢ False
have h1₁ : (↑a : ℂ) = 1
Tactic: rw [rotation_apply, map_one, mul_one] at h1
Cleared hypotheses: h1, hI
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
a : Circle
h : (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a = conjLIE
h1 : (↑a : ℂ) = 1
hI :
  Eq (α := ℂ) ((((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a : ℂ ≃ₗᵢ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
⊢ False
have hI₁ : Eq (α := ℂ) 1 0
Tactic: rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
have h₁ : norm (E := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) = ‖z‖
Tactic: have h₁ := f.norm_map z
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : norm (E := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) = ‖z‖
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
have h₃ : √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)
Tactic: simp only [norm_def] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
have rwa : ∀ (h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)),
  im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
Tactic: rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z,
    h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)
rwa :
  ∀ (h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
have rwa₁ : ∀
  (h₁ :
    re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
      (normSq : (a : ℂ) → ℝ) z),
  im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
Tactic: rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z,
    h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)
rwa :
  ∀ (h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₁ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        (normSq : (a : ℂ) → ℝ) z),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
have rwa₂ : ∀
  (h₁ :
    re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
      z.re * z.re + z.im * z.im),
  im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
Tactic: rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z,
    h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)
rwa :
  ∀ (h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₁ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        (normSq : (a : ℂ) → ℝ) z),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₂ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        z.re * z.re + z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
have rwa₃ : ∀ (h₁ : z.re * z.re + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) = z.re * z.re + z.im * z.im),
  im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
Tactic: rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z,
    h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)
rwa :
  ∀ (h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₁ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        (normSq : (a : ℂ) → ℝ) z),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₂ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        z.re * z.re + z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₃ :
  ∀ (h₁ : z.re * z.re + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) = z.re * z.re + z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
have rwa₄ : ∀ (h₁ : im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) = z.im * z.im),
  im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
Tactic: rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z,
    h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), re ((f : (a : ℂ) → ℂ) z) = z.re
z : ℂ
h₁ : √((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ)) = √((normSq : (a : ℂ) → ℝ) z)
rwa :
  ∀ (h₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₁ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        (normSq : (a : ℂ) → ℝ) z),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₂ :
  ∀
    (h₁ :
      re ((f : (a : ℂ) → ℂ) z) * re ((f : (a : ℂ) → ℂ) z) + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) =
        z.re * z.re + z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₃ :
  ∀ (h₁ : z.re * z.re + im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) = z.re * z.re + z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
rwa₄ :
  ∀ (h₁ : im ((f : (a : ℂ) → ℂ) z) * im ((f : (a : ℂ) → ℂ) z) = z.im * z.im),
    im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
⊢ im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
have rwa₅ : ∀ (h₁ : im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im),
  im ((f : (a : ℂ) → ℂ) z) = z.im ∨ im ((f : (a : ℂ) → ℂ) z) = -z.im
Tactic: rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z,
    h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
⊢ ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = ‖z - 1‖
have rw : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = norm (E := ℂ) ((f : (a : ℂ) → ℂ) (z - 1) : ℂ)
Tactic: rw [← f.norm_map (z - 1), f.map_sub, h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
rw : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = norm (E := ℂ) ((f : (a : ℂ) → ℂ) (z - 1) : ℂ)
⊢ ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = ‖z - 1‖
have rw₁ : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ =
  ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ)‖
Tactic: rw [← f.norm_map (z - 1), f.map_sub, h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (goal)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
rw : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = norm (E := ℂ) ((f : (a : ℂ) → ℂ) (z - 1) : ℂ)
rw₁ :
  ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ =
    ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ)‖
⊢ ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = ‖z - 1‖
have rw₂ : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ =
  ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖
Tactic: rw [← f.norm_map (z - 1), f.map_sub, h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
⊢ HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
have this : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = ‖z - 1‖
Tactic: have : ‖f z - 1‖ = ‖z - 1‖ := by rw [← f.norm_map (z - 1), f.map_sub, h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this : ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ = ‖z - 1‖
⊢ HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
have this₁ : HPow.hPow (β := ℕ) ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ 2 = HPow.hPow (β := ℕ) ‖z - 1‖ 2
Tactic: apply_fun fun x => x ^ 2 at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  HPow.hPow (β := ℕ) ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ 2 = HPow.hPow (β := ℕ) ‖z - 1‖ 2
⊢ HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
have this₁ : Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)) : ℝ)
  ((normSq : (a : ℂ) → ℝ) (z - 1) : ℝ)
Tactic: simp only [← normSq_eq_norm_sq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)) : ℝ)
    ((normSq : (a : ℂ) → ℝ) (z - 1) : ℝ)
⊢ HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
have this₁ : HMul.hMul (β := ℂ) (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ))
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)) : ℂ) =
  HMul.hMul (β := ℂ) (z - 1) ((starRingEnd ℂ : (a : ℂ) → ℂ) (z - 1) : ℂ)
Tactic: rw [← ofReal_inj, ← mul_conj, ← mul_conj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  HMul.hMul (β := ℂ) (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)) : ℂ) =
    HMul.hMul (β := ℂ) (z - 1) ((starRingEnd ℂ : (a : ℂ) → ℂ) (z - 1) : ℂ)
⊢ HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
have this₁ : HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ) *
    HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ) =
  (z - 1) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
Tactic: rw [map_sub, map_sub] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ) *
      HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ) =
    (z - 1) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
⊢ HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
have this₁ : HSub.hSub (β := ℂ)
      (HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ) -
    HSub.hSub (β := ℂ) (HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ) =
  HSub.hSub (β := ℂ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) -
    HSub.hSub (β := ℂ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
Tactic: simp only [sub_mul, mul_sub, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Isometry (hypothesis)
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  HSub.hSub (β := ℂ)
        (HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ))
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ) -
      HSub.hSub (β := ℂ) (HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
        ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ) =
    HSub.hSub (β := ℂ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
        ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) -
      HSub.hSub (β := ℂ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
        ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
⊢ HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
have this₁ : HSub.hSub (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖z‖ 2) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ) -
    HSub.hSub (β := ℂ) (HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ) =
  HSub.hSub (β := ℂ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) -
    HSub.hSub (β := ℂ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
Tactic: rw [mul_conj, normSq_eq_norm_sq, LinearIsometry.norm_map] at this
Cleared hypotheses: this