awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
⊢ count true l ≤ count false l + 1

Tactic:
hl.count_not_le_count_add_one false

Premises used: Bool.false, List.IsChain.count_not_le_count_add_one
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
rw : 2 * count b l = count (!b) l + count b l
rw₁ : 2 * count b l = count b l + count b l
rw₂ rw₃ : count b l + count b l = count b l + count b l
⊢ 2 * count b l = l.length

Tactic:
rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]

Premises used: two_mul, List.count_not_add_count, List.IsChain.count_not_eq_count
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
pos :
  ∀ (h2 : Even l.length),
    2 * count b l =
      if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1
neg :
  ∀ (h2 : ¬Even l.length),
    2 * count b l =
      if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
by_cases h2 : Even (length l)

Premises used: Even, List.length
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
h2 : Even l.length
pos : 2 * count b l = l.length
pos₁ pos₂ : l.length = l.length
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
rw [if_pos h2, hl.two_mul_count_bool_of_even h2]

Premises used: if_pos, List.IsChain.two_mul_count_bool_of_even
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
h2 : ¬Even l.length
neg :
  ∀ (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []) (h2 : ¬Even (length (α := Bool) [])),
    2 * count b [] =
      if Even (length (α := Bool) []) then length (α := Bool) []
      else if (some b == head? []) = true then length (α := Bool) [] + 1 else length (α := Bool) [] - 1
neg₁ :
  ∀ (x : Bool) (l : List Bool) (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) (x :: l)) (h2 : ¬Even (x :: l).length),
    2 * count b (x :: l) =
      if Even (x :: l).length then (x :: l).length
      else if (some b == (x :: l).head?) = true then (x :: l).length + 1 else (x :: l).length - 1
⊢ 2 * count b l = if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
rcases l with - | ⟨x, l⟩
-- Module: Mathlib.Data.Bool.Count
Goal:
b : Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []
h2 : ¬Even (length (α := Bool) [])
⊢ 2 * count b [] =
    if Even (length (α := Bool) []) then length (α := Bool) []
    else if (some b == head? []) = true then length (α := Bool) [] + 1 else length (α := Bool) [] - 1

Tactic:
(h2 .zero).elim

Premises used: Even.zero, False.elim
-- Module: Mathlib.Data.Bool.Count
Goal:
b : Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []
h2 : ¬Even (length (α := Bool) [])
⊢ 2 * count b [] =
    if Even (length (α := Bool) []) then length (α := Bool) []
    else if (some b == head? []) = true then length (α := Bool) [] + 1 else length (α := Bool) [] - 1

Tactic:
exact (h2 .zero).elim

Premises used: Even.zero, False.elim
-- Module: Mathlib.Data.Bool.Count
Goal:
b x : Bool
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) (x :: l)
h2 : ¬Even (x :: l).length
⊢ 2 * count b (x :: l) =
    if Even (x :: l).length then (x :: l).length
    else if (some b == (x :: l).head?) = true then (x :: l).length + 1 else (x :: l).length - 1

Tactic:
grind [hl.tail.two_mul_count_bool_of_even]

Premises used: List.IsChain.tail, List.IsChain.two_mul_count_bool_of_even
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
⊢ l.length - 1 ≤ 2 * count b l

Tactic:
grind [hl.two_mul_count_bool_eq_ite]

Premises used: List.IsChain.two_mul_count_bool_eq_ite
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
rw : l.length - HSub.hSub (α := ℕ) 2 1 ≤ 2 * count b l
⊢ l.length / 2 ≤ count b l

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred two_pos, ← tsub_le_iff_right]

Premises used: two_pos, tsub_le_iff_right, Nat.div_le_iff_le_mul_add_pred
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
⊢ l.length - HSub.hSub (α := ℕ) 2 1 ≤ 2 * count b l

Tactic:
length_sub_one_le_two_mul_count_bool hl b

Premises used: List.IsChain.length_sub_one_le_two_mul_count_bool
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
⊢ l.length - HSub.hSub (α := ℕ) 2 1 ≤ 2 * count b l

Tactic:
exact length_sub_one_le_two_mul_count_bool hl b

Premises used: List.IsChain.length_sub_one_le_two_mul_count_bool
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
⊢ 2 * count b l ≤ l.length + 1

Tactic:
grind [hl.two_mul_count_bool_eq_ite]

Premises used: List.IsChain.two_mul_count_bool_eq_ite
-- Module: Mathlib.Data.Bool.Set
Goal:
⊢ Eq (α := Set Bool) univ {false, true}

Tactic:
grind
-- Module: Mathlib.Data.Bool.Set
Goal:
α : Type u_1
f : Bool → α
⊢ range f = {f false, f true}

Tactic:
grind [cases Bool]

Premises used: Bool
-- Module: Mathlib.Data.Bool.Set
Goal:
b : Bool
⊢ Eq (α := Set Bool) {b}ᶜ {!b}

Tactic:
grind [cases Bool]

Premises used: Bool
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
x x' : B
h : x = x'
b : E x
subst : mk' (E := E) F x (cast ⋯ b) = mk (E := E) x b
⊢ mk' (E := E) F x' (cast ⋯ b) = mk (E := E) x b

Tactic:
subst h
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
x : B
b : E x
⊢ mk' (E := E) F x (cast ⋯ b) = mk (E := E) x b

Tactic:
rfl
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
y y' : E b
⊢ mk' (E := E) F b y = mk' (E := E) F b y' ↔ y = y'

Tactic:
simp [TotalSpace.ext_iff]

Premises used: Bundle.TotalSpace.ext_iff
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ Injective (α := E b) (β := TotalSpace F E) (mk (E := E) b)

Tactic:
fun _ _ ↦
  mk_inj.1

Premises used: Bundle.TotalSpace.mk_inj, Iff.mp, Function.Injective
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
z : TotalSpace F E
⊢ mk (E := E) (z.proj (E := E)) (z.snd (E := E)) = z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
p : TotalSpace F E → Prop
⊢ (∃ (x : TotalSpace F E), p x) ↔ ∃ (b : B), ∃ (y : E b), p (mk (E := E) b y)

Tactic:
⟨fun ⟨x, hx⟩ ↦ ⟨x.1, x.2, hx⟩, fun ⟨b, y, h⟩ ↦ ⟨⟨b, y⟩, h⟩⟩

Premises used: Exists, Bundle.TotalSpace.mk, _private.0.Bundle.TotalSpace.exists.match_1, Bundle.TotalSpace.proj, _private.0.Bundle.TotalSpace.exists.match_2, Iff.intro, Exists.intro, Bundle.TotalSpace.snd
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
h₁ : Subset (α := Set (TotalSpace F E)) (range (mk (E := E) b)) (proj (E := E) ⁻¹' {b})
h₂ : Subset (α := Set (TotalSpace F E)) (proj (E := E) ⁻¹' {b}) (range (mk (E := E) b))
⊢ Eq (α := Set (TotalSpace F E)) (range (mk (E := E) b)) (proj (E := E) ⁻¹' {b})

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
x : E b
⊢ Membership.mem (γ := Set (TotalSpace F E)) (proj (E := E) ⁻¹' {b}) (mk (E := E) b x)

Tactic:
rfl
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
proj : B
x : E proj
⊢ Membership.mem (γ := Set (TotalSpace F E))
    (range (mk (E := E) (TotalSpace.proj.{u_1, u_2, u_3} (F := F) (E := E) (mk (E := E) proj x)))) (mk (E := E) proj x)

Tactic:
⟨x, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
proj : B
x : E proj
⊢ Membership.mem (γ := Set (TotalSpace F E))
    (range (mk (E := E) (TotalSpace.proj.{u_1, u_2, u_3} (F := F) (E := E) (mk (E := E) proj x)))) (mk (E := E) proj x)

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.Data.Bundle
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
B' : Type u_4
f : B' → B
x : B'
y : E (f x)
⊢ lift (E := E) f (TotalSpace.mk' (E := f *ᵖ E) F x y) = TotalSpace.mk (E := E) (f x) y

Tactic:
rfl

Premises used: Bundle.Pullback.lift, rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
p : ℂ → Prop
⊢ (∀ (x : ℂ), p x) ↔ ∀ (a b : ℝ), p { re := a, im := b }

Tactic:
aesop
-- Module: Mathlib.Data.Complex.Basic
Goal:
p : ℂ → Prop
⊢ (∃ (x : ℂ), p x) ↔ ∃ (a : ℝ) (b : ℝ), p { re := a, im := b }

Tactic:
aesop
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Surjective re

Tactic:
fun x => ⟨⟨x, 0⟩, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, Complex.mk, Function.Surjective, rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Surjective im

Tactic:
fun y => ⟨⟨0, y⟩, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, Complex.mk, Function.Surjective, rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ range re = univ

Tactic:
re_surjective.range_eq

Premises used: Function.Surjective.range_eq, Complex.re_surjective
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ range im = univ

Tactic:
im_surjective.range_eq

Premises used: Function.Surjective.range_eq, Complex.im_surjective
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ (↑r : ℂ).re = r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ (↑r : ℂ).im = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
⊢ (↑r : ℂ) = { re := r, im := 0 }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℝ
⊢ z = w → (↑z : ℂ) = (↑w : ℂ)

Tactic:
apply congrArg

Premises used: congrArg
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Injective ofReal

Tactic:
fun _ _ => congrArg re

Premises used: congrArg, Complex.re, Function.Injective
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
s t : Set ℝ
⊢ z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Complex.reProdIm, Set.preimage
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ re 0 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ im 0 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ (↑0 : ℂ) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℝ
⊢ (↑z : ℂ) = 0 ↔ z = 0

Tactic:
ofReal_inj

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℝ
⊢ (↑z : ℂ) ≠ 0 ↔ z ≠ 0

Tactic:
not_congr ofReal_eq_zero

Premises used: Complex.ofReal_eq_zero, not_congr
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ re 1 = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ im 1 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ (↑1 : ℂ) = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℝ
⊢ (↑z : ℂ) = 1 ↔ z = 1

Tactic:
ofReal_inj

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℝ
⊢ (↑z : ℂ) ≠ 1 ↔ z ≠ 1

Tactic:
not_congr ofReal_eq_one

Premises used: Complex.ofReal_eq_one, not_congr
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (z + w).re = z.re + w.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (z + w).im = z.im + w.im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
r s : ℝ
⊢ (↑(r + s) : ℂ).re = ((↑r : ℂ) + (↑s : ℂ)).re ∧ (↑(r + s) : ℂ).im = ((↑r : ℂ) + (↑s : ℂ)).im

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (-z).re = -z.re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (-z).im = -z.im

Tactic:
rfl

Premises used: rfl
-- 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:
x₁ x₂ y₁ y₂ : ℝ
⊢ { re := x₁, im := y₁ : ℂ } * { re := x₂, im := y₂ : ℂ } = { re := x₁ * x₂ - y₁ * y₂, im := x₁ * y₂ + y₁ * x₂ }

Tactic:
(rfl)

Premises used: Complex.mulAux, rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (z * w).re = z.re * w.re - z.im * w.im

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
z w : ℂ
⊢ (z * w).im = z.re * w.im + z.im * w.re

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
r s : ℝ
⊢ (↑(r * s) : ℂ).re = ((↑r : ℂ) * (↑s : ℂ)).re ∧ (↑(r * s) : ℂ).im = ((↑r : ℂ) * (↑s : ℂ)).im

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
z : ℂ
⊢ ((↑r : ℂ) * z).re = r * z.re

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
z : ℂ
⊢ ((↑r : ℂ) * z).im = r * z.im

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
r : ℝ
⊢ (z * (↑r : ℂ)).re = z.re * r

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
r : ℝ
⊢ (z * (↑r : ℂ)).im = z.im * r

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
r : ℝ
z : ℂ
⊢ (↑r : ℂ) * z = { re := r * z.re, im := r * z.im }

Tactic:
ext (re_ofReal_mul _ _) (im_ofReal_mul _ _)

Premises used: Complex.ext, Complex.im_ofReal_mul, Complex.re_ofReal_mul
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ I.re = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ I.im = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ (I * I).re = re (-1) ∧ (I * I).im = im (-1)

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (I * z).re = { re := -z.im, im := z.re }.re ∧ (I * z).im = { re := -z.im, im := z.re }.im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ I ≠ 0

Tactic:
mt (congr_arg im) zero_ne_one.symm

Premises used: Complex.im, mt, zero_ne_one, Ne.symm, congr_arg
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℝ
⊢ { re := a, im := b : ℂ }.re = ((↑a : ℂ) + (↑b : ℂ) * I).re ∧
    { re := a, im := b : ℂ }.im = ((↑a : ℂ) + (↑b : ℂ) * I).im

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ ((↑z.re : ℂ) + (↑z.im : ℂ) * I).re = z.re ∧ ((↑z.re : ℂ) + (↑z.im : ℂ) * I).im = z.im

Tactic:
simp [ofReal]

Premises used: Complex.ofReal
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (z * I).re = -z.im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (z * I).im = z.re

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (I * z).re = -z.im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
z : ℂ
⊢ (I * z).im = z.re

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
p : ℝ × ℝ
a : re ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p) = ((↑p.1 : ℂ) + (↑p.2 : ℂ) * I).re
a₁ : im ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p) = ((↑p.1 : ℂ) + (↑p.2 : ℂ) * I).im
⊢ (equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p = (↑p.1 : ℂ) + (↑p.2 : ℂ) * I

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
p : ℝ × ℝ
⊢ re ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p) = ((↑p.1 : ℂ) + (↑p.2 : ℂ) * I).re

Tactic:
simp [Complex.equivRealProd, ofReal]

Premises used: Complex.ofReal, Complex.equivRealProd
-- Module: Mathlib.Data.Complex.Basic
Goal:
p : ℝ × ℝ
⊢ im ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p) = ((↑p.1 : ℂ) + (↑p.2 : ℂ) * I).im

Tactic:
simp [Complex.equivRealProd, ofReal]

Premises used: Complex.ofReal, Complex.equivRealProd
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ ∀ (x y : ℂ), equivRealProd.toFun (x + y) = equivRealProd.toFun x + equivRealProd.toFun y

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
p : ℝ × ℝ
⊢ (equivRealProdAddHom.symm : (a : ℝ × ℝ) → ℂ) p = (↑p.1 : ℂ) + (↑p.2 : ℂ) * I

Tactic:
equivRealProd_symm_apply p

Premises used: Complex.equivRealProd_symm_apply
-- Module: Mathlib.Data.Complex.Basic
Goal:
⊢ Nontrivial ℂ

Tactic:
domain_nontrivial re rfl rfl

Premises used: domain_nontrivial, Complex.re, rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
R : Type u_1
inst : SMul R ℝ
r : R
z : ℂ
⊢ r • z.re - 0 * z.im = r • z.re

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
R : Type u_1
inst : SMul R ℝ
r : R
z : ℂ
⊢ r • z.im + 0 * z.re = r • z.im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℝ
z : ℂ
⊢ x • z = (↑x : ℂ) * z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 b c : ℂ
a : (a_1 + b + c).re = (a_1 + (b + c)).re
a₁ : (a_1 + b + c).im = (a_1 + (b + c)).im
⊢ a_1 + b + c = a_1 + (b + c)

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b c : ℂ
⊢ a.re + b.re + c.re = a.re + (b.re + c.re)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b c : ℂ
⊢ a.im + b.im + c.im = a.im + (b.im + c.im)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 : ℂ
a : (0 + a_1).re = a_1.re
a₁ : (0 + a_1).im = a_1.im
⊢ 0 + a_1 = a_1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (0 + a).re = a.re

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (0 + a).im = a.im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 : ℂ
a : (a_1 + 0).re = a_1.re
a₁ : (a_1 + 0).im = a_1.im
⊢ a_1 + 0 = a_1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (a + 0).re = a.re

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (a + 0).im = a.im

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℂ
a : (HSMul.hSMul (α := ℕ) 0 x).re = re 0
a₁ : (HSMul.hSMul (α := ℕ) 0 x).im = im 0
⊢ HSMul.hSMul (α := ℕ) 0 x = 0

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℂ
⊢ (HSMul.hSMul (α := ℕ) 0 x).re = re 0

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
x : ℂ
⊢ (HSMul.hSMul (α := ℕ) 0 x).im = im 0

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
x : ℂ
a : ((n + 1) • x).re = (n • x + x).re
a₁ : ((n + 1) • x).im = (n • x + x).im
⊢ (n + 1) • x = n • x + x

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
x : ℂ
a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x.re = (↑n : ℝ) * x.re + x.re
⊢ ((n + 1) • x).re = (n • x + x).re

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
x : ℂ
a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x.im = (↑n : ℝ) * x.im + x.im
⊢ ((n + 1) • x).im = (n • x + x).im

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
x : ℂ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x.re = (↑n : ℝ) * x.re + x.re

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
x : ℂ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x.im = (↑n : ℝ) * x.im + x.im

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 : ℂ
a : (HSMul.hSMul (α := ℤ) 0 a_1).re = re 0
a₁ : (HSMul.hSMul (α := ℤ) 0 a_1).im = im 0
⊢ HSMul.hSMul (α := ℤ) 0 a_1 = 0

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (HSMul.hSMul (α := ℤ) 0 a).re = re 0

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (HSMul.hSMul (α := ℤ) 0 a).im = im 0

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a_1 : ℂ
a : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).re = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a_1 + a_1).re
a₁ : (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).im = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a_1 + a_1).im
⊢ HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1 = HSMul.hSMul (α := ℤ) (↑n : ℤ) a_1 + a_1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a_1 : ℂ
a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a_1.re = (↑n : ℝ) * a_1.re + a_1.re
⊢ (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).re = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a_1 + a_1).re

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a_1 : ℂ
a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a_1.im = (↑n : ℝ) * a_1.im + a_1.im
⊢ (HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).im = (HSMul.hSMul (α := ℤ) (↑n : ℤ) a_1 + a_1).im

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a : ℂ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a.re = (↑n : ℝ) * a.re + a.re

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a : ℂ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a.im = (↑n : ℝ) * a.im + a.im

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a_1 : ℂ
a : (Int.negSucc n • a_1).re = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).re
a₁ : (Int.negSucc n • a_1).im = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).im
⊢ Int.negSucc n • a_1 = -HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a_1 : ℂ
a : HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * a_1.re = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a_1.re)
⊢ (Int.negSucc n • a_1).re = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).re

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a_1 : ℂ
a : HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * a_1.im = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a_1.im)
⊢ (Int.negSucc n • a_1).im = (-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a_1).im

Tactic:
simp [smul_re, smul_im]

Premises used: Complex.smul_re, Complex.smul_im
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a : ℂ
⊢ HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * a.re = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a.re)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
a : ℂ
⊢ HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * a.im = -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a.im)

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 : ℂ
a : (-a_1 + a_1).re = re 0
a₁ : (-a_1 + a_1).im = im 0
⊢ -a_1 + a_1 = 0

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (-a + a).re = re 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a : ℂ
⊢ (-a + a).im = im 0

Tactic:
simp
-- Module: Mathlib.Data.Complex.Basic
Goal:
a_1 b : ℂ
a : (a_1 + b).re = (b + a_1).re
a₁ : (a_1 + b).im = (b + a_1).im
⊢ a_1 + b = b + a_1

Tactic:
ext
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
⊢ a.re + b.re = b.re + a.re

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
a b : ℂ
⊢ a.im + b.im = b.im + a.im

Tactic:
ring
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ (↑(OfNat.ofNat n) : ℂ) = OfNat.ofNat n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
⊢ (↑(↑n : ℝ) : ℂ) = (↑n : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℤ
⊢ (↑(↑n : ℝ) : ℂ) = (↑n : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ≥0
⊢ (↑(↑q : ℝ) : ℂ) = (↑q : ℂ)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
m : ℕ
s : Bool
e : ℕ
⊢ (↑(OfScientific.ofScientific m s e) : ℂ) = OfScientific.ofScientific m s e

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ im (OfNat.ofNat n) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
⊢ re (↑n : ℂ) = (↑n : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℕ
⊢ im (↑n : ℂ) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℤ
⊢ re (↑n : ℂ) = (↑n : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
n : ℤ
⊢ im (↑n : ℂ) = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Complex.Basic
Goal:
q : ℚ≥0
⊢ re (↑q : ℂ) = (↑q : ℝ)

Tactic:
rfl

Premises used: rfl