mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Lattice

Goal state before:
pp: case empty
α : Type u_2
inst✝ : DecidableEq α
⊢ (sup 0).Nodup ↔ ∀ (a : Multiset α), a ∈ 0 → a.Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ ((decode (unpair n).1).bind fun a ↦ Option.map (Sigma.mk a) (decode (unpair n).2)) =
    some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ofNat (α × β) n = (ofNat α (unpair n).1, ofNat β (unpair n).2)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: x✝ : ℕ
⊢ ofNat (ℕ × ℕ) x✝ = unpair x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ inl x ∈ u.toLeft.disjSum u.toRight ↔ inl x ∈ u

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ inr x ∈ u.toLeft.disjSum u.toRight ↔ inr x ∈ u

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : α
⊢ x ∈ (s.disjSum t).toLeft ↔ x ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ [a].maximum = max ↑a [].maximum

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
x : β
⊢ x ∈ (s.disjSum t).toRight ↔ x ∈ t

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toRight ↔ x ∈ u.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : α
⊢ y ∈ (cons (inl a) u ha).toLeft ↔ y ∈ cons a u.toLeft ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : α
⊢ y ∈ (cons (inr b) u hb).toLeft ↔ y ∈ u.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
ha : inl a ∉ u
y : β
⊢ y ∈ (cons (inl a) u ha).toRight ↔ y ∈ u.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
hb : inr b ∉ u
y : β
⊢ y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (image Sum.swap u).toLeft ↔ x ∈ u.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (image Sum.swap u).toRight ↔ x ∈ u.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inl a) u).toLeft ↔ y ∈ insert a u.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case bot
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
hmax : t.maximum = ⊥
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
refine ⟨0, le_antisymm bot_le (le_of_not_gt fun h => List.not_mem_nil (a := (⊥ : s)) ?_)⟩
      rwa [← List.maximum_eq_bot.1 hmax, hmt]

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
a : α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inl a) u).toRight ↔ y ∈ u.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : β
⊢ y ∈ (insert (inr b) u).toRight ↔ y ∈ insert b u.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∩ v).toLeft ↔ x ∈ u.toLeft ∩ v.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u ∩ v).toRight ↔ x ∈ u.toRight ∩ v.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u ∪ v).toRight ↔ x ∈ u.toRight ∪ v.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u \ v).toLeft ↔ x ∈ u.toLeft \ v.toLeft

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : β
⊢ x ∈ (u \ v).toRight ↔ x ∈ u.toRight \ v.toRight

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
s✝ : Finset α✝
t : Finset β✝
s₁ s₂ : Finset α✝
t₁ t₂ : Finset β✝
a✝ : α✝
b✝ : β✝
x : α✝ ⊕ β✝
u v : Finset (α✝ ⊕ β✝)
a : α✝
b : β✝
α : Type u_4
β : Type u_5
s : Finset α × Finset β
⊢ (fun s ↦ (s.toLeft, s.toRight)) ((fun s ↦ s.1.disjSum s.2) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
⊢ ([] ++ l₂).maximum = max [].maximum l₂.maximum

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ toFunAux x = #({y ∈ range ↑x | y ∈ s})

Tactic:
toFunAux,

Goal state after:
s : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑s
⊢ List.countP (fun x ↦ decide (x ∈ s)) (List.range ↑x) = #({y ∈ range ↑x | y ∈ s})
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
⊢ ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ [] → ↑a ≤ b
⊢ [].maximum ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithBot α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → ↑a ≤ b) → l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → ↑a_1 ≤ b
⊢ a ∈ a :: l

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b

Tactic:
induction l <;> simp [maximum_cons, *]

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a : α
h : ∀ (x : α), x ∈ [] → x ≤ a
⊢ foldr max ⊥ [] ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : Max α
inst✝ : SemilatticeSup β
P : β → Prop
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ∀ (a b : { x // P x }), ↑(a ⊔ b) = ↑a ⊔ ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.max = max ↑a ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderTop α
s : Finset α
⊢ (∃ b ∈ s, ↑b = ⊤) ↔ ⊤ ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.min = min ↑a ↑b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
x✝ : [].length = [].length
⊢ Forall p (zipWith f [] []) ↔ Forall₂ (fun x y ↦ p (f x y)) [] []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
init tail : List α
⊢ (init, tail) ∈ ([], []) :: [].zip [] ↔ init ++ tail = []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r₁ r₂ : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α), x.toList ++ [a :: y] = (x.push (a :: y)).toList

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.min' ⋯ = min a b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.max' ⋯ = max a b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : {x_1 ∈ s | x < x_1}.Nonempty
aux : {x_1 ∈ s | x < x_1}.min' Hne ∈ s ∧ x < {x_1 ∈ s | x < x_1}.min' Hne
⊢ x < {x_1 ∈ s | x < x_1}.min' Hne

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)

Goal state after:
case mp.inl
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl

case mp.inr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ tl.inits.zip tl.tails
⊢ (fun t ↦ hd :: t) w✝¹ ++ id w✝ = hd :: tl
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mp.inl
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mpr.nil
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
⊢ [] ++ tail = hd :: tl →
    ([], tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = ([], tail)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

Tactic:
obtain - | ⟨-, h⟩ | ⟨-, h⟩ := h

Goal state after:
case cons.mpr.cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

case cons.mpr.cons_cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α), x.toList ++ [y, a :: y] = ((x.push y).push (a :: y)).toList

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case nil
α : Type u_1
l₁ l₂ : List α
⊢ powersetAux' [] ~ powersetAux' []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ ∀ (a : List α), (powerset ⟦a⟧).card = 2 ^ card ⟦a⟧

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
l₂ : List α
⊢ foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      [] =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] [])

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux' l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
rw [revzip, powersetAux', ← map_reverse, zip_map, ← revzip, List.mem_map] at h
  simp only [Prod.map_apply, Prod.exists] at h
  rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
  exact Quot.sound (revzip_sublists' _ _ _ h)

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ (sublistsLen 0 l).length = l.length.choose 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n✝ : ℕ
⊢ (sublistsLen (n✝ + 1) []).length = [].length.choose (n✝ + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ sublistsLen 0 l <+ l.sublists'

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case zero
α : Type u
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen 0 l₁ <+ sublistsLen 0 l₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case zero
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetCardAux 0 l₁ ~ powersetCardAux 0 l₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case slnil
α : Type u
l l' : List α
⊢ [] ∈ sublistsLen [].length []

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.nil
α : Type u
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen [].length l₂
⊢ [] ∈ sublistsLen [].length (a :: l₂)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ (map f []).sublists = map (map f) [].sublists

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case empty
α : Type u_1
⊢ powersetCard (card 0) 0 = {0}

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ (map f []).sublists' = map (map f) [].sublists'

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ ∀ (a : List (Fin l.length)), a ∈ (finRange l.length).sublists ↔ a ∈ (finRange l.length).sublists'

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    (l'.sublists ++ map (fun x ↦ x ++ [a]) l'.sublists).zip
      ((map (fun x ↦ x ++ [a]) l'.sublists).reverse ++ l'.sublists.reverse)
⊢ l'.sublists.length = (map (fun x ↦ x ++ [a]) l'.sublists).reverse.length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l.sublists'.length = (map (cons a) l.sublists').reverse.length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s x✝ : Finset α
⊢ x✝ ∈ ↑s.powerset ↔ x✝ ∈ SetLike.coe ⁻¹' 𝒫 ↑s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ∅ ∈ s.powerset

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s ∈ s.powerset

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Finite.Powerset

Goal state before:
pp: α : Type u
a : Set α
h : a.Finite
⊢ {b | b ⊆ a}.Finite

Tactic:
convert! ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet

Goal state after:
α : Type u
a : Set α
h : a.Finite
⊢ {b | b ⊆ a} = ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)
Module: Mathlib.Data.Set.Finite.Range

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
f : ι → α
inst✝ : Fintype (PLift ι)
⊢ ∀ (x : α), x ∈ Finset.image (f ∘ PLift.down) Finset.univ ↔ x ∈ range f

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s✝ t s : Finset α
p : Finset α → Prop
inst✝ : (t : Finset α) → Decidable (p t)
⊢ (∃ t, ∃ (_ : t ⊆ s), p t) ↔ ∃ t ⊆ s, p t

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s✝ t s : Finset α
p : Finset α → Prop
inst✝ : (t : Finset α) → Decidable (p t)
⊢ (∀ t ⊆ s, p t) ↔ ∀ t ⊆ s, p t

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
⊢ (∃ a, (a ⊆ t \ s ∧ #a = n - #s) ∧ a ∪ s = x) → (x ⊆ t ∧ #x = n) ∧ s ⊆ x

Tactic:
· rintro ⟨y, ⟨hyt, hyn⟩, rfl⟩
    refine ⟨⟨union_subset (hyt.trans sdiff_subset) hst, ?_⟩, subset_union_right⟩
    rw [card_union_of_disjoint (disjoint_of_subset_left hyt disjoint_sdiff_self_left), hyn]
    lia

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
⊢ (fun x ↦ x.sup f) (insert a t) = f a ⊔ t.sup f

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
⊢ none ∉ map Embedding.some s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ some a = none ∨ some a ∈ (map Embedding.some s).val ↔ ∀ a_1 ∈ some a, a_1 ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ some a ∈ insertNone s ↔ a ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ none ∈ insertNone s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h : n ≤ #s
⊢ ∀ (a : Finset α), a ⊆ s ∧ #a = n → a ∈ powersetCard n s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
p : Option α → Prop
⊢ (∀ a ∈ eraseNone s, p (some a)) ↔ ∀ (a : α), some a ∈ s → p (some a)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

Tactic:
cases isEmpty_or_nonempty α
  · exact ⟨⊥, isEmptyElim⟩
  obtain ⟨_, ⟨t, rfl⟩, ht⟩ := wellFounded_gt.has_min _ (Set.range_nonempty (sup · f))
  refine ⟨t, fun a ↦ ?_⟩
  classical
  have := ht (f a ⊔ t.sup f) ⟨insert a t, by simp⟩
  rwa [right_lt_sup, not_not] at this

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone s ↔ a✝ ∈ s.biUnion Option.toFinset

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
a✝ : α
⊢ a✝ ∈ eraseNone (map Embedding.some s) ↔ a✝ ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone (s ∪ t) ↔ a✝ ∈ eraseNone s ∪ eraseNone t

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone (s ∩ t) ↔ a✝ ∈ eraseNone s ∩ eraseNone t

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
a✝ : α
⊢ a✝ ∈ eraseNone ∅ ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
a✝ : α
⊢ a✝ ∈ eraseNone {none} ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: case none
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ image some (eraseNone s) ↔ none ∈ s.erase none

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: case some
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ image some (eraseNone s) ↔ some x ∈ s.erase none

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mpr
α : Type u_1
a✝ : Finset α
⊢ a✝ ⊆ a✝ ∧ #a✝ = #a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: case none
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ insertNone (eraseNone s) ↔ none ∈ insert none s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: case some
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ insertNone (eraseNone s) ↔ some x ∈ insert none s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset α
a✝ : α
⊢ a✝ ∈ eraseNone (insertNone s) ↔ a✝ ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Fintype α
a : Option α
⊢ a ∈ insertNone univ

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α : Type u_3
inst✝ : Fintype α
⊢ none ∉ map Embedding.some univ

Tactic:
simp

Goal state after: