awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Analysis.Filter (goal)
Goal:
α : Type u_1
f : Filter α
F : Realizer.{u_1, u_5} f
⊢ (∃ (x : F.σ), ¬(F.F.f x).Nonempty) ↔
    ∀ (b : σ.{u_1, 0} (α := α) Realizer.bot), ∃ (a : F.σ), F.F.f a ≤ CFilter.f (Realizer.F Realizer.bot) b
have simp : (∃ (x : F.σ), F.F.f x = ∅) ↔
  ∀ (b : σ.{u_1, 0} (α := α) Realizer.bot), ∃ (a : F.σ), F.F.f a ≤ CFilter.f (Realizer.F Realizer.bot) b
Tactic: simp only [Set.not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
σ : Type u_3
τ : Type u_4
E : σ ≃ τ
F : Ctop α σ
a : τ
⊢ (ofEquiv E F).f a = F.f ((E.symm : (a : τ) → σ) a)
have mk : ∀ (f : σ → Set α) (top : α → σ) (top_mem : ∀ (x : α), x ∈ f (top x)) (inter : (a b : σ) → (x : α) → x ∈ f a ∩ f b → σ)
  (inter_mem : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), x ∈ f (inter a b x h))
  (inter_sub : ∀ (a b : σ) (x : α) (h : x ∈ f a ∩ f b), f (inter a b x h) ⊆ f a ∩ f b),
  (ofEquiv E
          { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub :
            Ctop α σ }).f
      a =
    { f := f, top := top, top_mem := top_mem, inter := inter, inter_mem := inter_mem, inter_sub := inter_sub :
          Ctop α σ }.f
      ((E.symm : (a : τ) → σ) a)
Tactic: cases F
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (hypothesis)
Goal:
α : Type u_1
T : TopologicalSpace α
F : Realizer.{u_5, u_1} α
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
have this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
Tactic: have := toTopsp_isTopologicalBasis F.F
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
T : TopologicalSpace α
F : Realizer.{u_5, u_1} α
this : TopologicalSpace.IsTopologicalBasis (range F.F.f)
⊢ TopologicalSpace.IsTopologicalBasis (range F.F.f)
have rwa : ∀ (this : TopologicalSpace.IsTopologicalBasis (range F.F.f)), TopologicalSpace.IsTopologicalBasis (range F.F.f)
Tactic: rwa [F.eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (hypothesis)
Goal:
α : Type u_1
T : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s
have this : s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s
Tactic: have := @mem_nhds_toTopsp _ _ F.F s a
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
T : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s
have rwa : ∀ (this : s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s), s ∈ 𝓝 a ↔ ∃ (b : F.σ), a ∈ F.F.f b ∧ F.F.f b ⊆ s
Tactic: rwa [F.eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
⊢ (a ∉ s → ∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔
    (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s
have haveI : ∀ (this : (a : Prop) → Decidable a),
  (a ∉ s → ∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔
    (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s
Tactic: haveI := Classical.propDecidable
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
s : Set α
a : α
this : (a : Prop) → Decidable a
⊢ (a ∉ s → ∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) ↔
    (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s
have rw : (¬∃ (b : F.σ), a ∈ F.F.f b ∧ ∀ z ∈ F.F.f b, z ∉ s) → a ∈ s ↔
  (∀ (b : F.σ), a ∈ F.F.f b → ∃ (z : α), z ∈ F.F.f b ∩ s) → a ∈ s
Tactic: rw [not_imp_comm]
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
⊢ F.toTopsp = T
have refine : ∀ (x : α), 𝓝 x = 𝓝 x
Tactic: refine TopologicalSpace.ext_nhds fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
x : α
⊢ 𝓝 x = 𝓝 x
have h : ∀ (s : Set α), s ∈ 𝓝 x ↔ s ∈ 𝓝 x
Tactic: ext s
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x
have h : (∃ (b : σ), x ∈ F.f b ∧ F.f b ⊆ s) ↔ s ∈ 𝓝 x
Tactic: rw [mem_nhds_toTopsp, H]
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ (b : σ), a ∈ F.f b ∧ F.f b ⊆ s
x : α
s : Set α
h : (∃ (b : σ), x ∈ F.f b ∧ F.f b ⊆ s) ↔ s ∈ 𝓝 x
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x
have h₁ : (∃ (b : σ), x ∈ F.f b ∧ F.f b ⊆ s) ↔ ∃ (b : σ), x ∈ F.f b ∧ F.f b ⊆ s
Tactic: rw [mem_nhds_toTopsp, H]
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
τ : Type u_4
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
E : Equiv.{u_5 + 1, u_4 + 1} F.σ τ
s : τ
⊢ (F.ofEquiv E).F.f s = F.F.f ((E.symm : (a : τ) → F.σ) s)
have delta : { σ := τ, F := Ctop.ofEquiv E F.F, eq := sorry : Realizer.{u_4, u_1} α }.F.f s = F.F.f ((E.symm : (a : τ) → F.σ) s)
Tactic: delta ofEquiv
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst : TopologicalSpace α
f : Filter α
F : Filter.Realizer.{u_1, u_5} f
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ { a : α // Membership.mem (γ := Set α) ∅ a ∧ 𝓝 a ⊓ f ≠ ⊥ }
have suffices : f = ⊥
Tactic: suffices f = ⊥ from absurd this h
-- Lean 4 proof step from Mathlib.Data.Analysis.Topology (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst : TopologicalSpace α
f : Filter α
F : Filter.Realizer.{u_1, u_5} f
x : F.σ
h : f ≠ ⊥
hF : F.F.f x ⊆ ∅
⊢ f = ⊥
have rw : F.F.toFilter ≤ ⊥
Tactic: rw [← F.eq, eq_bot_iff]
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
w : ℕ
z : ℤ
⊢ Eq (α := BitVec w) { toFin := (↑z : Fin (2 ^ w)) } (↑z : BitVec w)
have cases : Eq (α := BitVec 0) { toFin := (↑z : Fin (2 ^ 0)) } (↑z : BitVec 0)
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
w : ℕ
z : ℤ
cases : Eq (α := BitVec 0) { toFin := (↑z : Fin (2 ^ 0)) } (↑z : BitVec 0)
⊢ Eq (α := BitVec w) { toFin := (↑z : Fin (2 ^ w)) } (↑z : BitVec w)
have succ : ∀ (n : ℕ), Eq (α := BitVec (n + 1)) { toFin := (↑z : Fin (2 ^ (n + 1))) } (↑z : BitVec (n + 1))
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
z : ℤ
w : ℕ
⊢ Eq (α := BitVec (w + 1)) { toFin := (↑z : Fin (2 ^ (w + 1))) } (↑z : BitVec (w + 1))
have a : BitVec.toInt (n := w + 1) { toFin := (↑z : Fin (2 ^ (w + 1))) : BitVec (w + 1) } =
  BitVec.toInt (n := w + 1) (↑z : BitVec (w + 1))
Tactic: apply BitVec.eq_of_toInt_eq
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
z : ℤ
w : ℕ
⊢ BitVec.toInt (n := w + 1) { toFin := (↑z : Fin (2 ^ (w + 1))) : BitVec (w + 1) } =
    BitVec.toInt (n := w + 1) (↑z : BitVec (w + 1))
have a : (max (z % HPow.hPow (α := ℤ) 2 (w + 1)) 0).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
Tactic: rw [toInt_ofFin, Fin.val_intCast, Int.natCast_pow, Nat.cast_ofNat, Int.ofNat_toNat,
      toInt_intCast]
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
z : ℤ
w : ℕ
⊢ (max (z % HPow.hPow (α := ℤ) 2 (w + 1)) 0).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
have a : (z % HPow.hPow (α := ℤ) 2 (w + 1)).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
Tactic: rw [Int.max_eq_left]
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
z : ℤ
w : ℕ
a : (z % HPow.hPow (α := ℤ) 2 (w + 1)).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
⊢ (max (z % HPow.hPow (α := ℤ) 2 (w + 1)) 0).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
have a₁ : 0 ≤ z % HPow.hPow (α := ℤ) 2 (w + 1)
Tactic: rw [Int.max_eq_left]
-- Lean 4 proof step from Mathlib.Data.BitVec (hypothesis)
Goal:
z : ℤ
w : ℕ
⊢ (z % HPow.hPow (α := ℤ) 2 (w + 1)).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
have h : HPow.hPow (α := ℤ) 2 (w + 1) = (↑(HPow.hPow (α := ℕ) 2 (w + 1)) : ℤ)
Tactic: have h : (2 ^ (w + 1) : Int) = (2 ^ (w + 1) : Nat) := by simp
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
z : ℤ
w : ℕ
h : HPow.hPow (α := ℤ) 2 (w + 1) = (↑(HPow.hPow (α := ℕ) 2 (w + 1)) : ℤ)
⊢ (z % HPow.hPow (α := ℤ) 2 (w + 1)).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
have a : (z % (↑(HPow.hPow (α := ℕ) 2 (w + 1)) : ℤ)).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
Tactic: rw [h, Int.emod_bmod]
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
z : ℤ
w : ℕ
h : HPow.hPow (α := ℤ) 2 (w + 1) = (↑(HPow.hPow (α := ℕ) 2 (w + 1)) : ℤ)
a :
  (z % (↑(HPow.hPow (α := ℕ) 2 (w + 1)) : ℤ)).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) =
    z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
⊢ (z % HPow.hPow (α := ℤ) 2 (w + 1)).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
have a₁ : z.bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
Tactic: rw [h, Int.emod_bmod]
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
w : ℕ
z : ℤ
⊢ Eq (α := Fin (HPow.hPow (α := ℕ) 2 w)) (toFin (↑z : BitVec w)) (↑z : Fin (2 ^ w))
have rw : Eq (α := Fin (HPow.hPow (α := ℕ) 2 w)) (toFin { toFin := (↑z : Fin (2 ^ w)) }) (↑z : Fin (2 ^ w))
Tactic: rw [← ofFin_intCast]
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
w : ℕ
x : BitVec w
n : ℕ
⊢ (x ^ n).toFin = x.toFin ^ n
have zero : (HPow.hPow (β := ℕ) x 0).toFin = HPow.hPow (β := ℕ) x.toFin 0
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [ih, BitVec.pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.BitVec (goal)
Goal:
w : ℕ
x : BitVec w
n : ℕ
zero : (HPow.hPow (β := ℕ) x 0).toFin = HPow.hPow (β := ℕ) x.toFin 0
⊢ (x ^ n).toFin = x.toFin ^ n
have succ : ∀ (n : ℕ) (ih : (x ^ n).toFin = x.toFin ^ n), (x ^ (n + 1)).toFin = x.toFin ^ (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [ih, BitVec.pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
b : Bool
⊢ (b.toNat == 1) = b
have false : (false.toNat == 1) = false
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
b : Bool
false : (Bool.false.toNat == 1) = Bool.false
⊢ (b.toNat == 1) = b
have true : (true.toNat == 1) = true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
n m : Nat
h : n ≤ m
⊢ ofNat n ≤ ofNat m
have simp : (!decide (n = 0)) ≤ !decide (m = 0)
Tactic: simp only [ofNat, ne_eq, _root_.decide_not]
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
n m : Nat
h : n ≤ m
hn : ¬n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
have isFalse : ∀ (x : Decidable (m = 0)), (!decide (n = 0)) ≤ !decide (m = 0)
Tactic: cases Nat.decEq m 0 with grind [Bool.le_true]
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
n m : Nat
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
have cases : ∀ (x : Decidable (n = 0)), (!decide (n = 0)) ≤ !decide (m = 0)
Tactic: cases Nat.decEq n 0 with
  | isTrue hn => grind [Bool.false_le]
  | isFalse hn => cases Nat.decEq m 0 with grind [Bool.le_true]
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ b₀.toNat ≤ b₁.toNat
have false : ∀ (h : false ≤ b₁), false.toNat ≤ b₁.toNat
Tactic: cases b₀
Cleared hypotheses: b₀, h
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
b₀ b₁ : Bool
h : b₀ ≤ b₁
false : ∀ (h : Bool.false ≤ b₁), Bool.false.toNat ≤ b₁.toNat
⊢ b₀.toNat ≤ b₁.toNat
have true : ∀ (h : true ≤ b₁), true.toNat ≤ b₁.toNat
Tactic: cases b₀
Cleared hypotheses: b₀, h
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
b₁ : Bool
h : false ≤ b₁
⊢ false.toNat ≤ b₁.toNat
have false : ∀ (h : false ≤ false), false.toNat ≤ false.toNat
Tactic: cases b₁
Cleared hypotheses: b₁, h
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
b₁ : Bool
h : Bool.false ≤ b₁
false : ∀ (h : Bool.false ≤ Bool.false), Bool.false.toNat ≤ Bool.false.toNat
⊢ Bool.false.toNat ≤ b₁.toNat
have false₁ : ∀ (h : Bool.false ≤ true), Bool.false.toNat ≤ true.toNat
Tactic: cases b₁
Cleared hypotheses: b₁, h
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
b₁ : Bool
h : true ≤ b₁
⊢ true.toNat ≤ b₁.toNat
have true : ∀ (h : true ≤ false), true.toNat ≤ false.toNat
Tactic: cases b₁
Cleared hypotheses: b₁, h
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
b₁ : Bool
h : Bool.true ≤ b₁
true : ∀ (h : Bool.true ≤ false), Bool.true.toNat ≤ false.toNat
⊢ Bool.true.toNat ≤ b₁.toNat
have true₁ : ∀ (h : Bool.true ≤ Bool.true), Bool.true.toNat ≤ Bool.true.toNat
Tactic: cases b₁
Cleared hypotheses: b₁, h
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x
have false : ∀ (h₁ : f true = false), f (f (f x)) = f x
Tactic: cases h₁ : f true
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
f : Bool → Bool
x : Bool
false : ∀ (h₁ : f true = Bool.false), f (f (f x)) = f x
⊢ f (f (f x)) = f x
have true : ∀ (h₁ : f true = true), f (f (f x)) = f x
Tactic: cases h₁ : f true
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
f : Bool → Bool
x : Bool
h₁ : f true = false
⊢ f (f (f x)) = f x
have false : ∀ (h₂ : f false = false), f (f (f x)) = f x
Tactic: cases h₂ : f false
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
f : Bool → Bool
x : Bool
h₁ : f true = Bool.false
false : ∀ (h₂ : f Bool.false = Bool.false), f (f (f x)) = f x
⊢ f (f (f x)) = f x
have false₁ : ∀ (h₂ : f Bool.false = true), f (f (f x)) = f x
Tactic: cases h₂ : f false
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
f : Bool → Bool
x : Bool
h₁ : f true = true
⊢ f (f (f x)) = f x
have true : ∀ (h₂ : f false = false), f (f (f x)) = f x
Tactic: cases h₂ : f false
-- Lean 4 proof step from Mathlib.Data.Bool.Basic (goal)
Goal:
f : Bool → Bool
x : Bool
h₁ : f Bool.true = Bool.true
true : ∀ (h₂ : f false = false), f (f (f x)) = f x
⊢ f (f (f x)) = f x
have true₁ : ∀ (h₂ : f false = Bool.true), f (f (f x)) = f x
Tactic: cases h₂ : f false
-- Lean 4 proof step from Mathlib.Data.Bool.Count (hypothesis)
Goal:
l : List Bool
b : Bool
⊢ count (!b) l + count b l = l.length
have this : l.length = countP (fun (x : Bool) ↦ x == !b) l + countP (fun (a : Bool) ↦ decide ¬(a == !b) = true) l
Tactic: have := length_eq_countP_add_countP (l := l) (· == !b)
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ count (!b) l = count b l
have nil : ∀ (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []) (h2 : Even (length (α := Bool) [])), count (!b) [] = count b []
Tactic: rcases l with - | ⟨x, l⟩
Cleared hypotheses: l, hl, h2
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
nil : ∀ (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []) (h2 : Even (length (α := Bool) [])), count (!b) [] = count b []
⊢ count (!b) l = count b l
have cons : ∀ (x : Bool) (l : List Bool) (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) (x :: l)) (h2 : Even (x :: l).length),
  count (!b) (x :: l) = count b (x :: l)
Tactic: rcases l with - | ⟨x, l⟩
Cleared hypotheses: l, hl, h2
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
⊢ count (!b) l ≤ count b l + 1
have nil : ∀ (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []), count (!b) [] ≤ count b [] + 1
Tactic: cases l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
nil : ∀ (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []), count (!b) [] ≤ count b [] + 1
⊢ count (!b) l ≤ count b l + 1
have cons : ∀ (head : Bool) (tail : List Bool) (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) (head :: tail)),
  count (!b) (head :: tail) ≤ count b (head :: tail) + 1
Tactic: cases l
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ 2 * count b l = l.length
have rw : 2 * count b l = count (!b) l + count b l
Tactic: rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
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
⊢ 2 * count b l = l.length
have rw₁ : 2 * count b l = count b l + count b l
Tactic: rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
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
⊢ 2 * count b l = l.length
have rw₂ : count b l + count b l = count b l + count b l
Tactic: rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
⊢ 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
have 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
Tactic: by_cases h2 : Even (length l)
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
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
⊢ 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
have 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
Tactic: by_cases h2 : Even (length l)
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
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
have pos : 2 * count b l = l.length
Tactic: rw [if_pos h2, hl.two_mul_count_bool_of_even h2]
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
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
⊢ 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
have pos₁ : l.length = l.length
Tactic: rw [if_pos h2, hl.two_mul_count_bool_of_even h2]
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
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
have 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
Tactic: rcases l with - | ⟨x, l⟩
Cleared hypotheses: l, hl, h2
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
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
⊢ 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
have 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
Tactic: rcases l with - | ⟨x, l⟩
Cleared hypotheses: l, hl, h2
-- Lean 4 proof step from Mathlib.Data.Bool.Count (goal)
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
b : Bool
⊢ l.length / 2 ≤ count b l
have rw : l.length - HSub.hSub (α := ℕ) 2 1 ≤ 2 * count b l
Tactic: rw [Nat.div_le_iff_le_mul_add_pred two_pos, ← tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Data.Bundle (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
x x' : B
h : x = x'
b : E x
⊢ mk' (E := E) F x' (cast ⋯ b) = mk (E := E) x b
have subst : mk' (E := E) F x (cast sorry b) = mk (E := E) x b
Tactic: subst h
Cleared hypotheses: x', h
-- Lean 4 proof step from Mathlib.Data.Bundle (goal)
Goal:
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ Eq (α := Set (TotalSpace F E)) (range (mk (E := E) b)) (proj (E := E) ⁻¹' {b})
have h₁ : Subset (α := Set (TotalSpace F E)) (range (mk (E := E) b)) (proj (E := E) ⁻¹' {b})
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Bundle (goal)
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})
⊢ Eq (α := Set (TotalSpace F E)) (range (mk (E := E) b)) (proj (E := E) ⁻¹' {b})
have h₂ : Subset (α := Set (TotalSpace F E)) (proj (E := E) ⁻¹' {b}) (range (mk (E := E) b))
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
p : ℝ × ℝ
⊢ (equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p = (↑p.1 : ℂ) + (↑p.2 : ℂ) * I
have a : re ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p) = ((↑p.1 : ℂ) + (↑p.2 : ℂ) * I).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
p : ℝ × ℝ
a : re ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p) = ((↑p.1 : ℂ) + (↑p.2 : ℂ) * I).re
⊢ (equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p = (↑p.1 : ℂ) + (↑p.2 : ℂ) * I
have a₁ : im ((equivRealProd.symm : (a : ℝ × ℝ) → ℂ) p) = ((↑p.1 : ℂ) + (↑p.2 : ℂ) * I).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a b c : ℂ
⊢ a + b + c = a + (b + c)
have a : (a + b + c).re = (a + (b + c)).re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 b c : ℂ
a : (a_1 + b + c).re = (a_1 + (b + c)).re
⊢ a_1 + b + c = a_1 + (b + c)
have a₁ : (a_1 + b + c).im = (a_1 + (b + c)).im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : ℂ
⊢ 0 + a = a
have a : (0 + a).re = a.re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 : ℂ
a : (0 + a_1).re = a_1.re
⊢ 0 + a_1 = a_1
have a₁ : (0 + a_1).im = a_1.im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a : ℂ
⊢ a + 0 = a
have a : (a + 0).re = a.re
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
a_1 : ℂ
a : (a_1 + 0).re = a_1.re
⊢ a_1 + 0 = a_1
have a₁ : (a_1 + 0).im = a_1.im
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x : ℂ
⊢ HSMul.hSMul (α := ℕ) 0 x = 0
have a : (HSMul.hSMul (α := ℕ) 0 x).re = re 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
x : ℂ
a : (HSMul.hSMul (α := ℕ) 0 x).re = re 0
⊢ HSMul.hSMul (α := ℕ) 0 x = 0
have a₁ : (HSMul.hSMul (α := ℕ) 0 x).im = im 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Complex.Basic (goal)
Goal:
n : ℕ
x : ℂ
⊢ (n + 1) • x = n • x + x
have a : ((n + 1) • x).re = (n • x + x).re
Tactic: ext