awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  HPow.hPow (β := ℕ) ‖HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)‖ 2 = HPow.hPow (β := ℕ) ‖z - 1‖ 2
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)) : ℝ)
    ((normSq : (a : ℂ) → ℝ) (z - 1) : ℝ)

Tactic:
simp only [← normSq_eq_norm_sq] at this

Premises used: Complex.normSq_eq_norm_sq
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)) : ℝ)
    ((normSq : (a : ℂ) → ℝ) (z - 1) : ℝ)
⊢ 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

Premises used: Complex.mul_conj, Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Isometry
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) : ℂ)
⊢ 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

Premises used: map_sub
-- Module: Mathlib.Analysis.Complex.Isometry
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 : ℂ)
⊢ 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

Premises used: mul_sub, sub_mul, one_mul
-- Module: Mathlib.Analysis.Complex.Isometry
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 : ℂ)
⊢ 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

Premises used: LinearIsometry.norm_map, Complex.normSq_eq_norm_sq, Complex.mul_conj
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
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 : ℂ)
⊢ 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 (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖z‖ 2) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) -
      HSub.hSub (β := ℂ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
        ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)

Tactic:
rw [mul_conj, normSq_eq_norm_sq] at this

Premises used: Complex.normSq_eq_norm_sq, Complex.mul_conj
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
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 (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖z‖ 2) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) -
      HSub.hSub (β := ℂ) (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
        ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
⊢ HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)) =
    HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (z - 1)

Tactic:
simp only [sub_sub, sub_right_inj, mul_one, ofReal_pow, map_one] at this

Premises used: sub_right_inj, sub_sub, map_one, mul_one, Complex.ofReal_pow
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      (HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) (1 : ℂ)) =
    HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (z - 1)
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z

Tactic:
simp only [add_sub, sub_left_inj] at this

Premises used: add_sub, sub_left_inj
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
this :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z
rw :
  HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) z =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
rw₁ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
rw₂ rw₃ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
⊢ HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)

Tactic:
rw [add_comm, ← this, add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
h₃ :
  ∀ (z : ℂ),
    HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
      HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)
⊢ re ((f : (a : ℂ) → ℂ) z) = z.re

Tactic:
apply LinearIsometry.re_apply_eq_re_of_add_conj_eq

Premises used: LinearIsometry.re_apply_eq_re_of_add_conj_eq
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ →ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
⊢ ∀ (z : ℂ),
    HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) =
      HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℂ) → ℂ) z : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : ℂ) → ℂ) z : ℂ) : ℂ)

Tactic:
apply LinearIsometry.im_apply_eq_im h

Premises used: LinearIsometry.im_apply_eq_im
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
simp : re ((f : (a : ℂ) → ℂ) I) = 0 ∧ (im ((f : (a : ℂ) → ℂ) I) = I.im ∨ im ((f : (a : ℂ) → ℂ) I) = -I.im)
⊢ (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I

Tactic:
simp only [Complex.ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]

Premises used: and_or_left, Complex.I_re, Complex.ext_iff, Complex.neg_re, neg_zero, Complex.neg_im
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
left : re ((f : (a : ℂ) → ℂ) I) = 0
right : im ((f : (a : ℂ) → ℂ) I) = I.im ∨ im ((f : (a : ℂ) → ℂ) I) = -I.im
⊢ re ((f : (a : ℂ) → ℂ) I) = 0 ∧ (im ((f : (a : ℂ) → ℂ) I) = I.im ∨ im ((f : (a : ℂ) → ℂ) I) = -I.im)

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
⊢ re ((f : (a : ℂ) → ℂ) I) = I.re

Tactic:
@LinearIsometry.re_apply_eq_re f.toLinearIsometry h I

Premises used: LinearIsometry.re_apply_eq_re, Complex.I
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
⊢ re ((f : (a : ℂ) → ℂ) I) = I.re

Tactic:
exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I

Premises used: LinearIsometry.re_apply_eq_re, Complex.I
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
right : ∀ (z : ℂ), re ((f.toLinearIsometry : (a : ℂ) → ℂ) z) = z.re
⊢ im ((f : (a : ℂ) → ℂ) I) = I.im ∨ im ((f : (a : ℂ) → ℂ) I) = -I.im

Tactic:
apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry

Premises used: LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
z : ℂ
right right₁ : z.re = z.re
⊢ re ((f.toLinearIsometry : (a : ℂ) → ℂ) z) = z.re

Tactic:
rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]

Premises used: LinearIsometry.re_apply_eq_re
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
⊢ (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I

Tactic:
have h0 : f I = I ∨ f I = -I := by
    simp only [Complex.ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]
    constructor
    · rw [← I_re]
      exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I
    · apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry
      intro z
      rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
⊢ f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLIE

Tactic:
h0.imp (fun h' : f I = I => ?_) fun h' : f I = -I => ?_

Premises used: Or.imp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
refine_1 : ∀ (h' : (f : (a : ℂ) → ℂ) I = I), f = LinearIsometryEquiv.refl ℝ ℂ
refine_2 : ∀ (h' : (f : (a : ℂ) → ℂ) I = -I), f = conjLIE
⊢ f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLIE

Tactic:
refine h0.imp (fun h' : f I = I => ?_) fun h' : f I = -I => ?_

Premises used: Or.imp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = I
refine_1 : f.toLinearEquiv = LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl ℝ ℂ)
⊢ f = LinearIsometryEquiv.refl ℝ ℂ

Tactic:
apply LinearIsometryEquiv.toLinearEquiv_injective

Premises used: LinearIsometryEquiv.toLinearEquiv_injective
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = I
refine_1 :
  ∀ (i : Fin 2),
    Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) : ℂ)
      ((LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
          ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) :
        ℂ)
⊢ f.toLinearEquiv = LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl ℝ ℂ)

Tactic:
apply Complex.basisOneI.ext'

Premises used: Complex.basisOneI, Module.Basis.ext'
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = I
i : Fin 2
refine_1 :
  Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℂ) : ℂ)
    ((LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
        ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℂ) :
      ℂ)
refine_1₁ :
  Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℂ) : ℂ)
    ((LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
        ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℂ) :
      ℂ)
⊢ Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) : ℂ)
    ((LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
        ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) :
      ℂ)

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = I
⊢ Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℂ) : ℂ)
    ((LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
        ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℂ) :
      ℂ)

Tactic:
simp [h, h']
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = I
⊢ Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℂ) : ℂ)
    ((LinearIsometryEquiv.toLinearEquiv (LinearIsometryEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
        ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℂ) :
      ℂ)

Tactic:
simp [h, h']
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = -I
refine_2 : f.toLinearEquiv = conjLIE.toLinearEquiv
⊢ f = conjLIE

Tactic:
apply LinearIsometryEquiv.toLinearEquiv_injective

Premises used: LinearIsometryEquiv.toLinearEquiv_injective
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = -I
refine_2 :
  ∀ (i : Fin 2),
    Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) : ℂ)
      ((conjLIE.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) : ℂ)
⊢ f.toLinearEquiv = conjLIE.toLinearEquiv

Tactic:
apply Complex.basisOneI.ext'

Premises used: Complex.basisOneI, Module.Basis.ext'
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = -I
i : Fin 2
refine_2 :
  Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℂ) : ℂ)
    ((conjLIE.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℂ) : ℂ)
refine_2₁ :
  Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℂ) : ℂ)
    ((conjLIE.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℂ) : ℂ)
⊢ Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) : ℂ)
    ((conjLIE.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) i : ℂ) : ℂ)

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = -I
⊢ Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℂ) : ℂ)
    ((conjLIE.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℂ) : ℂ)

Tactic:
simp [h, h']
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ) (1 : ℂ)
h0 : (f : (a : ℂ) → ℂ) I = I ∨ (f : (a : ℂ) → ℂ) I = -I
h' : (f : (a : ℂ) → ℂ) I = -I
⊢ Eq (α := ℂ) ((f.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℂ) : ℂ)
    ((conjLIE.toLinearEquiv : (a : ℂ) → ℂ) ((basisOneI : (a : Fin 2) → ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℂ) : ℂ)

Tactic:
simp [h, h']
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ Membership.mem (α := ℂ) (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) ((f : (a : ℂ) → ℂ) 1 : ℂ)

Tactic:
simp [Submonoid.unitSphere, f.norm_map]

Premises used: LinearIsometryEquiv.norm_map, Submonoid.unitSphere
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle :=
  Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((f : (a : ℂ) → ℂ) 1) ⋯
h : f = (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a ∨ f = conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)
⊢ ∃ (a : Circle),
    f = (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a ∨ f = conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)

Tactic:
use a
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle :=
  Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((f : (a : ℂ) → ℂ) 1) ⋯
⊢ Eq (α := ℂ) ((f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : (a : ℂ) → ℂ) 1 : ℂ)
    (1 : ℂ)

Tactic:
simpa [a] using rotation_apply a⁻¹ (f 1)

Premises used: rotation_apply, Inv.inv, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle :=
  Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((f : (a : ℂ) → ℂ) 1) ⋯
⊢ Eq (α := ℂ) ((f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : (a : ℂ) → ℂ) 1 : ℂ)
    (1 : ℂ)

Tactic:
have : (f.trans (rotation a).symm) 1 = 1 := by simpa [a] using rotation_apply a⁻¹ (f 1)
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle :=
  Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((f : (a : ℂ) → ℂ) 1) ⋯
this :
  Eq (α := ℂ) ((f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : (a : ℂ) → ℂ) 1 : ℂ)
    (1 : ℂ)
⊢ f = (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a ∨ f = conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)

Tactic:
(linear_isometry_complex_aux this).imp (fun h₁ => ?_) fun h₂ => ?_

Premises used: linear_isometry_complex_aux, Or.imp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle :=
  Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((f : (a : ℂ) → ℂ) 1) ⋯
this :
  Eq (α := ℂ) ((f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : (a : ℂ) → ℂ) 1 : ℂ)
    (1 : ℂ)
h :
  ∀ (h₁ : f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) = LinearIsometryEquiv.refl ℝ ℂ),
    f = (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a
h₁ :
  ∀ (h₂ : f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) = conjLIE),
    f = conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)
⊢ f = (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a ∨ f = conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)

Tactic:
refine (linear_isometry_complex_aux this).imp (fun h₁ => ?_) fun h₂ => ?_

Premises used: linear_isometry_complex_aux, Or.imp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle :=
  Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((f : (a : ℂ) → ℂ) 1) ⋯
this :
  Eq (α := ℂ) ((f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : (a : ℂ) → ℂ) 1 : ℂ)
    (1 : ℂ)
h₁ : f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) = LinearIsometryEquiv.refl ℝ ℂ
⊢ f = (rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a

Tactic:
simpa using eq_mul_of_inv_mul_eq h₁

Premises used: eq_mul_of_inv_mul_eq
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle :=
  Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((f : (a : ℂ) → ℂ) 1) ⋯
this :
  Eq (α := ℂ) ((f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : (a : ℂ) → ℂ) 1 : ℂ)
    (1 : ℂ)
h₂ : f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) = conjLIE
⊢ f = conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)

Tactic:
eq_mul_of_inv_mul_eq h₂

Premises used: eq_mul_of_inv_mul_eq
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : Circle :=
  Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Submonoid ℂ) (Submonoid.unitSphere ℂ) x) ((f : (a : ℂ) → ℂ) 1) ⋯
this :
  Eq (α := ℂ) ((f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : (a : ℂ) → ℂ) 1 : ℂ)
    (1 : ℂ)
h₂ : f.trans (LinearIsometryEquiv.symm ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) = conjLIE
⊢ f = conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)

Tactic:
exact eq_mul_of_inv_mul_eq h₂

Premises used: eq_mul_of_inv_mul_eq
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
⊢ HPow.hPow (β := ℕ) (↑a : ℂ).re 2 + HPow.hPow (β := ℕ) (↑a : ℂ).im 2 ≠ 0

Tactic:
simp [pow_two, ← normSq_apply]

Premises used: pow_two, Complex.normSq_apply