awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) +
      -(2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ) -
      2 * (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ z⁻¹ = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ)

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ z⁻¹.re = HDiv.hDiv (β := ℝ) z.re ((normSq : (a : ℂ) → ℝ) z : ℝ)

Tactic:
simp [inv_def, division_def, ofReal]

Premises used: Complex.inv_def, division_def, Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ z⁻¹.im = HDiv.hDiv (β := ℝ) (-z.im) ((normSq : (a : ℂ) → ℝ) z : ℝ)

Tactic:
simp [inv_def, division_def, ofReal]

Premises used: Complex.inv_def, division_def, Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ (↑r⁻¹ : ℂ).re = (↑r : ℂ)⁻¹.re ∧ (↑r⁻¹ : ℂ).im = (↑r : ℂ)⁻¹.im

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
rw : (↑0 : ℂ)⁻¹ = (↑0 : ℂ)
rw₁ : (↑0⁻¹ : ℂ) = (↑0 : ℂ)
rw₂ rw₃ : (↑0 : ℂ) = (↑0 : ℂ)
⊢ Eq (α := ℂ) 0⁻¹ 0

Tactic:
rw [← ofReal_zero, ← ofReal_inv, inv_zero]

Premises used: inv_zero, Complex.ofReal_zero, Complex.ofReal_inv
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
h : z ≠ 0
rw : z * HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₁ : HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₂ : (↑((normSq : (a : ℂ) → ℝ) z) : ℂ) * (↑((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℂ) = 1
rw₃ : (↑(HMul.hMul (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) (((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℝ)) : ℂ) = 1
rw₄ : (↑1 : ℂ) = 1
rw₅ rw₆ : Eq (α := ℂ) 1 1
⊢ z * z⁻¹ = 1

Tactic:
rw [inv_def, ← mul_assoc, mul_conj, ← ofReal_mul, mul_inv_cancel₀ (mt normSq_eq_zero.1 h),
    ofReal_one]

Premises used: mul_inv_cancel₀, mul_assoc, mt, Complex.ofReal_one, Complex.inv_def, Iff.mp, Complex.mul_conj, Complex.normSq_eq_zero, Complex.ofReal_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (z / w).re =
    HDiv.hDiv (β := ℝ) (z.re * w.re) ((normSq : (a : ℂ) → ℝ) w : ℝ) +
      HDiv.hDiv (β := ℝ) (z.im * w.im) ((normSq : (a : ℂ) → ℝ) w : ℝ)

Tactic:
simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg]

Premises used: mul_assoc, sub_eq_add_neg, div_eq_mul_inv
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (z / w).im =
    HDiv.hDiv (β := ℝ) (z.im * w.re) ((normSq : (a : ℂ) → ℝ) w : ℝ) -
      HDiv.hDiv (β := ℝ) (z.re * w.im) ((normSq : (a : ℂ) → ℝ) w : ℝ)

Tactic:
simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm]

Premises used: mul_assoc, sub_eq_add_neg, div_eq_mul_inv, add_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
q : ℚ≥0
a : re (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).re
a₁ : im (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).im
⊢ (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
q : ℚ≥0
⊢ re (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).re

Tactic:
simp [NNRat.cast_def, div_re, div_im, mul_div_mul_comm]

Premises used: NNRat.cast_def, Complex.div_im, Complex.div_re, mul_div_mul_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
q : ℚ≥0
⊢ im (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).im

Tactic:
simp [NNRat.cast_def, div_re, div_im, mul_div_mul_comm]

Premises used: NNRat.cast_def, Complex.div_im, Complex.div_re, mul_div_mul_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
n : ℚ≥0
z : ℂ
⊢ (n • z).re = ((↑n : ℂ) * z).re ∧ (n • z).im = ((↑n : ℂ) * z).im

Tactic:
simp [NNRat.smul_def, smul_re, smul_im]

Premises used: Complex.smul_re, NNRat.smul_def, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
q : ℚ
a : re (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).re
a₁ : im (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).im
⊢ (↑q : ℂ) = HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
q : ℚ
⊢ re (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).re

Tactic:
simp [Rat.cast_def, div_re, div_im, mul_div_mul_comm]

Premises used: Complex.div_im, Complex.div_re, Rat.cast_def, mul_div_mul_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
q : ℚ
⊢ im (↑q : ℂ) = (HDiv.hDiv (α := ℂ) (↑q.num : ℂ) (↑q.den : ℂ)).im

Tactic:
simp [Rat.cast_def, div_re, div_im, mul_div_mul_comm]

Premises used: Complex.div_im, Complex.div_re, Rat.cast_def, mul_div_mul_comm
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
n : ℚ
z : ℂ
⊢ (n • z).re = ((↑n : ℂ) * z).re ∧ (n • z).im = ((↑n : ℂ) * z).im

Tactic:
simp [Rat.smul_def, smul_re, smul_im]

Premises used: Complex.smul_re, Rat.smul_def, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ≥0
r : ℝ
⊢ (↑(q • r) : ℂ) = q • (↑r : ℂ)

Tactic:
simp [NNRat.smul_def]

Premises used: NNRat.smul_def
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ
r : ℝ
⊢ (↑(q • r) : ℂ) = q • (↑r : ℂ)

Tactic:
simp [Rat.smul_def]

Premises used: Rat.smul_def
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℂ
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x⁻¹ : ℂ) (((starRingEnd ℂ : (a : ℂ) → ℂ) x)⁻¹ : ℂ)

Tactic:
star_inv₀ _

Premises used: star_inv₀
-- Module: Mathlib.Data.Complex.Basic
Goal:
r s : ℝ
⊢ (↑(r / s) : ℂ) = (↑r : ℂ) / (↑s : ℂ)

Tactic:
map_div₀ ofRealHom r s

Premises used: Complex.ofRealHom, map_div₀
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
n : ℤ
⊢ (↑(r ^ n) : ℂ) = (↑r : ℂ) ^ n

Tactic:
map_zpow₀ ofRealHom r n

Premises used: Complex.ofRealHom, map_zpow₀
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ -(z * I) * I = z

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Data.Complex.Basic
Goal:
rw : 1 / I = -I
rw₁ : -(1 * I) = -I
rw₂ rw₃ : -I = -I
⊢ I⁻¹ = -I

Tactic:
rw [inv_eq_one_div, div_I, one_mul]

Premises used: inv_eq_one_div, Complex.div_I, one_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ Eq (α := ℝ) ((normSq : (a : ℂ) → ℝ) z⁻¹ : ℝ) (((normSq : (a : ℂ) → ℝ) z)⁻¹ : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (normSq : (a : ℂ) → ℝ) (z / w) =
    HDiv.hDiv (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) w : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
x : ℝ
simp_rw : (↑x : ℂ)⁻¹ * z = { re := x⁻¹ * z.re, im := x⁻¹ * z.im }
simp_rw₁ : (↑x⁻¹ : ℂ) * z = { re := x⁻¹ * z.re, im := x⁻¹ * z.im }
⊢ z / (↑x : ℂ) = { re := z.re / x, im := z.im / x }

Tactic:
simp_rw [div_eq_inv_mul, ← ofReal_inv, ofReal_mul']

Premises used: Complex.ofReal_mul', div_eq_inv_mul, Complex.ofReal_inv
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℕ
⊢ z / (↑n : ℂ) = { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) }

Tactic:
mod_cast div_ofReal z n

Premises used: Complex.im, cast, HDiv.hDiv, Nat.cast, Complex.re, Complex.div_ofReal, Eq.refl, Eq, Complex.mk
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℤ
⊢ z / (↑n : ℂ) = { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) }

Tactic:
mod_cast div_ofReal z n

Premises used: Int.cast, Complex.im, cast, HDiv.hDiv, Complex.re, Complex.div_ofReal, Eq.refl, Eq, Complex.mk
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
x : ℚ
⊢ z / (↑x : ℂ) = { re := z.re / (↑x : ℝ), im := z.im / (↑x : ℝ) }

Tactic:
mod_cast div_ofReal z x

Premises used: Complex.im, cast, HDiv.hDiv, Rat.cast, Complex.re, Complex.div_ofReal, Eq.refl, Eq, Complex.mk
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℕ
inst : n.AtLeastTwo
⊢ z / OfNat.ofNat n = { re := z.re / OfNat.ofNat n, im := z.im / OfNat.ofNat n }

Tactic:
div_natCast z n

Premises used: Complex.div_natCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
x : ℝ
rw rw₁ : { re := z.re / x, im := z.im / x : ℂ }.re = z.re / x
⊢ (z / (↑x : ℂ)).re = z.re / x

Tactic:
rw [div_ofReal]

Premises used: Complex.div_ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
x : ℝ
rw rw₁ : { re := z.re / x, im := z.im / x : ℂ }.im = z.im / x
⊢ (z / (↑x : ℂ)).im = z.im / x

Tactic:
rw [div_ofReal]

Premises used: Complex.div_ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℕ
rw rw₁ : { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) : ℂ }.re = z.re / (↑n : ℝ)
⊢ (z / (↑n : ℂ)).re = z.re / (↑n : ℝ)

Tactic:
rw [div_natCast]

Premises used: Complex.div_natCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℕ
rw rw₁ : { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) : ℂ }.im = z.im / (↑n : ℝ)
⊢ (z / (↑n : ℂ)).im = z.im / (↑n : ℝ)

Tactic:
rw [div_natCast]

Premises used: Complex.div_natCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℤ
rw rw₁ : { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) : ℂ }.re = z.re / (↑n : ℝ)
⊢ (z / (↑n : ℂ)).re = z.re / (↑n : ℝ)

Tactic:
rw [div_intCast]

Premises used: Complex.div_intCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℤ
rw rw₁ : { re := z.re / (↑n : ℝ), im := z.im / (↑n : ℝ) : ℂ }.im = z.im / (↑n : ℝ)
⊢ (z / (↑n : ℂ)).im = z.im / (↑n : ℝ)

Tactic:
rw [div_intCast]

Premises used: Complex.div_intCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
x : ℚ
rw rw₁ : { re := z.re / (↑x : ℝ), im := z.im / (↑x : ℝ) : ℂ }.re = z.re / (↑x : ℝ)
⊢ (z / (↑x : ℂ)).re = z.re / (↑x : ℝ)

Tactic:
rw [div_ratCast]

Premises used: Complex.div_ratCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
x : ℚ
rw rw₁ : { re := z.re / (↑x : ℝ), im := z.im / (↑x : ℝ) : ℂ }.im = z.im / (↑x : ℝ)
⊢ (z / (↑x : ℂ)).im = z.im / (↑x : ℝ)

Tactic:
rw [div_ratCast]

Premises used: Complex.div_ratCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℕ
inst : n.AtLeastTwo
⊢ (z / OfNat.ofNat n).re = z.re / OfNat.ofNat n

Tactic:
div_natCast_re z n

Premises used: Complex.div_natCast_re
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
n : ℕ
inst : n.AtLeastTwo
⊢ (z / OfNat.ofNat n).im = z.im / OfNat.ofNat n

Tactic:
div_natCast_im z n

Premises used: Complex.div_natCast_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
n : ℕ
h : Eq (α := ℂ) (↑n : ℂ) 0
rwa : ∀ (h : (↑(↑n : ℝ) : ℂ) = 0), n = 0
rwa₁ : ∀ (h : Eq (α := ℝ) (↑n : ℝ) 0), n = 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : n = 0), n = 0
⊢ n = 0

Tactic:
rwa [← ofReal_natCast, ofReal_eq_zero, Nat.cast_eq_zero] at h

Premises used: Complex.ofReal_eq_zero, Nat.cast_eq_zero, Complex.ofReal_natCast
-- Module: Mathlib.Data.Complex.Basic
Goal:
α : Type u_1
⊢ IsAddTorsionFree ℂ

Tactic:
IsDomain.instIsAddTorsionFreeOfCharZero _

Premises used: IsDomain.instIsAddTorsionFreeOfCharZero
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (↑z.re : ℂ) = HAdd.hAdd (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) / 2

Tactic:
simp only [add_conj, ofReal_mul, ofReal_ofNat, mul_div_cancel_left₀ (z.re : ℂ) two_ne_zero]

Premises used: mul_div_cancel_left₀, Complex.ofReal, Complex.add_conj, Complex.re, two_ne_zero, Complex.ofReal_ofNat, Complex.ofReal_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (↑z.im : ℂ) = HSub.hSub (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) / (2 * I)

Tactic:
simp only [sub_conj, ofReal_mul, ofReal_ofNat, mul_right_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]

Premises used: mul_div_cancel_left₀, Complex.sub_conj, Complex.I_ne_zero, two_ne_zero, mul_right_comm, mul_ne_zero, Complex.ofReal_ofNat, Complex.ofReal_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
s t : Set ℝ
⊢ (⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s ×ˢ t = s ×ℂ t

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, Set.inter, Complex.reProdIm, Set.preimage, rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
s s₁ t t₁ : Set ℝ
rw :
  Subset (α := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s ×ˢ t)
      ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s₁ ×ˢ t₁) ↔
    s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
rw [← @preimage_equivRealProd_prod s t, ← @preimage_equivRealProd_prod s₁ t₁]

Premises used: Complex.preimage_equivRealProd_prod
-- Module: Mathlib.Data.Complex.Basic
Goal:
s s₁ t t₁ : Set ℝ
⊢ Subset (α := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s ×ˢ t)
      ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s₁ ×ˢ t₁) ↔
    s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
Equiv.preimage_subset equivRealProd _ _

Premises used: Equiv.preimage_subset, Complex.equivRealProd
-- Module: Mathlib.Data.Complex.Basic
Goal:
s s₁ t t₁ : Set ℝ
⊢ Subset (α := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s ×ˢ t)
      ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' s₁ ×ˢ t₁) ↔
    s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
exact Equiv.preimage_subset equivRealProd _ _

Premises used: Equiv.preimage_subset, Complex.equivRealProd
-- Module: Mathlib.Data.Complex.Basic
Goal:
s s₁ t t₁ : Set ℝ
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
prod_subset_prod_iff

Premises used: Set.prod_subset_prod_iff
-- Module: Mathlib.Data.Complex.Basic
Goal:
s s₁ t t₁ : Set ℝ
h : s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
convert! prod_subset_prod_iff

Premises used: Set.prod_subset_prod_iff
-- Module: Mathlib.Data.Complex.Basic
Goal:
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
reProdIm_subset_iff

Premises used: Complex.reProdIm_subset_iff
-- Module: Mathlib.Data.Complex.Basic
Goal:
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
exact reProdIm_subset_iff

Premises used: Complex.reProdIm_subset_iff
-- Module: Mathlib.Data.Complex.Basic
Goal:
s t : Set ℝ
⊢ (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
simp [Set.Nonempty, reProdIm, Complex.exists]

Premises used: Set.Nonempty, Complex.reProdIm, Complex.exists
-- Module: Mathlib.Data.Complex.Basic
Goal:
s t : Set ℝ
⊢ s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, reProdIm_nonempty, -not_and, not_and_or]

Premises used: Complex.reProdIm_nonempty, Set.not_nonempty_iff_eq_empty, not_and_or, not_and
-- Module: Mathlib.Data.Complex.Basic
Goal:
a₁ a₂ b : ℝ
h :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x ↔
      Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
⊢ Eq (α := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]])
    ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b})

Tactic:
ext x
-- Module: Mathlib.Data.Complex.Basic
Goal:
a₁ a₂ b : ℝ
x : ℂ
h :
  Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x →
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
h₁ :
  Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x →
    Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x ↔
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x

Tactic:
constructor
-- Module: Mathlib.Data.Complex.Basic
Goal:
a₁ a₂ b : ℝ
x : ℂ
hx : Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x
h :
  ∀ (x₁ : ℝ) (hx₁ : x₁ ∈ [[a₁, a₂]]) (hx₁' : (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) x₁ = x),
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
⊢ Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x

Tactic:
obtain ⟨x₁, hx₁, hx₁'⟩ := hx
-- Module: Mathlib.Data.Complex.Basic
Goal:
a₁ a₂ b : ℝ
x : ℂ
x₁ : ℝ
hx₁ : x₁ ∈ [[a₁, a₂]]
hx₁' : (fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) x₁ = x
⊢ Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x

Tactic:
simp [← hx₁', mem_preimage, mem_prod, hx₁]

Premises used: Set.mem_prod, Set.mem_preimage
-- Module: Mathlib.Data.Complex.Basic
Goal:
a₁ a₂ b : ℝ
x : ℂ
hx : Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (β := Set ℝ) [[a₁, a₂]] {b}) x
h :
  ∀ (x₁ : ((equivRealProd : (a : ℂ) → ℝ × ℝ) x).1 ∈ [[a₁, a₂]]),
    Membership.mem (γ := Set ℂ)
      ((fun (x_1 : ℝ) ↦ (↑x_1 : ℂ) + (↑((equivRealProd : (a : ℂ) → ℝ × ℝ) x).2 : ℂ) * I) '' [[a₁, a₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((fun (x : ℝ) ↦ (↑x : ℂ) + (↑b : ℂ) * I) '' [[a₁, a₂]]) x

Tactic:
obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
-- Module: Mathlib.Data.Complex.Basic
Goal:
a₁ a₂ : ℝ
x : ℂ
x₁ : ((equivRealProd : (a : ℂ) → ℝ × ℝ) x).1 ∈ [[a₁, a₂]]
⊢ (fun (x_1 : ℝ) ↦ (↑x_1 : ℂ) + (↑((equivRealProd : (a : ℂ) → ℝ × ℝ) x).2 : ℂ) * I) x.re = x

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a₁ a₂ : ℝ
x : ℂ
x₁ : ((equivRealProd : (a : ℂ) → ℝ × ℝ) x).1 ∈ [[a₁, a₂]]
⊢ Membership.mem (γ := Set ℂ)
    ((fun (x_1 : ℝ) ↦ (↑x_1 : ℂ) + (↑((equivRealProd : (a : ℂ) → ℝ × ℝ) x).2 : ℂ) * I) '' [[a₁, a₂]]) x

Tactic:
refine ⟨x.re, x₁, by simp⟩
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b₁ b₂ : ℝ
h :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x ↔
      Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
⊢ Eq (α := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]])
    ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]])

Tactic:
ext x
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b₁ b₂ : ℝ
x : ℂ
h :
  Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x →
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
h₁ :
  Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x →
    Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x ↔
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x

Tactic:
constructor
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b₁ b₂ : ℝ
x : ℂ
hx : Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x
h :
  ∀ (x₁ : ℝ) (hx₁ : x₁ ∈ [[b₁, b₂]]) (hx₁' : (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) x₁ = x),
    Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x

Tactic:
obtain ⟨x₁, hx₁, hx₁'⟩ := hx
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b₁ b₂ : ℝ
x : ℂ
x₁ : ℝ
hx₁ : x₁ ∈ [[b₁, b₂]]
hx₁' : (fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) x₁ = x
⊢ Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x

Tactic:
simp [← hx₁', mem_preimage, mem_prod, hx₁]

Premises used: Set.mem_prod, Set.mem_preimage
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b₁ b₂ : ℝ
x : ℂ
hx : Membership.mem (γ := Set ℂ) ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) {a} [[b₁, b₂]]) x
⊢ x.im ∈ [[b₁, b₂]] ∧ a = x.re

Tactic:
simp only [equivRealProd_apply, singleton_prod, mem_image, Prod.mk.injEq,
      exists_eq_right_right, mem_preimage] at hx

Premises used: exists_eq_right_right, Complex.equivRealProd_apply, Set.mem_image, Set.singleton_prod, Prod.mk.injEq, Set.mem_preimage
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b₁ b₂ : ℝ
x : ℂ
hx : x.im ∈ [[b₁, b₂]] ∧ a = x.re
h : ∀ (x₁ : x.im ∈ [[b₁, b₂]]), Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑x.re : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x
⊢ Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑a : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x

Tactic:
obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
-- Module: Mathlib.Data.Complex.Basic
Goal:
b₁ b₂ : ℝ
x : ℂ
x₁ : x.im ∈ [[b₁, b₂]]
⊢ (fun (y : ℝ) ↦ (↑x.re : ℂ) + (↑y : ℂ) * I) x.im = x

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
b₁ b₂ : ℝ
x : ℂ
x₁ : x.im ∈ [[b₁, b₂]]
⊢ Membership.mem (γ := Set ℂ) ((fun (y : ℝ) ↦ (↑x.re : ℂ) + (↑y : ℂ) * I) '' [[b₁, b₂]]) x

Tactic:
refine ⟨x.im, x₁, by simp⟩
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ (↑(∏ i ∈ s, f i) : ℂ) = ∏ i ∈ s, (↑(f i) : ℂ)

Tactic:
map_prod ofRealHom _ _

Premises used: Complex.ofRealHom, map_prod
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ (↑(∑ i ∈ s, f i) : ℂ) = ∑ i ∈ s, (↑(f i) : ℂ)

Tactic:
map_sum ofRealHom _ _

Premises used: map_sum, Complex.ofRealHom
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ (↑(𝔼 i ∈ s, f i) : ℂ) = 𝔼 i ∈ s, (↑(f i) : ℂ)

Tactic:
map_expect ofRealHom ..

Premises used: Complex.ofRealHom, map_expect
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
inst : Fintype α
f : α → ℝ
a : α
⊢ (↑(balance f a) : ℂ) = balance (ofReal ∘ f) a

Tactic:
simp [balance]

Premises used: Fintype.balance
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
ι : Type u_2
inst : Fintype ι
f : ι → ℝ
⊢ ofReal ∘ balance f = balance (ofReal ∘ f)

Tactic:
funext <| ofReal_balance _

Premises used: Complex.ofReal_balance, funext
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℂ
⊢ re (∑ i ∈ s, f i) = ∑ i ∈ s, (f i).re

Tactic:
map_sum reAddGroupHom f s

Premises used: Complex.reAddGroupHom, map_sum
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ),
    (↑reAddGroupHom : ℂ →ₙ+ ℝ).toFun (m • x) =
      HSMul.hSMul (α := ℚ≥0) ((RingHom.id ℚ≥0 : (a : ℚ≥0) → ℚ≥0) m : ℚ≥0) ((↑reAddGroupHom : ℂ →ₙ+ ℝ).toFun x)

Tactic:
simp
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
inst : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).re = balance (re ∘ f) a

Tactic:
simp [balance]

Premises used: Fintype.balance
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
ι : Type u_2
inst : Fintype ι
f : ι → ℂ
⊢ re ∘ balance f = balance (re ∘ f)

Tactic:
funext <| re_balance _

Premises used: Complex.re_balance, funext
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℂ
⊢ im (∑ i ∈ s, f i) = ∑ i ∈ s, (f i).im

Tactic:
map_sum imAddGroupHom f s

Premises used: map_sum, Complex.imAddGroupHom
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ),
    (↑imAddGroupHom : ℂ →ₙ+ ℝ).toFun (m • x) =
      HSMul.hSMul (α := ℚ≥0) ((RingHom.id ℚ≥0 : (a : ℚ≥0) → ℚ≥0) m : ℚ≥0) ((↑imAddGroupHom : ℂ →ₙ+ ℝ).toFun x)

Tactic:
simp
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
α : Type u_1
inst : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).im = balance (im ∘ f) a

Tactic:
simp [balance]

Premises used: Fintype.balance
-- Module: Mathlib.Data.Complex.BigOperators
Goal:
ι : Type u_2
inst : Fintype ι
f : ι → ℂ
⊢ im ∘ balance f = balance (im ∘ f)

Tactic:
funext <| im_balance _

Premises used: Complex.im_balance, funext
-- Module: Mathlib.Data.Countable.Basic
Goal:
⊢ Countable ℤ

Tactic:
Countable.of_equiv ℕ Equiv.intEquivNat.symm

Premises used: Countable.of_equiv, Nat, Equiv.intEquivNat, Equiv.symm
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
⊢ Countable α ↔ Nonempty.{max 1 u} (α ↪ ℕ)

Tactic:
⟨fun ⟨⟨f, hf⟩⟩ => ⟨⟨f, hf⟩⟩, fun ⟨f⟩ => ⟨⟨f, f.2⟩⟩⟩

Premises used: Function.Embedding.mk, Function.Embedding.inj', _private.0.countable_iff_nonempty_embedding.match_2, Nonempty.intro, Function.Embedding, _private.0.countable_iff_nonempty_embedding.match_1, Nat, Countable.mk, Iff.intro, Exists.intro, Countable, Nonempty, DFunLike.coe
-- Module: Mathlib.Data.Countable.Basic
Goal:
α : Sort u
rw : ¬Countable α ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
rw₁ : ¬Nonempty.{max 1 u} (α ↪ ℕ) ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
rw₂ rw₃ : IsEmpty.{max 1 u} (α ↪ ℕ) ↔ IsEmpty.{max 1 u} (α ↪ ℕ)
⊢ Uncountable α ↔ IsEmpty.{max 1 u} (α ↪ ℕ)

Tactic:
rw [← not_countable_iff, countable_iff_nonempty_embedding, not_nonempty_iff]

Premises used: not_nonempty_iff, not_countable_iff, countable_iff_nonempty_embedding