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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ ∀ (a : α), a ∈ (s ∩ t).toFinset ↔ a ∈ s.toFinset ∩ t.toFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : α
⊢ ↑{a} ≠ ↑univ

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ ∀ (a : α), a ∈ (filter p univ)ᶜ ↔ a ∈ {x | ¬p x}

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.toList.isEmpty = true ↔ s = ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ univ ∩ s ↔ a ∈ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a : α
⊢ {a} = univ

Tactic:
ext b

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a b : α
⊢ b ∈ {a} ↔ b ∈ univ
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
b : β
⊢ e.toEmbedding (e.symm b) = b

Tactic:
simp

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

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

Tactic:
by
  simp only [mem_map, Equiv.coe_toEmbedding]
  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 ↦ ∃ x, f x = y
inst✝ : DecidableEq β
a✝ : β
⊢ a✝ ∈ {y | ∃ x, f x = y} ↔ a✝ ∈ image f univ

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
s : Finset α
⊢ map (Equiv.cast ⋯).toEmbedding s ≍ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Finset.subtype p univ = univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ {x | x ∈ s} = s

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
h : IsEmpty α
⊢ {∅} ⊆ Set.univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
x✝ : IsEmpty α
⊢ Set.univ = {∅}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
s : Finset α
x y : ↥s
⊢ (fun x ↦ ⟨f ↑x, ⋯⟩) x = (fun x ↦ ⟨f ↑x, ⋯⟩) y → x = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n i j : ℕ
⊢ (fun i ↦ i + 1) i = (fun i ↦ i + 1) j → i = j

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ Subsingleton ↥s.toFinset ↔ s.Subsingleton

Tactic:
simp

Goal state after:
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)
a✝ : α
⊢ a✝ ∈ (s ∩ t).toFinset ↔ a✝ ∈ s.toFinset ∩ t.toFinset

Tactic:
simp

Goal state after:
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)
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset

Tactic:
simp

Goal state after:
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)
a✝ : α
⊢ a✝ ∈ (s \ t).toFinset ↔ a✝ ∈ s.toFinset \ t.toFinset

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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
⊢ (∀ y ∈ image f s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

Tactic:
simp

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
⊢ (∃ y ∈ image f s, p y) ↔ ∃ x ∈ s, p (f x)

Tactic:
simp

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

Goal state before:
pp: α : 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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a✝ : α
b c✝ : β
c : α → β
p : β → Prop
inst✝ : CanLift β α c p
val✝ : Multiset β
l : List α
hd : (List.map c l).Nodup
a : β
⊢ a ∈ image c { val := ↑l, nodup := ⋯ } ↔ a ∈ { val := Quot.mk (⇑(List.isSetoid β)) (List.map c l), nodup := hd }

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset ⊂ Finset.univ ↔ s ⊂ univ

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : 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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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
a✝ : α
⊢ a✝ ∈ (insert a s).toFinset ↔ a✝ ∈ insert a s.toFinset

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
⊢ {True, False}.Nodup

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
⊢ univ.val = True ::ₘ {False}
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype α
⊢ ∀ (x : α), x ∈ filter p univ ↔ p x

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
b : β
⊢ b ∈ image f univ ↔ b ∈ Set.range f

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: case inl
a : Int
ha : 0 ≤ a
b : Int
hc : 0 ≤ 0
⊢ a * (b / 0) ≤ a * b / 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
f g : α → β
s✝ : Finset α
t : Finset β
a✝ : α
b c : β
a : α
s : Finset α
ha : a ∉ s
x y : ↥s
⊢ (fun x ↦ ⟨↑x, ⋯⟩) x = (fun x ↦ ⟨↑x, ⋯⟩) y → x = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
ha : a ∉ s
⊢ (cons a s ha).attach = cons ⟨a, ⋯⟩ (map { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach) ⋯

Tactic:
ext ⟨x, hx⟩; simpa using hx

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).attach = insert ⟨a, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)

Tactic:
ext ⟨x, hx⟩; simpa using hx

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

Goal state before:
pp: case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
⊢ (image f)^[0] s = image f^[0] s

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x ↦ x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ range (0 + 1) \ {0} = image Nat.succ (range 0)

Tactic:
simp

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

Goal state before:
pp: case succ.h
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ k + 1 ∉ {0}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ (Equiv.refl α).finsetCongr x✝ ↔ a✝ ∈ (Equiv.refl (Finset α)) x✝

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Fin.cast ⋯ i.rev = (Fin.cast ⋯ i).rev

Tactic:
simp

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
y : Fin m
xin : y ∈ {i | m ≤ ↑i + n}
⊢ ((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) (subNat (m - n) (Fin.cast ⋯ y) ⋯) = y

Tactic:
simp

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ min (↑a) n = ↑a

Tactic:
simp

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ max (↑a) n = n

Tactic:
simp

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 < n + 1

Tactic:
Nat.lt_add_left_iff_pos,

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 < last (n + 1)

Tactic:
rw [lt_def, val_one, val_last, Nat.lt_add_left_iff_pos, Nat.pos_iff_ne_zero]
  exact NeZero.ne n

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

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

Tactic:
simp

Goal state after:
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
⊢ image (fun a ↦ i ↑a ⋯) s.attach = t

Tactic:
ext b

Goal state after:
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
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : 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
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ ⟨a, ha⟩ ∈ s.attach ∧ i ↑⟨a, ha⟩ ⋯ = i a ha

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ finCongr ⋯ = Equiv.cast ⋯

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
t : Finset β
f : ↥∅ → ↥t
hf : Injective f
⊢ #∅ ≤ #t

Tactic:
simp

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ 1 % (n + 1) - 1 = 0

Tactic:
Nat.sub_eq_zero_iff_le,

Goal state after:
n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ 1 % (n + 1) ≤ 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
h : ¬last (n + 1) = 0
⊢ (last (n + 1)).pred h = last n

Tactic:
← succ_last,

Goal state after:
n : ℕ
h : ¬last (n + 1) = 0
⊢ (last n).succ.pred ⋯ = last n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc + 1 = a

Tactic:
simp

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

Goal state before:
pp: n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : ℕ
hi : i < n
⊢ motive ⟨i, hi⟩

Tactic:
induction i using Nat.strong_induction_on with
  | h j hj => exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)

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

Goal state before:
pp: case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
⊢ ∀ (i_1 : Fin n),
    ((fun x1 x2 ↦ x1 < x2) i i_1.castSucc → r (f i) (f i_1.castSucc)) →
      (fun x1 x2 ↦ x1 < x2) i i_1.succ → r (f i) (f i_1.succ)

Tactic:
intro j

Goal state after:
case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
⊢ ((fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)) → (fun x1 x2 ↦ x1 < x2) i j.succ → r (f i) (f j.succ)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr.refine_2
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij : i ≤ j.castSucc
⊢ r (f i) (f j.succ)

Tactic:
obtain hij | hij := (le_def.1 hij).eq_or_lt

Goal state after:
case mpr.refine_2.inl
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i = ↑j.castSucc
⊢ r (f i) (f j.succ)

case mpr.refine_2.inr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i < ↑j.castSucc
⊢ r (f i) (f j.succ)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case zero
⊢ ↑(-1) = 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ ↑(last n - i) = ↑i.rev

Tactic:
by rw [coe_sub_iff_le.2 i.le_last, val_last, val_rev, Nat.succ_sub_succ_eq_sub]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ (ofFn f).length = n

Tactic:
simp

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ (ofFn f).get i = f (Fin.cast ⋯ i)

Tactic:
simp

Goal state after:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ f ⟨↑i, ⋯⟩ = f (Fin.cast ⋯ i)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
hinj' : Set.InjOn f' ↑s.attach
⊢ ⟨a₁, ha₁⟩ ∈ ↑s.attach

Tactic:
simp

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ ≤ b ↔ a < b

Tactic:
rw [succ_castPred_eq_castPred_succ ha, castpred_succ_le_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
hinj' : Set.InjOn f' ↑s.attach
⊢ ⟨a₂, ha₂⟩ ∈ ↑s.attach

Tactic:
simp

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 f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
| succ m IH =>

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
P : α → Prop
⊢ (∀ (i : α), i ∈ ofFn f → P i) ↔ ∀ (j : Fin n), P (f j)

Tactic:
simp

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

Goal state before:
pp: α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = c :: ofFn fun x ↦ c

Tactic:
simp

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i.succ.succAbove 0 = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ #∅ ≤ n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
h : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
exact exists_subset_card_eq h

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

Goal state before:
pp: n : ℕ
a✝ : Fin n
⊢ a✝ ∈ (finRange n).toFinset ↔ a✝ ∈ univ

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i m : Fin (n + 1)
⊢ m ∈ image i.succAbove univ ↔ m ∈ {i}ᶜ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
p : Fin (n + 1)
⊢ p ∉ map p.succAboveEmb univ

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
⊢ #∅ ≤ 1 ↔ ∀ a ∈ ∅, ∀ b ∈ ∅, a = b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → β
⊢ image (fun x ↦ f (l.get x)) univ = (List.map f l).toFinset

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
y : α
⊢ ∀ (x : α), x ∈ {y} ↔ x = y

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.11
β : Type ?u.10
inst✝² : DecidableEq α
inst✝¹ : Fintype (α × β)
inst✝ : Nonempty β
a : α
⊢ a ∈ image Prod.fst univ

Tactic:
simp

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

Goal state before:
pp: case zero
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (cons x p) 0 z 0 = cons z p 0

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type ?u.11
β : Type ?u.10
inst✝² : DecidableEq β
inst✝¹ : Fintype (α × β)
inst✝ : Nonempty α
b : β
⊢ b ∈ image Prod.snd univ

Tactic:
simp

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

Goal state before:
pp: case succ
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
i✝ : Fin n
⊢ update (cons x p) 0 z i✝.succ = cons z p i✝.succ

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ (a : α), β a
x✝ : (a : α) ×' β a
fst✝ : α
snd✝ : β fst✝
⊢ ⟨fst✝, snd✝⟩ ∈ {⟨⋯, ⋯⟩}

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.8
inst✝¹ : Nonempty α
inst✝ : Fintype α
⊢ ∃ x, x ∈ univ.val

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Fin (n + 1) → Type u_1
f : α 0 × ((i : Fin n) → α i.succ)
⊢ (fun f ↦ (f 0, tail f)) ((fun f ↦ cons f.1 f.2) f) = f

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
⊢ (fun f ↦ cons f.1 f.2) ((fun f ↦ (f 0, tail f)) f) = f

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
⊢ ∀ x ∈ ∅, P x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
⊢ #∅ = n + 1 → ∃ a t, ∃ (h : a ∉ t), cons a t h = ∅ ∧ #t = n

Tactic:
simp

Goal state after: