awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
F : Realizer.{u_5, u_1} α
f : β → Set α
⊢ LocallyFinite f ↔ Nonempty (LocallyFinite.Realizer F f)

Tactic:
⟨fun h ↦
    let ⟨g, h₁⟩ := Classical.axiom_of_choice h
    let ⟨g₂, h₂⟩ :=
      Classical.axiom_of_choice fun x ↦
        show ∃ b : F.σ, x ∈ F.F b ∧ F.F b ⊆ g x from
          let ⟨h, _h'⟩ := h₁ x
          F.mem_nhds.1 h
    ⟨⟨fun x ↦ ⟨g₂ x, (h₂ x).1⟩, fun x ↦
        Finite.fintype <|
          let ⟨_h, h'⟩ := h₁ x
          h'.subset fun _i hi ↦ hi.mono (inter_subset_inter_right _ (h₂ x).2)⟩⟩,
    fun ⟨R⟩ ↦ R.to_locallyFinite⟩

Premises used: Set.inter_subset_inter_right, setOf, Set.Finite, Membership.mem, Exists, Set.Finite.fintype, HasSubset.Subset, Set.Finite.subset, Ctop.f, _private.0.locallyFinite_iff_exists_realizer.match_3, Ctop.Realizer.mem_nhds, Nonempty.intro, LocallyFinite.Realizer.to_locallyFinite, Classical.axiom_of_choice, LocallyFinite, Set.Nonempty.mono, Subtype.mk, Inter.inter, LocallyFinite.Realizer.mk, And, Set.Nonempty, And.right, And.left, Iff.intro, Iff.mp, Nonempty, LocallyFinite.Realizer, _private.0.locallyFinite_iff_exists_realizer.match_4, _private.0.locallyFinite_iff_exists_realizer.match_1, Subtype.val, _private.0.locallyFinite_iff_exists_realizer.match_2, Ctop.Realizer.F
-- Module: Mathlib.Data.Analysis.Topology
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst : TopologicalSpace α
inst_1 : Finite β
F : Realizer.{u_5, u_1} α
f : β → Set α
⊢ Nonempty (LocallyFinite.Realizer F f)

Tactic:
(locallyFinite_iff_exists_realizer _).1 <| locallyFinite_of_finite _

Premises used: locallyFinite_of_finite, locallyFinite_iff_exists_realizer, Iff.mp
-- Module: Mathlib.Data.Analysis.Topology
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 ⊆ ∅
suffices : f = ⊥
⊢ { a : α // Membership.mem (γ := Set α) ∅ a ∧ 𝓝 a ⊓ f ≠ ⊥ }

Tactic:
suffices f = ⊥ from absurd this h
-- Module: Mathlib.Data.Analysis.Topology
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 ⊆ ∅
rw : F.F.toFilter ≤ ⊥
⊢ f = ⊥

Tactic:
rw [← F.eq, eq_bot_iff]

Premises used: Filter.Realizer.eq, eq_bot_iff
-- Module: Mathlib.Data.Analysis.Topology
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.F.toFilter ≤ ⊥

Tactic:
fun s _ ↦ ⟨x, hF.trans s.empty_subset⟩

Premises used: Set.Mem, setOf, HasSubset.Subset.trans, Set.empty_subset, Exists.intro
-- Module: Mathlib.Data.Analysis.Topology
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.F.toFilter ≤ ⊥

Tactic:
exact fun s _ ↦ ⟨x, hF.trans s.empty_subset⟩
-- Module: Mathlib.Data.BitVec
Goal:
w : ℕ
z : ℤ
cases : Eq (α := BitVec 0) { toFin := (↑z : Fin (2 ^ 0)) } (↑z : BitVec 0)
succ : ∀ (n : ℕ), Eq (α := BitVec (n + 1)) { toFin := (↑z : Fin (2 ^ (n + 1))) } (↑z : BitVec (n + 1))
⊢ Eq (α := BitVec w) { toFin := (↑z : Fin (2 ^ w)) } (↑z : BitVec w)

Tactic:
cases w
-- Module: Mathlib.Data.BitVec
Goal:
z : ℤ
⊢ Eq (α := BitVec 0) { toFin := (↑z : Fin (2 ^ 0)) } (↑z : BitVec 0)

Tactic:
simp only [eq_nil]

Premises used: BitVec.eq_nil
-- Module: Mathlib.Data.BitVec
Goal:
z : ℤ
⊢ Eq (α := BitVec 0) { toFin := (↑z : Fin (2 ^ 0)) } (↑z : BitVec 0)

Tactic:
case zero =>
    simp only [eq_nil]

Premises used: BitVec.eq_nil
-- Module: Mathlib.Data.BitVec
Goal:
z : ℤ
w : ℕ
a :
  BitVec.toInt (n := w + 1) { toFin := (↑z : Fin (2 ^ (w + 1))) : BitVec (w + 1) } =
    BitVec.toInt (n := w + 1) (↑z : BitVec (w + 1))
⊢ Eq (α := BitVec (w + 1)) { toFin := (↑z : Fin (2 ^ (w + 1))) } (↑z : BitVec (w + 1))

Tactic:
apply BitVec.eq_of_toInt_eq

Premises used: BitVec.eq_of_toInt_eq
-- Module: Mathlib.Data.BitVec
Goal:
z : ℤ
w : ℕ
a :
  (max (z % HPow.hPow (α := ℤ) 2 (w + 1)) 0).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
⊢ BitVec.toInt (n := w + 1) { toFin := (↑z : Fin (2 ^ (w + 1))) : BitVec (w + 1) } =
    BitVec.toInt (n := w + 1) (↑z : BitVec (w + 1))

Tactic:
rw [toInt_ofFin, Fin.val_intCast, Int.natCast_pow, Nat.cast_ofNat, Int.ofNat_toNat,
      toInt_intCast]

Premises used: Nat.cast_ofNat, Int.natCast_pow, BitVec.toInt_intCast, Int.ofNat_toNat, Fin.val_intCast, BitVec.toInt_ofFin
-- Module: Mathlib.Data.BitVec
Goal:
z : ℤ
w : ℕ
a : (z % HPow.hPow (α := ℤ) 2 (w + 1)).bmod (HPow.hPow (α := ℕ) 2 (w + 1)) = z.bmod (HPow.hPow (α := ℕ) 2 (w + 1))
a₁ : 0 ≤ z % 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))

Tactic:
rw [Int.max_eq_left]

Premises used: Int.max_eq_left
-- Module: Mathlib.Data.BitVec
Goal:
z : ℤ
w : ℕ
⊢ HPow.hPow (α := ℤ) 2 (w + 1) = (↑(HPow.hPow (α := ℕ) 2 (w + 1)) : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.BitVec
Goal:
z : ℤ
w : ℕ
⊢ HPow.hPow (α := ℤ) 2 (w + 1) = (↑(HPow.hPow (α := ℕ) 2 (w + 1)) : ℤ)

Tactic:
have h : (2 ^ (w + 1) : Int) = (2 ^ (w + 1) : Nat) := by simp
-- Module: Mathlib.Data.BitVec
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))
a₁ a₂ : z.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))

Tactic:
rw [h, Int.emod_bmod]

Premises used: Int.emod_bmod
-- Module: Mathlib.Data.BitVec
Goal:
z : ℤ
w : ℕ
⊢ 0 ≤ z % HPow.hPow (α := ℤ) 2 (w + 1)

Tactic:
omega
-- Module: Mathlib.Data.BitVec
Goal:
w : ℕ
z : ℤ
rw rw₁ : Eq (α := Fin (HPow.hPow (α := ℕ) 2 w)) (toFin { toFin := (↑z : Fin (2 ^ w)) }) (↑z : Fin (2 ^ w))
⊢ Eq (α := Fin (HPow.hPow (α := ℕ) 2 w)) (toFin (↑z : BitVec w)) (↑z : Fin (2 ^ w))

Tactic:
rw [← ofFin_intCast]

Premises used: BitVec.ofFin_intCast
-- Module: Mathlib.Data.BitVec
Goal:
w n : ℕ
x : BitVec w
⊢ toFin (↑n : BitVec w) * x.toFin = n • x.toFin

Tactic:
simp only [natCast_eq_ofNat, toFin_ofNat, Fin.ofNat_eq_cast, nsmul_eq_mul]

Premises used: Fin.ofNat_eq_cast, nsmul_eq_mul, BitVec.toFin_ofNat, BitVec.natCast_eq_ofNat
-- Module: Mathlib.Data.BitVec
Goal:
w n : ℕ
x : BitVec w
⊢ toFin (↑n : BitVec w) * x.toFin = n • x.toFin

Tactic:
open scoped Fin.CommRing in
    simp only [natCast_eq_ofNat, toFin_ofNat, Fin.ofNat_eq_cast, nsmul_eq_mul]

Premises used: Fin.ofNat_eq_cast, nsmul_eq_mul, BitVec.toFin_ofNat, BitVec.natCast_eq_ofNat
-- Module: Mathlib.Data.BitVec
Goal:
w : ℕ
z : ℤ
x : BitVec w
⊢ toFin (↑z : BitVec w) * x.toFin = z • x.toFin

Tactic:
simp only [zsmul_eq_mul, toFin_intCast]

Premises used: zsmul_eq_mul, BitVec.toFin_intCast
-- Module: Mathlib.Data.BitVec
Goal:
w : ℕ
z : ℤ
x : BitVec w
⊢ toFin (↑z : BitVec w) * x.toFin = z • x.toFin

Tactic:
open scoped Fin.CommRing in
    simp only [zsmul_eq_mul, toFin_intCast]

Premises used: zsmul_eq_mul, BitVec.toFin_intCast
-- Module: Mathlib.Data.BitVec
Goal:
w : ℕ
x : BitVec w
⊢ (HPow.hPow (β := ℕ) x 0).toFin = HPow.hPow (β := ℕ) x.toFin 0

Tactic:
simp
-- Module: Mathlib.Data.BitVec
Goal:
w : ℕ
x : BitVec w
n : ℕ
ih : (x ^ n).toFin = x.toFin ^ n
⊢ (x ^ (n + 1)).toFin = x.toFin ^ (n + 1)

Tactic:
simp [ih, BitVec.pow_succ]

Premises used: BitVec.pow_succ
-- Module: Mathlib.Data.BitVec
Goal:
w : ℕ
x : BitVec w
n : ℕ
zero : (HPow.hPow (β := ℕ) x 0).toFin = HPow.hPow (β := ℕ) x.toFin 0
succ : ∀ (n : ℕ) (ih : (x ^ n).toFin = x.toFin ^ n), (x ^ (n + 1)).toFin = x.toFin ^ (n + 1)
⊢ (x ^ n).toFin = x.toFin ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [ih, BitVec.pow_succ]

Premises used: BitVec.pow_succ
-- Module: Mathlib.Data.BitVec
Goal:
w : ℕ
⊢ Eq (α := HPow (Fin (HPow.hPow (α := ℕ) 2 w)) ℕ (Fin (HPow.hPow (α := ℕ) 2 w))) instHPow
    Lean.Grind.Fin.instHPowFinNatOfNeZero

Tactic:
rfl

Premises used: Lean.Grind.Fin.npow, rfl
-- Module: Mathlib.Data.Bool.AllAny
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : List α
⊢ (l.all fun (a : α) ↦ decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a

Tactic:
simp
-- Module: Mathlib.Data.Bool.AllAny
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
l : List α
⊢ (l.any fun (a : α) ↦ decide (p a)) = true ↔ ∃ (a : α), a ∈ l ∧ p a

Tactic:
simp
-- Module: Mathlib.Data.Bool.AllAny
Goal:
α : Type u_1
l : List α
a : α
p : α → Bool
h₁ : a ∈ l
h₂ : p a = true
⊢ l.any p = true

Tactic:
any_eq_true.2 ⟨_, h₁, h₂⟩

Premises used: Iff.mpr, And.intro, Exists.intro, List.any_eq_true
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ¬true = false

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ¬false = true

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ (¬b = true) = (b = false)

Tactic:
simp
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ (¬b = false) = (b = true)

Tactic:
simp
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ ¬b = true → b = false

Tactic:
Eq.mp (eq_false_eq_not_eq_true b)

Premises used: Eq.mp, Bool.eq_false_eq_not_eq_true
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ ¬b = false → b = true

Tactic:
Eq.mp (eq_true_eq_not_eq_false b)

Premises used: Bool.eq_true_eq_not_eq_false, Eq.mp
-- Module: Mathlib.Data.Bool.Basic
Goal:
a b : Bool
⊢ ((a && b) = true) = (a = true ∧ b = true)

Tactic:
simp
-- Module: Mathlib.Data.Bool.Basic
Goal:
a b : Bool
⊢ ((a || b) = true) = (a = true ∨ b = true)

Tactic:
simp
-- Module: Mathlib.Data.Bool.Basic
Goal:
a : Bool
⊢ ((!a) = true) = (a = false)

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
a b : Bool
⊢ ((a && b) = false) = (a = false ∨ b = false)

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
a b : Bool
⊢ ((a || b) = false) = (a = false ∧ b = false)

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
a : Bool
⊢ ((!a) = false) = (a = true)

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ (false = true) = False

Tactic:
simp
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ (true = true) = True

Tactic:
simp
-- Module: Mathlib.Data.Bool.Basic
Goal:
p : Prop
d : Decidable p
⊢ decide p = true ↔ p

Tactic:
simp
-- Module: Mathlib.Data.Bool.Basic
Goal:
p : Prop
inst : Decidable p
⊢ p → decide p = true

Tactic:
(decide_iff p).2

Premises used: Bool.decide_iff, Iff.mpr
-- Module: Mathlib.Data.Bool.Basic
Goal:
p : Prop
inst : Decidable p
⊢ decide p = true → p

Tactic:
(decide_iff p).1

Premises used: Bool.decide_iff, Iff.mp
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ ¬b = true ↔ b = false

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ ¬b = true → b = false

Tactic:
bool_iff_false.1

Premises used: Bool.bool_iff_false, Iff.mp
-- Module: Mathlib.Data.Bool.Basic
Goal:
p : Prop
x : Decidable p
⊢ decide p = false ↔ ¬p

Tactic:
bool_iff_false.symm.trans (not_congr (decide_iff _))

Premises used: Bool.decide_iff, Bool.bool_iff_false, Iff.trans, Iff.symm, not_congr
-- Module: Mathlib.Data.Bool.Basic
Goal:
p : Prop
inst : Decidable p
⊢ ¬p → decide p = false

Tactic:
(decide_false_iff p).2

Premises used: Iff.mpr, Bool.decide_false_iff
-- Module: Mathlib.Data.Bool.Basic
Goal:
p : Prop
inst : Decidable p
⊢ decide p = false → ¬p

Tactic:
(decide_false_iff p).1

Premises used: Bool.decide_false_iff, Iff.mp
-- Module: Mathlib.Data.Bool.Basic
Goal:
p q : Prop
inst : Decidable p
inst_1 : Decidable q
h : p ↔ q
⊢ decide p = decide q

Tactic:
decide_eq_decide.mpr h

Premises used: Iff.mpr, decide_eq_decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
a b : Bool
⊢ (a ^^ b) = true ↔ Xor (a = true) (b = true)

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ b = false ∨ b = true

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ not ≠ id

Tactic:
fun h ↦ false_ne_true <| congrFun h true

Premises used: Bool.true, congrFun, Bool.false_ne_true, Not
-- Module: Mathlib.Data.Bool.Basic
Goal:
a b : Bool
H : a = true
⊢ (a || b) = true

Tactic:
simp [H]
-- Module: Mathlib.Data.Bool.Basic
Goal:
a b : Bool
H : b = true
⊢ (a || b) = true

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {a b : Bool}, (a && b) = true → a = true

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {a b : Bool}, a = true → b = true → (a && b) = true

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {a b : Bool}, (a && b) = true → b = true

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {a b : Bool}, a = !b ↔ a ≠ b

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {a b : Bool}, (!a) = b ↔ a ≠ b

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
a b : Bool
⊢ a ≠ !b ↔ a = b

Tactic:
not_eq_not

Premises used: Bool.not_eq_not
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (b : Bool), (!b) ≠ b

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (b : Bool), b ≠ !b

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (a b : Bool), a = b ∨ a = !b

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {b : Bool}, (!b) = true ↔ ¬b = true

Tactic:
simp
-- Module: Mathlib.Data.Bool.Basic
Goal:
a : Bool
⊢ (!a) = false → a = true

Tactic:
decide +revert
-- Module: Mathlib.Data.Bool.Basic
Goal:
a : Bool
⊢ (!a) = true → a = false

Tactic:
decide +revert
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ bne = xor

Tactic:
constructor
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {x y : Bool}, (x ^^ y) = true ↔ x ≠ y

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (a : Bool), a ≤ a

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (a b c : Bool), a ≤ b → b ≤ c → a ≤ c

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (a b : Bool), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (a b : Bool), a ≤ b → b ≤ a → a = b

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (a b : Bool), a ≤ b ∨ b ≤ a

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (a b : Bool), min a b = if a ≤ b then a else b

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (a b : Bool), max a b = if a ≤ b then b else a

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ false < true

Tactic:
lt_iff.2 ⟨rfl, rfl⟩

Premises used: Iff.mpr, And.intro, rfl, Bool.lt_iff
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {x y : Bool}, x ≤ y ↔ x = true → y = true

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (x y : Bool), (x && y) ≤ x

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (x y : Bool), (x && y) ≤ y

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (x y : Bool), x ≤ (x || y)

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ (x y : Bool), y ≤ (x || y)

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ∀ {x y z : Bool}, x ≤ z → y ≤ z → (x || y) ≤ z

Tactic:
decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ ofNat 0 = false

Tactic:
rfl

Premises used: Decidable.decide, Bool.ofNat, rfl
-- Module: Mathlib.Data.Bool.Basic
Goal:
n : Nat
⊢ ofNat (n + 1) = true

Tactic:
rfl

Premises used: Decidable.decide, Bool.ofNat, rfl
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ (b.toNat == 0) = !b

Tactic:
grind
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ (b.toNat != 0) = b

Tactic:
simp [bne]

Premises used: bne
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
false : (Bool.false.toNat == 1) = Bool.false
true : (Bool.true.toNat == 1) = Bool.true
⊢ (b.toNat == 1) = b

Tactic:
cases b
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ (false.toNat == 1) = false

Tactic:
rfl
-- Module: Mathlib.Data.Bool.Basic
Goal:
⊢ (true.toNat == 1) = true

Tactic:
rfl
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ (b.toNat != 1) = !b

Tactic:
simp [bne]

Premises used: bne
-- Module: Mathlib.Data.Bool.Basic
Goal:
n m : Nat
h : n ≤ m
simp : (!decide (n = 0)) ≤ !decide (m = 0)
⊢ ofNat n ≤ ofNat m

Tactic:
simp only [ofNat, ne_eq, _root_.decide_not]

Premises used: decide_not, ne_eq, Bool.ofNat
-- Module: Mathlib.Data.Bool.Basic
Goal:
n m : Nat
h : n ≤ m
hn : n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
grind [Bool.false_le]

Premises used: Bool.false_le
-- Module: Mathlib.Data.Bool.Basic
Goal:
n m : Nat
h : n ≤ m
hn : ¬n = 0
h_1 : ¬m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
grind [Bool.le_true]

Premises used: Bool.le_true
-- Module: Mathlib.Data.Bool.Basic
Goal:
n m : Nat
h : n ≤ m
hn : ¬n = 0
h_1 : m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
grind [Bool.le_true]

Premises used: Bool.le_true
-- Module: Mathlib.Data.Bool.Basic
Goal:
n m : Nat
h : n ≤ m
hn : ¬n = 0
isFalse : ∀ (x : Decidable (m = 0)), (!decide (n = 0)) ≤ !decide (m = 0)
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
cases Nat.decEq m 0 with grind [Bool.le_true]

Premises used: Bool.le_true, Nat.decEq, OfNat.ofNat
-- Module: Mathlib.Data.Bool.Basic
Goal:
n m : Nat
h : n ≤ m
cases : ∀ (x : Decidable (n = 0)), (!decide (n = 0)) ≤ !decide (m = 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]

Premises used: Decidable.isTrue, Bool.le_true, Bool.false_le, Nat.decEq, Decidable.isFalse, OfNat.ofNat
-- Module: Mathlib.Data.Bool.Basic
Goal:
b₀ b₁ : Bool
h : b₀ ≤ b₁
false : ∀ (h : Bool.false ≤ b₁), Bool.false.toNat ≤ b₁.toNat
true : ∀ (h : Bool.true ≤ b₁), Bool.true.toNat ≤ b₁.toNat
⊢ b₀.toNat ≤ b₁.toNat

Tactic:
cases b₀
-- Module: Mathlib.Data.Bool.Basic
Goal:
b₁ : Bool
h : Bool.false ≤ b₁
false : ∀ (h : Bool.false ≤ Bool.false), Bool.false.toNat ≤ Bool.false.toNat
false₁ : ∀ (h : Bool.false ≤ true), Bool.false.toNat ≤ true.toNat
⊢ Bool.false.toNat ≤ b₁.toNat

Tactic:
cases b₁
-- Module: Mathlib.Data.Bool.Basic
Goal:
b₁ : Bool
h : Bool.true ≤ b₁
true : ∀ (h : Bool.true ≤ false), Bool.true.toNat ≤ false.toNat
true₁ : ∀ (h : Bool.true ≤ Bool.true), Bool.true.toNat ≤ Bool.true.toNat
⊢ Bool.true.toNat ≤ b₁.toNat

Tactic:
cases b₁
-- Module: Mathlib.Data.Bool.Basic
Goal:
h : false ≤ false
⊢ false.toNat ≤ false.toNat

Tactic:
simp_all +decide

Premises used: Decidable.decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
h : false ≤ true
⊢ false.toNat ≤ true.toNat

Tactic:
simp_all +decide

Premises used: Decidable.decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
h : true ≤ false
⊢ true.toNat ≤ false.toNat

Tactic:
simp_all +decide

Premises used: Decidable.decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
h : true ≤ true
⊢ true.toNat ≤ true.toNat

Tactic:
simp_all +decide

Premises used: Decidable.decide
-- Module: Mathlib.Data.Bool.Basic
Goal:
b : Bool
⊢ ofNat b.toNat = b

Tactic:
grind [cases Bool]

Premises used: Bool
-- Module: Mathlib.Data.Bool.Basic
Goal:
α : Sort u_1
f : Bool → α
H : f false ≠ f true
x y : Bool
⊢ f x = f y → x = y

Tactic:
grind [cases Bool]

Premises used: Bool
-- Module: Mathlib.Data.Bool.Basic
Goal:
f : Bool → Bool
x : Bool
false : ∀ (h₁ : f Bool.true = Bool.false), f (f (f x)) = f x
true : ∀ (h₁ : f Bool.true = Bool.true), f (f (f x)) = f x
⊢ f (f (f x)) = f x

Tactic:
cases h₁ : f true

Premises used: Bool.true
-- Module: Mathlib.Data.Bool.Basic
Goal:
f : Bool → Bool
x : Bool
h₁ : f true = Bool.false
false : ∀ (h₂ : f Bool.false = Bool.false), f (f (f x)) = f x
false₁ : ∀ (h₂ : f Bool.false = true), f (f (f x)) = f x
⊢ f (f (f x)) = f x

Tactic:
cases h₂ : f false

Premises used: Bool.false
-- Module: Mathlib.Data.Bool.Basic
Goal:
f : Bool → Bool
x : Bool
h₁ : f Bool.true = Bool.true
true : ∀ (h₂ : f false = false), f (f (f x)) = f x
true₁ : ∀ (h₂ : f false = Bool.true), f (f (f x)) = f x
⊢ f (f (f x)) = f x

Tactic:
cases h₂ : f false

Premises used: Bool.false
-- Module: Mathlib.Data.Bool.Basic
Goal:
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = false
⊢ f (f (f x)) = f x

Tactic:
grind [cases Bool]

Premises used: Bool
-- Module: Mathlib.Data.Bool.Basic
Goal:
f : Bool → Bool
x : Bool
h₁ : f true = false
h₂ : f false = true
⊢ f (f (f x)) = f x

Tactic:
grind [cases Bool]

Premises used: Bool
-- Module: Mathlib.Data.Bool.Basic
Goal:
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f (f x)) = f x

Tactic:
grind [cases Bool]

Premises used: Bool
-- Module: Mathlib.Data.Bool.Basic
Goal:
f : Bool → Bool
x : Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f (f x)) = f x

Tactic:
grind [cases Bool]

Premises used: Bool
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
b : Bool
⊢ 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)
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
b : Bool
this : l.length = countP (fun (x : Bool) ↦ x == !b) l + countP (fun (a : Bool) ↦ decide ¬(a == !b) = true) l
⊢ count (!b) l + count b l = l.length

Tactic:
aesop (add simp this)
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
b : Bool
⊢ count b l + count (!b) l = l.length

Tactic:
grind
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
⊢ count false l + count true l = l.length

Tactic:
count_not_add_count l true

Premises used: Bool.true, List.count_not_add_count
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
⊢ count true l + count false l = l.length

Tactic:
count_not_add_count l false

Premises used: List.count_not_add_count, Bool.false
-- Module: Mathlib.Data.Bool.Count
Goal:
b x : Bool
l : List Bool
h : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) (b :: x :: l)
⊢ count (!b) (x :: l) = count b (x :: l) + (x :: l).length % 2

Tactic:
grind [h.of_cons.count_not_cons]

Premises used: List.IsChain.of_cons
-- Module: Mathlib.Data.Bool.Count
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 []
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)
⊢ count (!b) l = count b l

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) [])
⊢ count (!b) [] = count b []

Tactic:
rfl
-- 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
⊢ count (!b) (x :: l) = count b (x :: l)

Tactic:
grind [count_cons_of_ne x.not_ne_self.symm, hl.count_not_cons]

Premises used: List.count_cons_of_ne, Ne.symm, List.IsChain.count_not_cons, Bool.not_ne_self
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
h2 : Even l.length
⊢ count false l = count true l

Tactic:
hl.count_not_eq_count h2 true

Premises used: Bool.true, 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
nil : ∀ (hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []), count (!b) [] ≤ count b [] + 1
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
⊢ count (!b) l ≤ count b l + 1

Tactic:
cases l
-- Module: Mathlib.Data.Bool.Count
Goal:
b : Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []
⊢ count (!b) [] ≤ count b [] + 1

Tactic:
zero_le

Premises used: zero_le, List.countP.go
-- Module: Mathlib.Data.Bool.Count
Goal:
b : Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) []
⊢ count (!b) [] ≤ count b [] + 1

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.Data.Bool.Count
Goal:
b 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:
grind [hl.count_not_cons]

Premises used: List.IsChain.count_not_cons
-- Module: Mathlib.Data.Bool.Count
Goal:
l : List Bool
hl : IsChain (fun (x1 x2 : Bool) ↦ x1 ≠ x2) l
⊢ count false l ≤ count true l + 1

Tactic:
hl.count_not_le_count_add_one true

Premises used: Bool.true, List.IsChain.count_not_le_count_add_one