mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
⊢ insert a (s.erase a) = s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s.erase a ⊂ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s.erase a ∪ {a} = s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∉ s
⊢ (cons a s h).erase a = s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ⊆ insert a t ↔ s.erase a ⊆ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ s \ {a} = s.erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ∩ t.erase a = (s ∩ t).erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s.erase a ∩ t = (s ∩ t).erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.erase a \ t = (s \ t).erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.erase a ∩ t = s ∩ t.erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (s ∪ t).erase a = s.erase a ∪ t.erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a (s ∩ t) = insert a s ∩ insert a t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (s \ t).erase a = s.erase a \ t.erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Finset α
a : α
ha : a ∈ t
s : Finset α
⊢ s.erase a ∪ t = s ∪ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
t : Finset α
⊢ s ∪ t.erase a = s ∪ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
hts : t ⊆ s
ha : a ∈ t
⊢ s \ t ∪ t.erase a = s.erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
⊢ s \ insert x t = (s \ t).erase x

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α
hxs : x ∈ s
hxt : x ∉ t
⊢ insert x (s \ insert x t) = s \ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ s
⊢ s \ t.erase a = insert a (s \ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ s \ s.erase a = {a}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Finset α
ha : a ∉ s
⊢ filter p (cons a s ha) = if p a then cons a (filter p s) ⋯ else filter p s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ filter p (s₁ ∪ s₂) = filter p s₁ ∪ filter p s₂

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
⊢ filter p s ∪ filter q s = filter (fun x ↦ p x ∨ q x) s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∈ t)
⊢ filter (fun i ↦ i ∈ t) s = s ∩ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∉ t)
⊢ filter (fun i ↦ i ∉ t) s = s \ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p (s ∩ t) = filter p s ∩ filter p t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p s ∩ t = filter p (s ∩ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∩ filter p t = filter p (s ∩ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (insert a s) = if p a then insert a (filter p s) else filter p s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a ↦ p a ∨ q a) s = filter p s ∪ filter q s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a ↦ p a ∧ q a) s = filter p s ∩ filter q s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a ↦ ¬p a) s = s \ filter p s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun a ↦ p a ∧ ¬q a) s = filter p s \ filter q s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ \ s₂ = filter (fun x ↦ x ∉ s₂) s₁

Tactic:
grind

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ filter (fun x ↦ x ∈ t₁) s ∪ filter (fun x ↦ x ∉ t₁) s = s

Tactic:
grind

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∈ t₁) s) ⊆ t₁

Tactic:
grind

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

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (Eq b) s = if b ∈ s then {b} else ∅

Tactic:
grind

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

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (fun a ↦ a = b) s = if b ∈ s then {b} else ∅

Tactic:
grind

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

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (fun a ↦ b ≠ a) s = s.erase b

Tactic:
grind

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

Goal state before:
pp: n m : ℕ
⊢ filter (fun x ↦ x = m) (range n) = if m < n then {m} else ∅

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s

Tactic:
by rwa [Subsingleton.elim y x]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a ∈ s, f a = b) ↔ f.symm b ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
p : (a : β) → a ∈ map f s → Prop
⊢ (∀ (y : β) (H : y ∈ map f s), p y H) ↔ ∀ (x : α) (H : x ∈ s), p (f x) ⋯

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ↑(map f s) = ⇑f '' ↑s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ↑(map f s) ⊆ Set.range ⇑f

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y ↦ y ∈ Set.range f
inst✝ : DecidableEq β
⊢ {y | y ∈ Set.range f} = image f univ

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ Multiset.map (⇑g ∘ ⇑f) s.val = Multiset.map (⇑(f.trans g)) s.val

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g (Sum.inl ⟨i, hi⟩) = f ⟨i, hi⟩

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g (Sum.inr ⟨i, hi⟩) = g ⟨i, hi⟩

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
b c : β
⊢ c ∈ image (const α b) s ↔ s.Nonempty ∧ b = c

Tactic:
grind

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

Goal state before:
pp: ⊢ univ.val = True ::ₘ {False}

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
a : α
hf : Injective f
⊢ f a ∈ image f s ↔ a ∈ s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (image f s) = image f ({a ∈ s | p (f a)})

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
a : α
⊢ image f {a} = {f a}

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
a : α
s : Finset α
⊢ image f (insert a s) = insert (f a) (image f s)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ (image f s).erase (f a) ⊆ image f (s.erase a)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
⊢ image f (s.erase a) = (image f s).erase (f a)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (image Subtype.val s.attach).val = s.val

Tactic:
image_val,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (Multiset.map Subtype.val s.attach.val).dedup = s.val
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Option β
s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
h : s ⊆ t
⊢ filterMap f s f_inj ⊆ filterMap f t f_inj

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s

Tactic:
grind

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h : ∃ a_1, ∃ (h : ∃ (x : p a_1), ⟨a_1, ⋯⟩ ∈ s), ⟨a_1, ⋯⟩ = a
⊢ a ∈ s

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h : a ∈ s
⊢ ∃ a_1, ∃ (h : ∃ (x : p a_1), ⟨a_1, ⋯⟩ ∈ s), ⟨a_1, ⋯⟩ = a

Tactic:
grind

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h : ∃ a_1, ∃ (h : p a_1), (∃ a, ∃ (h_1 : a ∈ ↑s), True ∧ ⟨a, ⋯⟩ = ⟨a_1, ⋯⟩) ∧ a_1 = a
⊢ a ∈ ↑s

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h : a ∈ ↑s
⊢ ∃ a_1, ∃ (h : p a_1), (∃ a, ∃ (h_1 : a ∈ ↑s), True ∧ ⟨a, ⋯⟩ = ⟨a_1, ⋯⟩) ∧ a_1 = a

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #({a} ∩ s) ≤ 1

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ #(insert a s) ≤ #s + 1

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #(insert a s) = if a ∈ s then #s else #s + 1

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ #{a, b} = 1 ∨ #{a, b} = 2

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #s - 1 ≤ #(s.erase a)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ (last n).rev = ⊥

Tactic:
rev_last,

Goal state after:
n : ℕ
⊢ 0 = ⊥
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : b.castSucc < i
⊢ i.pred ⋯ ≤ i.pred ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case inr.inr
n : ℕ
j : Fin (n + 1)
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
hij : j.predAbove = j.predAbove
h : j ≤ j
⊢ j = j

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ (castOrderIso ⋯).symm = castOrderIso ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ (castOrderIso ⋯).toEquiv = Equiv.cast ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
h : n = m
⊢ Fin.cast h = cast ⋯

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
h : i < p
⊢ i.succ ≠ last n

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ castPred 1 ⋯ = 1

Tactic:
rfl

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

Goal state before:
pp: case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ (ofFn fun i ↦ f (Fin.cast ⋯ (Fin.natAdd (m * n) i))) = ofFn fun j ↦ f ⟨m * n + ↑j, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ ∀ (a : α) (s_1 : Finset α),
    a ∉ s_1 → #(s ∪ s_1) + #(s ∩ s_1) = #s + #s_1 → #(s ∪ insert a s_1) + #(s ∩ insert a s_1) = #s + #(insert a s_1)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) + #(s ∪ t) = #s + #t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∪ t) = #s + #t - #(s ∩ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ a ∈ Set.range f

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) = #s + #t - #(s ∪ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∪ t) ≤ #s + #t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(t \ s) = #(t \ (s ∩ t))

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ∩ t ⊆ t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) + #s = #t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #t - #s = #t - #(s ∩ t) - #(s \ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #t - #(s ∩ t) - #(s \ t) = #(t \ (s ∩ t)) - #(s \ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(t \ (s ∩ t)) - #(s \ t) = #(t \ s) - #(s \ t)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #t - #s ≤ #(t \ s)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #s ≤ #(s \ t) + #t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : #s < #t
⊢ (t \ s).Nonempty

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) + #(s \ t) = #s

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) ≤ #(t \ s) ↔ #s ≤ #t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) < #(t \ s) ↔ #s < #t

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s \ t) = #(t \ s) ↔ #s = #t

Tactic:
grind

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
f : Fin n → α
⊢ (Fin.cons a f 0 :: ofFn fun i ↦ Fin.cons a f i.succ) = a :: ofFn f

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ (u \ s).Nonempty

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
a✝ : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ s ⊆ u.erase a ∧ u.erase a ⊆ t ∧ #(u.erase a) = k

Tactic:
grind

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ (!p (ofFn f)[j]) = true

Tactic:
simpa using! h ⟨j, by lia⟩ (by simpa using! hj)

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

Goal state before:
pp: case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ f ≍ f

Tactic:
rfl

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
i✝ : ℕ
a✝ : α
⊢ (ofFn f)[i✝]? = some a✝ ↔ (pmap (fun i hi ↦ f ⟨i, hi⟩) (range n) ⋯)[i✝]? = some a✝

Tactic:
grind

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

Goal state before:
pp: case mp
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ s, insert a s = t) → s ⊆ t ∧ #s + 1 = #t

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = cons x p (succ 0)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
⊢ #(t \ s) = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p (last (n + 1)) = cons x p (last n).succ

Tactic:
rfl

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∃ a, s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
grind

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

Goal state before:
pp: a : Fin 2
⊢ a = 0 ↔ a = 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
x : α
hx : x ∈ s
h : ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ s = {x}

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : j = 0
⊢ (g ∘ cons y q) 0 = cons (g y) (g ∘ q) 0

Tactic:
rfl

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → #s = 2

Tactic:
grind

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3

Tactic:
grind

Goal state after: