mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → q a) → p (foldr f x s)
q_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
⊢ p (foldr f x (a ::ₘ s))

Tactic:
simp only [forall_mem_cons, foldr_cons] at q_s ⊢

Goal state after:
case cons
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → q a) → p (foldr f x s)
q_s : q a ∧ ∀ (x : α), x ∈ s → q x
⊢ p (f a (foldr f x s))
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ∩ t + u = (s + u) ∩ (t + u)

Tactic:
by_contra! h
  obtain ⟨a, ha⟩ := lt_iff_cons_le.1 <| h.lt_of_le <| le_inter
    (Multiset.add_le_add_right inter_le_left) (Multiset.add_le_add_right inter_le_right)
  rw [← cons_add] at ha
  exact (lt_cons_self (s ∩ t) a).not_ge <| le_inter
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_left))
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_right))

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
⊢ ↑s ∩ ↑t = ↑(s.bagInter t)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(s.bagInter t)
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.val.toFinset = s

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ s.val.toFinset ↔ a✝ ∈ s
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.toList.toFinset = s

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ s.toList.toFinset ↔ a✝ ∈ s
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
x y : α
⊢ [x] <:+: [y] ↔ x = y

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
x y : α
⊢ [x] <:+: [y] → x = y

case mpr
α : Type u_1
x y : α
⊢ x = y → [x] <:+: [y]
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] ↔ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] → head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

case mpr
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x] → head✝¹ :: head✝ :: tail✝ <:+: [x]
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.inits.length = l.length + 1

Tactic:
by simp [inits_eq_tails]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Tactic:
simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ ↑(cons a s h) = insert a ↑s

Tactic:
ext

Goal state after:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
x✝ : α
⊢ x✝ ∈ ↑(cons a s h) ↔ x✝ ∈ insert a ↑s
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
by by_cases h : a ∈ l <;> simp [h]

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

Goal state before:
pp: α : Type u_1
h : DecidablePred fun x ↦ True
s : Finset α
⊢ filter (fun x ↦ True) s = s

Tactic:
ext

Goal state after:
α : Type u_1
h : DecidablePred fun x ↦ True
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x ↦ True) s ↔ a✝ ∈ s
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
h : DecidablePred fun x ↦ False
s : Finset α
⊢ filter (fun x ↦ False) s = ∅

Tactic:
ext

Goal state after:
α : Type u_1
h : DecidablePred fun x ↦ False
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x ↦ False) s ↔ a✝ ∈ ∅
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ⊆ filter (fun x ↦ p x ∧ ¬q x) s
⊢ x✝ ⊆ filter (fun x ↦ q x ∧ ¬p x) s → x✝ ⊆ ⊥

Tactic:
htq

Goal state after:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ⊆ filter (fun x ↦ p x ∧ ¬q x) s
htq : x✝ ⊆ filter (fun x ↦ q x ∧ ¬p x) s
⊢ x✝ ⊆ ⊥
Module: Mathlib.Data.Finset.SDiff

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
⊢ insert a s \ insert b s = {a}

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
a✝ : α
⊢ a✝ ∈ insert a s \ insert b s ↔ a✝ ∈ {a}
Module: Mathlib.Data.Finite.Defs

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ s.Finite ↔ t.Finite

Tactic:
← Set.finite_coe_iff,

Goal state after:
α : Type u
β : Type v
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ Finite ↑s ↔ Finite ↑t
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ ↑univ = Set.univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Fintype α
x✝ : α
⊢ x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ
Module: Mathlib.Data.Finset.Basic

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

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
a✝ : α
⊢ a✝ ∈ s.erase a \ s.erase b ↔ a✝ ∈ {b}
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) ↔ ∀ x ∈ s, p x → ¬q x

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) → ∀ x ∈ s, p x → ¬q x

case mpr
α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (∀ x ∈ s, p x → ¬q x) → Disjoint (filter p s) (filter q s)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ Disjoint (filter p s) (filter q t)

Tactic:
disjoint_left,

Goal state after:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ ∀ ⦃a : α⦄, a ∈ filter p s → a ∉ filter q t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: m n : ℕ
⊢ range m ∩ range n = range (min m n)

Tactic:
ext

Goal state after:
m n a✝ : ℕ
⊢ a✝ ∈ range m ∩ range n ↔ a✝ ∈ range (min m n)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: m n : ℕ
⊢ range m ∪ range n = range (max m n)

Tactic:
ext

Goal state after:
m n a✝ : ℕ
⊢ a✝ ∈ range m ∪ range n ↔ a✝ ∈ range (max m n)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset
Module: Mathlib.Data.Finset.Basic

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

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter p s.toFinset
Module: Mathlib.Data.Finset.BooleanAlgebra

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

Tactic:
ext

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (s.erase a)ᶜ ↔ a✝ ∈ insert a sᶜ
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
a✝ : α
⊢ a✝ ∈ (l ∪ l').toFinset ↔ a✝ ∈ l.toFinset ∪ l'.toFinset
Module: Mathlib.Data.Finset.BooleanAlgebra

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

Tactic:
ext

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (insert a s)ᶜ ↔ a✝ ∈ sᶜ.erase a
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
a✝ : α
⊢ a✝ ∈ (l ∩ l').toFinset ↔ a✝ ∈ l.toFinset ∩ l'.toFinset
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
⊢ (filter p s).toFinset = Finset.filter (fun x ↦ p x = true) s.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter (fun x ↦ p x = true) s.toFinset
Module: Mathlib.Data.Finset.BooleanAlgebra

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y ↦ ∃ x, f x = y
inst✝ : DecidableEq β
a✝ : β
⊢ a✝ ∈ {y | ∃ x, f x = y} ↔ a✝ ∈ image f univ
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t ↔ map f.toEmbedding s ⊆ t

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t → map f.toEmbedding s ⊆ t

case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ map f.toEmbedding s ⊆ t → s ⊆ map f.symm.toEmbedding t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ n ≠ 0 ∧ x = a ↔ x ∈ if n = 0 then ∅ else {a}

Tactic:
split_ifs with hn <;> simp [hn]

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

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = insert 0 (map { toFun := fun i ↦ i + 1, inj' := ⋯ } (range n))

Tactic:
ext (⟨⟩ | ⟨n⟩)

Goal state after:
case zero
n : ℕ
⊢ 0 ∈ range (n + 1) ↔ 0 ∈ insert 0 (map { toFun := fun i ↦ i + 1, inj' := ⋯ } (range n))

case succ
n✝ n : ℕ
⊢ n + 1 ∈ range (n✝ + 1) ↔ n + 1 ∈ insert 0 (map { toFun := fun i ↦ i + 1, inj' := ⋯ } (range n✝))
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∩ t)
⊢ (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∩ t)
a✝ : α
⊢ a✝ ∈ (s ∩ t).toFinset ↔ a✝ ∈ s.toFinset ∩ t.toFinset
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∪ t)
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∪ t)
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
⊢ (s \ t).toFinset = s.toFinset \ t.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
a✝ : α
⊢ a✝ ∈ (s \ t).toFinset ↔ a✝ ∈ s.toFinset \ t.toFinset
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
⊢ (s ∆ t).toFinset = s.toFinset ∆ t.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∆ t)
a✝ : α
⊢ a✝ ∈ (s ∆ t).toFinset ↔ a✝ ∈ s.toFinset ∆ t.toFinset
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype α
inst✝ : Fintype ↑sᶜ
⊢ sᶜ.toFinset = s.toFinsetᶜ

Tactic:
ext

Goal state after:
α : Type u_1
s : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype α
inst✝ : Fintype ↑sᶜ
a✝ : α
⊢ a✝ ∈ sᶜ.toFinset ↔ a✝ ∈ s.toFinsetᶜ
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝ : Fintype ↑∅
⊢ ∅.toFinset = ∅

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Fintype ↑∅
a✝ : α
⊢ a✝ ∈ ∅.toFinset ↔ a✝ ∈ ∅
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
⊢ univ.toFinset = Finset.univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
a✝ : α
⊢ a✝ ∈ univ.toFinset ↔ a✝ ∈ Finset.univ
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
⊢ {x | p x}.toFinset = filter p Finset.univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
a✝ : α
⊢ a✝ ∈ {x | p x}.toFinset ↔ a✝ ∈ filter p Finset.univ
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
⊢ (range f).toFinset = Finset.image f Finset.univ

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
a✝ : α
⊢ a✝ ∈ (range f).toFinset ↔ a✝ ∈ Finset.image f Finset.univ
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Fintype ↑{a}
⊢ {a}.toFinset = {a}

Tactic:
ext

Goal state after:
α : Type u_1
a : α
inst✝ : Fintype ↑{a}
a✝ : α
⊢ a✝ ∈ {a}.toFinset ↔ a✝ ∈ {a}
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
a : α
s : Set α
inst✝¹ : Fintype ↑(insert a s)
inst✝ : Fintype ↑s
⊢ (insert a s).toFinset = insert a s.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
a : α
s : Set α
inst✝¹ : Fintype ↑(insert a s)
inst✝ : Fintype ↑s
a✝ : α
⊢ a✝ ∈ (insert a s).toFinset ↔ a✝ ∈ insert a s.toFinset
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {x | x ∈ s} = s.toFinset

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : α
⊢ a✝ ∈ {x | x ∈ s} ↔ a✝ ∈ s.toFinset
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
⊢ image f s = image g s

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ image f s ⊆ t ↔ f '' ↑s ⊆ ↑t

Tactic:
by norm_cast

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f ↔ a ∈ image (fun i ↦ f i) (range n)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f → a ∈ image (fun i ↦ f i) (range n)

case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i ↦ f i) (range n) → a ∈ Set.range f
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Finset.subtype (fun x ↦ x ∈ s) s = s.attach

Tactic:
ext

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : ↥s
⊢ a✝ ∈ Finset.subtype (fun x ↦ x ∈ s) s ↔ a✝ ∈ s.attach
Module: Mathlib.Data.Finset.Image

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

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s → ∃ s', ↑s' ⊆ s ∧ image f s' = t

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
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
⊢ (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)

Tactic:
ext

Goal state after:
α : Type u_1
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ (Equiv.refl α).finsetCongr x✝ ↔ a✝ ∈ (Equiv.refl (Finset α)) x✝
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
x✝ : Finset α
a✝ : γ
⊢ a✝ ∈ (e.finsetCongr.trans e'.finsetCongr) x✝ ↔ a✝ ∈ (e.trans e').finsetCongr x✝
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
⊢ a ∈
      (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
        ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s) ↔
    a ∈ s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
⊢ a ∈
      (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
        ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s) →
    a ∈ s

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
⊢ a ∈ s →
    a ∈
      (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
        ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
⊢ a ∈
      ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
          ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s)) ↔
    a ∈ ↑s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
⊢ a ∈
      ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
          ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s)) →
    a ∈ ↑s

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
⊢ a ∈ ↑s →
    a ∈
      ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
          ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s))
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
P : α → Prop
inst✝ : DecidablePred P
h : l.Nodup
⊢ #(Finset.filter P l.toFinset) = countP (fun b ↦ decide (P b)) l

Tactic:
rw [l.countP_eq_length_filter, l.filter_toFinset P]
  exact toFinset_card_of_nodup (h.filter P)

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

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f ↔ ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f → ∀ (i : Fin n), f i.castSucc ≠ f i.succ

case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ (∀ (i : Fin n), f i.castSucc ≠ f i.succ) → Injective ⇑f
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ a ∈ s → ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a

case mpr
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ (∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a) → a ∈ s
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ p.predAbove a ≤ p.predAbove b

Tactic:
by
  dsimp [predAbove]
  split_ifs with ha hb hb
  all_goals simp only [le_iff_val_le_val, val_pred]
  · exact pred_le_pred H
  · calc
      _ ≤ _ := Nat.pred_le _
      _ ≤ _ := H
  · exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)
  · exact H

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

Goal state before:
pp: n : ℕ
h : n = n
⊢ castOrderIso h = OrderIso.refl (Fin n)

Tactic:
ext

Goal state after:
n : ℕ
h : n = n
x✝ : Fin n
⊢ ↑((castOrderIso h) x✝) = ↑((OrderIso.refl (Fin n)) x✝)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach ↔ b ∈ t

Tactic:
constructor

Goal state after:
case calc_2.mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach → b ∈ t

case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
⊢ b ∈ t → b ∈ image (fun a ↦ i ↑a ⋯) s.attach
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ↑n = 0

Tactic:
ext

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ ↑↑n = ↑0
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n = last n

Tactic:
ext

Goal state after:
n : ℕ
⊢ ↑↑n = ↑(last n)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ castLE h ↑a = ↑(a % m)

Tactic:
ext

Goal state after:
m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ ↑(castLE h ↑a) = ↑↑(a % m)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
⊢ i.rev.modNat = i.modNat.rev

Tactic:
ext

Goal state after:
n m : ℕ
i : Fin (m * n)
⊢ ↑i.rev.modNat = ↑i.modNat.rev
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
h : n = n
⊢ finCongr h = Equiv.refl (Fin n)

Tactic:
ext

Goal state after:
n : ℕ
h : n = n
x✝ : Fin n
⊢ ↑((finCongr h) x✝) = ↑((Equiv.refl (Fin n)) x✝)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin n
⊢ ↑↑a = a.castSucc

Tactic:
ext

Goal state after:
n : ℕ
a : Fin n
⊢ ↑↑↑a = ↑a.castSucc