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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
⊢ ∀ (t : Multiset α) (eq : ndinsert a s = t), t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
by
    intro t ht
    by_cases h : a ∈ s
    · rw [ndinsert_of_mem h] at ht
      subst ht
      rw [eq, map_id, ndinsert_of_mem (mem_attach _ _)]
    · rw [ndinsert_of_notMem h] at ht
      subst ht
      simp [attach_cons, h]

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
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : f a × ((i : α) → i ∈ s → f i)
⊢ consPiProd f has (prodPiCons f has x✝) = x✝

Tactic:
by
    -- I'm surprised `grind` needs this `ext` step: it is just `Prod.ext` and `funext`.
    ext _ hi <;> grind [prodPiCons, consPiProd]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise (r on fun a_1 ↦ f ↑a_1) ↔ _root_.Pairwise (r on fun a ↦ f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Tactic:
simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert]
  grind

Goal state after:
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
  simp

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

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

Tactic:
simp only [not_or, mem_insert, mem_compl, mem_erase]

Goal state after:
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
  simp

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 β
⊢ {y | ∃ x, f x = y} = image f univ

Tactic:
ext
  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)
⊢ (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

Tactic:
ext
  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)
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
ext
  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)
⊢ (s \ t).toFinset = s.toFinset \ t.toFinset

Tactic:
ext
  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ᶜ
⊢ sᶜ.toFinset = s.toFinsetᶜ

Tactic:
ext
  simp

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

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

Tactic:
ext
  simp

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

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

Tactic:
ext
  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}
⊢ {x | p x}.toFinset = filter p Finset.univ

Tactic:
ext
  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)
⊢ (range f).toFinset = Finset.image f Finset.univ

Tactic:
ext
  simp

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

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

Tactic:
ext
  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
⊢ (insert a s).toFinset = insert a s.toFinset

Tactic:
ext
  simp

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

Goal state before:
pp: a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
⊢ c = 0 ∨ 0 < c

Tactic:
lia

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

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

Tactic:
ext
  simp

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

Goal state before:
pp: n m : ℕ
p : Fin (n + 1)
hmn : n ≤ m
⊢ n + (m - n) = m

Tactic:
lia

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
y : Fin m
x✝ : y ∈ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding)
x : Fin n
hx : ((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) x = y
⊢ m ≤ ↑x + (m - n) + n

Tactic:
lia

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

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) = ↑↑u + ↑↑v

Tactic:
lia

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

Goal state before:
pp: case isTrue.H1
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v)

Tactic:
lia

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

Goal state before:
pp: case isTrue.H2
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) < ↑n

Tactic:
lia

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

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n = ↑↑u + ↑↑v - ↑n

Tactic:
lia

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

Goal state before:
pp: case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v) - ↑n

Tactic:
lia

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

Goal state before:
pp: case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n < ↑n

Tactic:
lia

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

Goal state before:
pp: n : ℕ
⊢ 1 < n ↔ 2 ≤ n

Tactic:
lia

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : 2 < n
⊢ n ≠ 0

Tactic:
lia

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

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ 1 < n

Tactic:
lia

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

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ 2 < n

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ 2 ≠ i ∧ 2 ≠ j

Tactic:
lia

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

Goal state before:
pp: n✝ m n : ℕ
i j : Fin n
hij : i < j
⊢ n - ↑i ≠ 0

Tactic:
lia

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

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i < j
⊢ ¬0 = ↑j - ↑i

Tactic:
lia

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : ↑i < ↑a
hu : ↑b < ↑i + 1
⊢ ↑b < ↑a

Tactic:
lia

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑i < ↑p ∨ ↑p < ↑i + 1

Tactic:
lia

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

Goal state before:
pp: n : ℕ
⊢ n ≤ n + 1

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
this : image f s = t
⊢ Set.SurjOn f ↑s ↑t

Tactic:
rw [Finset.surjOn_iff_subset_image, this]

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

Goal state before:
pp: i : Fin 2
hi : i ≠ 0
⊢ i = 1

Tactic:
lia

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

Goal state before:
pp: n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
⊢ k ≤ ↑b

Tactic:
lia

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

Goal state before:
pp: case zero
a b : Fin (0 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
lia

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

Goal state before:
pp: n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
⊢ k < ↑b

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝¹ : image f s = t
this✝ : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ #(image f s) = #s

Tactic:
lia

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

Goal state before:
pp: n : ℕ
i : Fin n
h : ↑i + 1 < n
⊢ ↑i + 1 < n

Tactic:
lia

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
⊢ j < n

Tactic:
lia

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
α : Sort u_1
u : Fin m → α
v : Fin n → α
i : Fin m
⊢ m ≤ m + n

Tactic:
lia

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
⊢ ∃ a, f a = x

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
⊢ ∃ a, f a = x
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ↑j < ↑i
h✝² : ↑k < ↑i - 1
h✝¹ : ↑k < ↑j
h✝ : ↑k < ↑i
⊢ ↑k = ↑k

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ↑j < ↑i
h✝² : ↑k < ↑i - 1
h✝¹ : ↑k < ↑j
h✝ : ¬↑k < ↑i
⊢ ↑k = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ↑j < ↑i
h✝² : ↑k < ↑i - 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ↑j < ↑i
h✝² : ↑k < ↑i - 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1 + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ↑k + 1 < ↑j
h✝¹ : ↑k < ↑j
h✝ : ↑k < ↑i
⊢ ↑k + 1 = ↑k

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ↑k + 1 < ↑j
h✝¹ : ↑k < ↑j
h✝ : ¬↑k < ↑i
⊢ ↑k + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ↑k + 1 < ↑j
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ↑k + 1 < ↑j
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1 + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ¬↑k + 1 < ↑j
h✝¹ : ↑k < ↑j
h✝ : ↑k < ↑i
⊢ ↑k + 1 + 1 = ↑k

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ¬↑k + 1 < ↑j
h✝¹ : ↑k < ↑j
h✝ : ¬↑k < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ¬↑k + 1 < ↑j
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ↑j < ↑i
h✝³ : ¬↑k < ↑i - 1
h✝² : ¬↑k + 1 < ↑j
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1 + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ¬↑j < ↑i
h✝² : ↑k < ↑i
h✝¹ : ↑k < ↑j + 1
h✝ : ↑k < ↑j
⊢ ↑k = ↑k

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ↑k < ↑i
h✝² : ↑k < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ↑k < ↑i
h✝² : ↑k < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k = ↑k + 1 + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ¬↑j < ↑i
h✝² : ↑k < ↑i
h✝¹ : ¬↑k < ↑j + 1
h✝ : ↑k < ↑j
⊢ ↑k + 1 = ↑k

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ↑k < ↑i
h✝² : ¬↑k < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ↑k < ↑i
h✝² : ¬↑k < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1 + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ¬↑j < ↑i
h✝² : ¬↑k < ↑i
h✝¹ : ↑k + 1 < ↑j + 1
h✝ : ↑k < ↑j
⊢ ↑k + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ¬↑k < ↑i
h✝² : ↑k + 1 < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ¬↑k < ↑i
h✝² : ↑k + 1 < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 = ↑k + 1 + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝³ : ¬↑j < ↑i
h✝² : ¬↑k < ↑i
h✝¹ : ¬↑k + 1 < ↑j + 1
h✝ : ↑k < ↑j
⊢ ↑k + 1 + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ¬↑k < ↑i
h✝² : ¬↑k + 1 < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ↑k + 1 < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1

Tactic:
lia

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

Goal state before:
pp: α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ append x₀ x = cons (x₀ 0) x ∘ Fin.cast ⋯

Tactic:
by
  ext i
  refine Fin.addCases ?_ ?_ i <;> clear i
  · intro i
    rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]
    exact Fin.cons_zero _ _
  · intro i
    rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
    exact Fin.cons_succ _ _ _

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

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h✝⁴ : ¬↑j < ↑i
h✝³ : ¬↑k < ↑i
h✝² : ¬↑k + 1 < ↑j + 1
h✝¹ : ¬↑k < ↑j
h✝ : ¬↑k + 1 < ↑i
⊢ ↑k + 1 + 1 = ↑k + 1 + 1

Tactic:
lia

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

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

Tactic:
induction i using Fin.addCases

Goal state after:
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)

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.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
⊢ card { x // ¬p x } = card { x // ¬q x }

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
α : Type u_1
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
val✝ : Fintype α
⊢ card { x // ¬p x } = card { x // ¬q x }
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
⊢ WellFounded r

Tactic:
cases nonempty_fintype α

Goal state after:
case intro
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
⊢ WellFounded r
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
s✝ t✝ u : Finset α
f : α → β
n✝ : ℕ
p : Finset α → Sort u_4
n : ℕ
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
x✝ : Finset α
s : Finset α := x✝
t : Finset α
ht : #t ≤ n
h : s ⊂ t
this : #s < #t
⊢ n - #t < n - #s

Tactic:
lia

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

Goal state before:
pp: case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : i < l.length
hj : ¬j < l.length
⊢ ↑(f ⟨i, hi⟩) < j + l'.length

Tactic:
lia

Goal state after:
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
  simp

Goal state after:
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
  simp

Goal state after:
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
  simp

Goal state after:
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
  simp

Goal state after:
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
  simp

Goal state after:
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
  simp

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Multiset α
⊢ ⋯.toFinset = s.toFinset

Tactic:
by
  ext x
  simp

Goal state after:
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 <;> simp

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

Goal state before:
pp: case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : natAdd m i < natAdd m (Fin.find (fun j ↦ p (natAdd m j)) ⋯)
⊢ ¬p (natAdd m i)

Tactic:
Fin.natAdd_lt_natAdd_iff

Goal state after:
case right
m n : ℕ
p : Fin (m + n) → Prop
inst✝ : DecidablePred p
hᵢ : ∃ i, p i
hm : m ≤ ↑(Fin.find p hᵢ)
hⱼ : ∃ j, p (natAdd m j)
i : Fin n
hi : i < Fin.find (fun j ↦ p (natAdd m j)) ⋯
⊢ ¬p (natAdd m i)
Module: Mathlib.Data.List.Range

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u < a
⊢ (∃ a_1, a_1 ∈ s' ∧ a + a_1 = u) → False

Tactic:
lia

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

Goal state before:
pp: α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ i < l.length

Tactic:
lia

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

Goal state before:
pp: case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
⊢ m - (l.length - n % l.length) = n % l.length + m - l.length

Tactic:
lia

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
have _ : Std.Symm fun a b : List β ↦ List.Disjoint a b := { symm a b h := h.symm }

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
x✝ : Std.Symm fun a b ↦ a.Disjoint b
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
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
  simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * ((m * (p + 1))! * (p + 1)!) =
    (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)!

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1))! = (m * (p + 1) + p + 1)!

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p + 1) * (m * (p + 1) + p)! = (m * (p + 1) + p)! * ((p + 1) * (m + 1))

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * p ! * ((p + 1) * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))

Tactic:
lia

Goal state after: