case tfae_1_to_4
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
⊢ ↑(starRingEnd K) z = z → ↑im z = 0

K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
tfae_have 1 → 4
case tfae_4_to_3
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
⊢ ↑im z = 0 → ↑(↑re z) = z

K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
tfae_have 4 → 3
case tfae_3_to_2
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
⊢ ↑(↑re z) = z → ∃ r, ↑r = z

K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
tfae_have 3 → 2
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
case tfae_3_to_2
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
⊢ ↑(↑re z) = z → ∃ r, ↑r = z

K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
exact fun h => ⟨_, h⟩
case tfae_2_to_1
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ (∃ r, ↑r = z) → ↑(starRingEnd K) z = z

K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → ↑(starRingEnd K) z = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
tfae_have 2 → 1
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → ↑(starRingEnd K) z = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
case tfae_2_to_1
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
⊢ (∃ r, ↑r = z) → ↑(starRingEnd K) z = z

K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → ↑(starRingEnd K) z = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
exact fun ⟨r, hr⟩ => hr ▸ conj_ofReal _
no goals
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
tfae_4_to_3 : ↑im z = 0 → ↑(↑re z) = z
tfae_3_to_2 : ↑(↑re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → ↑(starRingEnd K) z = z
⊢ TFAE [↑(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(↑re z) = z, ↑im z = 0]
tfae_finish
case tfae_1_to_4
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
h : ↑(starRingEnd K) z = z
⊢ ↑im z = 0
case tfae_1_to_4
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
⊢ ↑(starRingEnd K) z = z → ↑im z = 0
intro h
no goals
case tfae_1_to_4
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
h : ↑(starRingEnd K) z = z
⊢ ↑im z = 0
rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, MulZeroClass.mul_zero, zero_div,
  ofReal_zero]
case tfae_4_to_3
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
h : ↑im z = 0
⊢ ↑(↑re z) = z
case tfae_4_to_3
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
⊢ ↑im z = 0 → ↑(↑re z) = z
intro h
no goals
case tfae_4_to_3
K : Type u_1
E : Type ?u.3632144
inst✝ : IsROrC K
z : K
tfae_1_to_4 : ↑(starRingEnd K) z = z → ↑im z = 0
h : ↑im z = 0
⊢ ↑(↑re z) = z
conv_rhs => rw [← re_add_im z, h, ofReal_zero, MulZeroClass.zero_mul, add_zero]