awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.RCLike.Basic
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 : ℝ)
⊢ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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 : ℝ)
⊢ (↑((re : (a : K) → ℝ) z) : K) = z

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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 : ℝ)
⊢ ∀ (a : Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)), (↑((re : (a : K) → ℝ) z) : K) = z

Tactic:
4 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
rw : (↑((re : (a : K) → ℝ) z) : K)
| z

Tactic:
rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]

Premises used: RCLike.re_add_im, MulZeroClass.zero_mul, RCLike.ofReal_zero, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
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
conv_rhs₁ : Eq.{u_1 + 1} (α := K) (↑((re : (a : K) → ℝ) z) : K) (↑((re : (a : K) → ℝ) z) : K)
⊢ (↑((re : (a : K) → ℝ) z) : K) = z

Tactic:
conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]

Premises used: RCLike.re_add_im, MulZeroClass.zero_mul, RCLike.ofReal_zero, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
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 : ℝ)
⊢ ∀ (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]
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ (↑((re : (a : K) → ℝ) z) : K) = z

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∃ (r : ℝ), (↑r : K) = z

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∀ (a : (↑((re : (a : K) → ℝ) z) : K) = z), ∃ (r : ℝ), (↑r : K) = z

Tactic:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∀ (a : (↑((re : (a : K) → ℝ) z) : K) = z), ∃ (r : ℝ), (↑r : K) = z

Tactic:
tfae_have 3 → 2 := fun h => ⟨_, h⟩
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∃ (r : ℝ), (↑r : K) = z

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∀ (a : ∃ (r : ℝ), (↑r : K) = z), (starRingEnd K : (a : K) → K) z = z

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∀ (a : ∃ (r : ℝ), (↑r : K) = z), (starRingEnd K : (a : K) → K) z = z

Tactic:
tfae_have 2 → 1 := fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
-- Module: Mathlib.Analysis.RCLike.Basic
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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ IsSelfAdjoint z

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∀ (a : (starRingEnd K : (a : K) → K) z = z), IsSelfAdjoint z

Tactic:
1 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
rwa rwa₁ rwa₂ rwa₃ : star z = z
⊢ IsSelfAdjoint z

Tactic:
rwa [isSelfAdjoint_iff]

Premises used: isSelfAdjoint_iff
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∀ (a : (starRingEnd K : (a : K) → K) z = z), IsSelfAdjoint z

Tactic:
tfae_have 1 → 5 := fun _ => by rwa [isSelfAdjoint_iff]
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ IsSelfAdjoint z

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∀ (a : IsSelfAdjoint z), (starRingEnd K : (a : K) → K) z = z

Tactic:
5 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Analysis.RCLike.Basic
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (hz : star z = z), (starRingEnd K : (a : K) → K) z = z
⊢ (starRingEnd K : (a : K) → K) z = z

Tactic:
rwa [isSelfAdjoint_iff] at hz

Premises used: isSelfAdjoint_iff
-- Module: Mathlib.Analysis.RCLike.Basic
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
⊢ ∀ (a : IsSelfAdjoint z), (starRingEnd K : (a : K) → K) z = z

Tactic:
tfae_have 5 → 1 := fun hz => by rwa [isSelfAdjoint_iff] at hz
-- Module: Mathlib.Analysis.RCLike.Basic
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
tfae_5_to_1 : ∀ (a : IsSelfAdjoint 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

Tactic:
tfae_finish
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (∃ (r : ℝ), (↑r : K) = z) ↔ ∃ (r : ℝ), z = (↑r : K)

Tactic:
simp only [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (starRingEnd K : (a : K) → K) z = z ↔ (↑((re : (a : K) → ℝ) z) : K) = z

Tactic:
(is_real_TFAE z).out 0 2

Premises used: RCLike.is_real_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (starRingEnd K : (a : K) → K) z = z ↔ Eq (α := ℝ) ((im : (a : K) → ℝ) z : ℝ) (0 : ℝ)

Tactic:
(is_real_TFAE z).out 0 3

Premises used: RCLike.is_real_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := K → K) star (⇑(starRingEnd K) : (a : K) → K)

Tactic:
rfl

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

Tactic:
is_real_TFAE x |>.out 3 4

Premises used: RCLike.is_real_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
y : ℝ
hx : IsSelfAdjoint x
⊢ (re : (a : K) → ℝ) x = y ↔ x = (↑y : K)

Tactic:
simp [RCLike.ext_iff (K := K), hx, im_eq_zero_iff_isSelfAdjoint]

Premises used: RCLike.im_eq_zero_iff_isSelfAdjoint, RCLike.ext_iff
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
x : K
y : ℝ
hx : IsSelfAdjoint x
⊢ y = (re : (a : K) → ℝ) x ↔ (↑y : K) = x

Tactic:
simpa [eq_comm] using re_eq_ofReal_of_isSelfAdjoint hx

Premises used: eq_comm, RCLike.re_eq_ofReal_of_isSelfAdjoint
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) 0 : ℝ) ((re : (a : K) → ℝ) 0 : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) 0 : ℝ) ((im : (a : K) → ℝ) 0 : ℝ) =
    0

Tactic:
simp only [add_zero, mul_zero, map_zero]

Premises used: map_zero, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z : K
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) 1 : ℝ) ((re : (a : K) → ℝ) 1 : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) 1 : ℝ) ((im : (a : K) → ℝ) 1 : ℝ) =
    1

Tactic:
simp only [one_im, add_zero, mul_one, one_re, mul_zero]

Premises used: RCLike.one_re, RCLike.one_im, MulZeroClass.mul_zero, mul_one, add_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z_1 z w : K
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 : ℝ))
⊢ 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 : ℝ))

Tactic:
simp only [mul_im, mul_re]

Premises used: RCLike.mul_im, RCLike.mul_re
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
E : Type u_2
inst : RCLike K
z_1 z w : K
⊢ (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:
ring
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (normSq : (a : K) → ℝ) z =
    HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ HPow.hPow (β := ℕ) ‖z‖ 2 =
    HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : K) → ℝ) z : ℝ) ((re : (a : K) → ℝ) z : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) ((im : (a : K) → ℝ) z : ℝ) ((im : (a : K) → ℝ) z : ℝ)

Tactic:
norm_sq_eq_def_ax z

Premises used: RCLike.norm_sq_eq_def_ax
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ (normSq : (a : K) → ℝ) z = HPow.hPow (β := ℕ) ‖z‖ 2

Tactic:
norm_sq_eq_def.symm

Premises used: RCLike.norm_sq_eq_def, Eq.symm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := ℝ) ((normSq : (a : K) → ℝ) 0 : ℝ) (0 : ℝ)

Tactic:
normSq.map_zero

Premises used: MonoidWithZeroHom.map_zero, RCLike.normSq
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
⊢ Eq (α := ℝ) ((normSq : (a : K) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
normSq.map_one

Premises used: MonoidWithZeroHom.map_one, RCLike.normSq
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)

Tactic:
add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)

Premises used: mul_self_nonneg, add_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((normSq : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔ z = 0

Tactic:
map_eq_zero _

Premises used: map_eq_zero
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
rw : LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ∧ ¬Eq (α := ℝ) ((normSq : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔ z ≠ 0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ↔ z ≠ 0

Tactic:
rw [lt_iff_le_and_ne, Ne, eq_comm]

Premises used: lt_iff_le_and_ne, Ne, eq_comm
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ LE.le (α := ℝ) (0 : ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ∧ ¬Eq (α := ℝ) ((normSq : (a : K) → ℝ) z : ℝ) (0 : ℝ) ↔ z ≠ 0

Tactic:
simp [normSq_nonneg]

Premises used: RCLike.normSq_nonneg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((normSq : (a : K) → ℝ) (-z) : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)

Tactic:
simp only [normSq_eq_def', norm_neg]

Premises used: RCLike.normSq_eq_def', norm_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z : K
⊢ Eq (α := ℝ) ((normSq : (a : K) → ℝ) ((starRingEnd K : (a : K) → K) z : K) : ℝ) ((normSq : (a : K) → ℝ) z : ℝ)

Tactic:
simp only [normSq_apply, neg_mul, mul_neg, neg_neg, rclike_simps]

Premises used: neg_neg, neg_mul, RCLike.normSq_apply, mul_neg
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
⊢ (normSq : (a : K) → ℝ) (z * w) =
    HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : K) → ℝ) z : ℝ) ((normSq : (a : K) → ℝ) w : ℝ)

Tactic:
map_mul _ z w

Premises used: map_mul
-- Module: Mathlib.Analysis.RCLike.Basic
Goal:
K : Type u_1
inst : RCLike K
z w : K
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 : ℝ))
⊢ (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)) : ℝ)

Tactic:
simp only [normSq_apply, map_add, rclike_simps]

Premises used: map_add, RCLike.normSq_apply