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

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

Tactic:
constructor

Goal state after:
case mp
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f → ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ n✝ + 1 < n✝ + 1 + 1

Tactic:
constructor

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

Goal state before:
pp: n : ℕ
⊢ (last n).succAbove = castSucc

Tactic:
ext

Goal state after:
n : ℕ
x✝ : Fin n
⊢ ↑((last n).succAbove x✝) = ↑x✝.castSucc
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
· rw [iff_false_right (Fin.not_le.2 H), succAbove_of_castSucc_lt _ _ H]
    exact Fin.not_lt.2 <| Fin.le_of_lt H

Goal state after:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < p.succAbove i ↔ p ≤ i.castSucc
Module: Mathlib.Data.List.FinRange

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

Tactic:
ext

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

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

Tactic:
constructor

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

case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: n : ℕ
⊢ (finRange n).toFinset = univ

Tactic:
ext

Goal state after:
n : ℕ
a✝ : Fin n
⊢ a✝ ∈ (finRange n).toFinset ↔ a✝ ∈ univ
Module: Mathlib.Data.Fintype.Basic

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

Tactic:
ext m
  simp

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

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

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}

case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → #s = 2
Module: Mathlib.Data.Finset.Card

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

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 4 → ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) → #s = 4
Module: Mathlib.Data.Finset.Card

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

Tactic:
grind [card_eq_three]

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

Goal state before:
pp: case intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
have := And.intro (@univ α _).2 (@mem_univ_val α _)

Goal state after:
case intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) →
    ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)

Tactic:
ext

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ ↑((i.succAbove j).succAbove ((j.predAbove i).succAbove k)) = ↑(i.succAbove (j.succAbove k))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ append (append a b) c (natAdd (m + n) r) = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))

Tactic:
· rw [append_right]
    simp [← natAdd_natAdd]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) ↔
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) →
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d) →
    ∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case left
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin m
⊢ append xs ys (castAdd n i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (castAdd n i✝).rev)

pp: case right
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin n
⊢ append xs ys (natAdd m i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (natAdd m i✝).rev)

Tactic:
· simp [rev_castAdd]

Goal state after:
case right
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin n
⊢ append xs ys (natAdd m i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (natAdd m i✝).rev)
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l

Tactic:
induction h with
  | cons_mem => exact mem_cons_self
  | cons_duplicate _ hm => exact mem_cons_of_mem _ hm

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

Goal state before:
pp: n : ℕ
α : Type u_2
f : Fin n → α
x : α
⊢ Set.range (snoc f x) = insert x (Set.range f)

Tactic:
ext

Goal state after:
n : ℕ
α : Type u_2
f : Fin n → α
x x✝ : α
⊢ x✝ ∈ Set.range (snoc f x) ↔ x✝ ∈ insert x (Set.range f)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast.cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
i j : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ j.castSucc
⊢ i.castSucc = j.castSucc

Tactic:
simpa only [castSucc_inj, ← Injective.eq_iff hx, snoc_castSucc] using h

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

Goal state before:
pp: α : Type u_1
l l' : List α
⊢ l <+ l' ↔ ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
l l' : List α
⊢ l <+ l' → ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) → l <+ l'
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
e : α ↪ α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding = e

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Finite α
e : α ↪ α
x✝ : α
⊢ e.equivOfFiniteSelfEmbedding.toEmbedding x✝ = e x✝
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?) → ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)

case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)) → ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
⊢ p.removeNth (p.insertNth a f) = f

Tactic:
ext

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.removeNth (p.insertNth a f) x✝ = f x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
⊢ removeNth 0 f = tail f

Tactic:
ext

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ removeNth 0 f x✝ = tail f x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
f : Fin (n + 1) → α
⊢ (last n).removeNth f = init f

Tactic:
ext

Goal state after:
n : ℕ
α : Type u_3
f : Fin (n + 1) → α
x✝ : Fin n
⊢ (last n).removeNth f x✝ = init f x✝
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
⊢ h.toFinset = hs.toFinset ∩ ht.toFinset

Tactic:
ext

Goal state after:
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∩ ht.toFinset
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
⊢ h.toFinset = hs.toFinset ∪ ht.toFinset

Tactic:
ext

Goal state after:
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∪ ht.toFinset
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
⊢ h.toFinset = hs.toFinset \ ht.toFinset

Tactic:
ext

Goal state after:
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset \ ht.toFinset
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
⊢ h.toFinset = hs.toFinset ∆ ht.toFinset

Tactic:
ext

Goal state after:
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∆ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∆ ht.toFinset
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : s.Finite
h : sᶜ.Finite
⊢ h.toFinset = hs.toFinsetᶜ

Tactic:
ext

Goal state after:
α : Type u
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : s.Finite
h : sᶜ.Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinsetᶜ
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝ : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
⊢ h.toFinset = Finset.image f hs.toFinset

Tactic:
ext

Goal state after:
α : Type u
β : Type v
s : Set α
inst✝ : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
a✝ : β
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.image f hs.toFinset
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : (range f).Finite
⊢ h.toFinset = Finset.image f Finset.univ

Tactic:
ext

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : (range f).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ Finset.image f Finset.univ
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) ↔
    ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) →
    ∃ n m x_1, x = l.get n ∧ x = l.get m

case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
⊢ (fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f) = f

Tactic:
ext

Goal state after:
case fst
m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
⊢ ((fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f)).1 = f.1

case snd
m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
x✝ : Fin n
⊢ ((fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f)).2 x✝ = f.2 x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_3
⊢ (insertNthEquiv α 0).symm = (consEquiv α).symm

Tactic:
ext

Goal state after:
case fst
n : ℕ
α : Fin (n + 1) → Type u_3
x✝ : (i : Fin (n + 1)) → α i
⊢ ((insertNthEquiv α 0).symm x✝).1 = ((consEquiv α).symm x✝).1

case snd
n : ℕ
α : Fin (n + 1) → Type u_3
x✝¹ : (i : Fin (n + 1)) → α i
x✝ : Fin n
⊢ ((insertNthEquiv α 0).symm x✝¹).2 x✝ = ((consEquiv α).symm x✝¹).2 x✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
⊢ insertNthEquiv (fun x ↦ α) (last n) = snocEquiv fun x ↦ α

Tactic:
ext

Goal state after:
n : ℕ
α : Type u_3
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthEquiv (fun x ↦ α) (last n)) x✝¹ x✝ = (snocEquiv fun x ↦ α) x✝¹ x✝
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite

Tactic:
exact (infinite_range_of_injective hi).mono hf

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

Goal state before:
pp: n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
⊢ Nat.find ⋯ = ↑(Fin.find (fun x ↦ p ↑x) ⋯)

Tactic:
rw [val_find]

Goal state after:
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ k, k < n ∧ p k
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case rel
α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂

pp: case cons
α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂

Tactic:
exacts [(irrefl_of r a h).elim, h]

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

Goal state before:
pp: case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m + 1 < n → r m m.succ
⊢ IsChain r (range n ++ [n]) ↔ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]

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

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ (∀ (a' : List ℕ), a' ∈ map (map fun x ↦ a + x) l.ranges → (range a).Disjoint a') ∧
    Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)

Tactic:
constructor

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ (a' : List ℕ), a' ∈ map (map fun x ↦ a + x) l.ranges → (range a).Disjoint a'

case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Tactic:
· rw [rotate'_cons_succ]
      exact (hn _).trans (perm_append_singleton _ _)

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + 1) = [] ↔ hd :: tl = []

Tactic:
· simp [rotate_cons_succ, hn]

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

Goal state before:
pp: α : Type u_1
β : Type v
f g : α → Multiset β
m : Multiset α
⊢ (∀ (a : α), a ∈ m → f a = g a) → m.bind f = m.bind g

Tactic:
by simp +contextual [bind]

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

Goal state before:
pp: α : Type u
β : Type u_1
f : α → β
l : List α
n : ℕ
⊢ map f (l.rotate n) = (map f l).rotate n

Tactic:
by
  induction n generalizing l with
  | zero => simp
  | succ n hn =>
    rcases l with - | ⟨hd, tl⟩
    · simp
    · simp [hn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
⊢ ⋃₀ ↑(I.disjiUnion f hf) = ⋃ a ∈ I, ⋃₀ ↑(f a)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
f : α → Finset (Set β)
I : Finset α
hf : (↑I).PairwiseDisjoint f
x✝ : β
⊢ x✝ ∈ ⋃₀ ↑(I.disjiUnion f hf) ↔ x✝ ∈ ⋃ a ∈ I, ⋃₀ ↑(f a)
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ Function.onFun Disjoint (fun a ↦ {x ∈ s | f x = a}) x' y'

Tactic:
disjoint_left,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ {x ∈ s | f x = x'} → a ∉ {x ∈ s | f x = y'}
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
⊢ l.reverse ~r l' ↔ l ~r l'.reverse

Tactic:
constructor

Goal state after:
case mp
α : Type u
l l' : List α
⊢ l.reverse ~r l' → l ~r l'.reverse

case mpr
α : Type u
l l' : List α
⊢ l ~r l'.reverse → l.reverse ~r l'
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
⊢ s.disjiUnion (fun a ↦ {f a}) ⋯ = map { toFun := f, inj' := hf } s

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
a✝ : β
⊢ a✝ ∈ s.disjiUnion (fun a ↦ {f a}) ⋯ ↔ a✝ ∈ map { toFun := f, inj' := hf } s
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations ↔ l ~r l'

Tactic:
constructor

Goal state after:
case mp
α : Type u
l l' : List α
⊢ l ∈ l'.cyclicPermutations → l ~r l'

case mpr
α : Type u
l l' : List α
⊢ l ~r l' → l ∈ l'.cyclicPermutations
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) ↔ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y) → (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y

case mpr
α : Type u_1
l : List α
h : l.Nodup
x y : α
⊢ (∃ i h, l[i] = x) ∧ (∃ i h, l[i] = y) ∧ ¬x = y → ∃ i h j h_1, ¬i = j ∧ l[i] = x ∧ l[j] = y
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
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
β : Type u_2
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
a✝ : α × β
⊢ a✝ ∈ (s ×ˢ t).toFinset ↔ a✝ ∈ s.toFinset ×ˢ t.toFinset
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.diag = {a ∈ s ×ˢ s | a.1 = a.2}

Tactic:
ext

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : α × α
⊢ a✝ ∈ s.diag ↔ a✝ ∈ {a ∈ s ×ˢ s | a.1 = a.2}
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
s : Finset ι
inst✝ : DecidablePred fun x ↦ x ∈ s
t : (i : ↥s) → Set (π ↑i)
⊢ s.restrict ⁻¹' Set.univ.pi t = (↑s).pi fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ

Tactic:
ext

Goal state after:
ι : Type u_2
π : ι → Type u_3
s : Finset ι
inst✝ : DecidablePred fun x ↦ x ∈ s
t : (i : ↥s) → Set (π ↑i)
x✝ : (i : ι) → π i
⊢ x✝ ∈ s.restrict ⁻¹' Set.univ.pi t ↔ x✝ ∈ (↑s).pi fun i ↦ if h : i ∈ s then t ⟨i, h⟩ else Set.univ
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: ι : Type u_4
inst✝² : PartialOrder ι
inst✝¹ : DecidableLE ι
inst✝ : DecidableLT ι
s : Finset ι
⊢ {i ∈ s.offDiag | i.1 < i.2} = {i ∈ s.offDiag | i.1 ≤ i.2}

Tactic:
ext

Goal state after:
ι : Type u_4
inst✝² : PartialOrder ι
inst✝¹ : DecidableLE ι
inst✝ : DecidableLT ι
s : Finset ι
a✝ : ι × ι
⊢ a✝ ∈ {i ∈ s.offDiag | i.1 < i.2} ↔ a✝ ∈ {i ∈ s.offDiag | i.1 ≤ i.2}
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
union : u.disjUnion v disj = s.offDiag
⊢ #u = (#s).choose 2

Tactic:
have swap : #u = #v := Finset.card_equiv (Equiv.prodComm α α) (by grind)

Goal state after:
α : Type u_1
s : Finset α
inst✝ : LinearOrder α
u : Finset (α × α) := {x ∈ s ×ˢ s | x.1 < x.2}
v : Finset (α × α) := {x ∈ s ×ˢ s | x.2 < x.1}
disj : Disjoint u v
union : u.disjUnion v disj = s.offDiag
swap : #u = #v
⊢ #u = (#s).choose 2
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t ↔ ∀ (a : α), f a ∈ t a

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
⊢ (piFinset fun a ↦ image (f a) (s a)) = image (fun b a ↦ f a (b a)) (piFinset s)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
a✝ : (a : α) → δ a
⊢ (a✝ ∈ piFinset fun a ↦ image (f a) (s a)) ↔ a✝ ∈ image (fun b a ↦ f a (b a)) (piFinset s)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ (univ.pi fun a ↦ univ) = univ

Tactic:
ext

Goal state after:
α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
a✝ : (a : α) → a ∈ univ → β a
⊢ (a✝ ∈ univ.pi fun a ↦ univ) ↔ a✝ ∈ univ