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

Goal state before:
pp: n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) ^ (0 + 2) < n.descFactorial (0 + 2)

Tactic:
by
    rw [descFactorial_succ, Nat.pow_succ, Nat.pow_one, descFactorial_one]
    exact Nat.mul_lt_mul_of_pos_left (by lia) (Nat.sub_pos_of_lt h)

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

Goal state before:
pp: p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ (⟨n, h⟩ + 1).recOn one succ = succ ⟨n, h⟩ (recOn ⟨n, h⟩ one succ)

Tactic:
cases n

Goal state after:
case zero
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
h : 0 < 0
⊢ (⟨0, h⟩ + 1).recOn one succ = succ ⟨0, h⟩ (recOn ⟨0, h⟩ one succ)

case succ
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n✝ : ℕ
h : 0 < n✝ + 1
⊢ (⟨n✝ + 1, h⟩ + 1).recOn one succ = succ ⟨n✝ + 1, h⟩ (recOn ⟨n✝ + 1, h⟩ one succ)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ (0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z) → fract a = b

Tactic:
by
    rintro ⟨h₀, h₁, z, hz⟩
    rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz]
    refine congrArg Int.cast ?_
    rw [floor_eq_iff, ← hz]
    constructor <;> simpa [sub_eq_add_neg, add_assoc]

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddCommGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℤ
x : G
⊢ f (n • a + x) = f x + n • b

Tactic:
rw [add_comm, map_add_zsmul]

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R (f (l + n • a)) (f (y - n • a + n • a))

Tactic:
map_add_zsmul,

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R (f l + n • b) (f (y - n • a + n • a))
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
H : ∀ (x : K), ∃ n, x < ↑n
x y : K
y0 : 0 < y
n : ℕ
h : x / y < ↑n
⊢ x < n • y

Tactic:
by rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h

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

Goal state before:
pp: case mk.nil
α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
a✝ : Multiset α
⊢ Quot.mk ⇑(isSetoid α) [] = 0

pp: case mk.cons
α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
a✝ : Multiset α
a : α
l : List α
⊢ Quot.mk (⇑(isSetoid α)) (a :: l) = 0

Tactic:
exacts [rfl, isEmptyElim a]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk (⇑(isSetoid α)) l = 0

Tactic:
rw [eq_nil_iff_forall_not_mem.mpr H]

Goal state after:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk ⇑(isSetoid α) [] = 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
⊢ (∀ (a : α), ¬[a, a] <+ l) → l.Nodup

Tactic:
induction l <;> intro h; · exact nodup_nil
      case cons a l IH =>
        exact (IH fun a s => h a <| sublist_cons_of_sublist _ s).cons
          fun al => h a <| (singleton_sublist.2 al).cons_cons _

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
card_erase_of_mem h,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ s.card.pred = if a ∈ s then s.card.pred else s.card
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ Rel r 0 0

Tactic:
rel_zero_left

Goal state after:
case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 : Rel r 0 u
⊢ 0 = 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
β : Type v
l₁ : List α
l₂ : List β
d₁ : l₁.Nodup
d₂ : l₂.Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : α × β
h₁ : x ∈ (fun a ↦ map (Prod.mk a) l₂) a₁
h₂ : x ∈ (fun a ↦ map (Prod.mk a) l₂) a₂
⊢ False

Tactic:
by
        rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
        rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
        exact n rfl

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

Goal state before:
pp: α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : x ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₁
h₂ : x ∈ (fun a ↦ map (Sigma.mk a) (l₂ a)) a₂
⊢ False

Tactic:
by
        rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
        rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
        exact n rfl

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

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Tactic:
cases l₂ with grind [List.bagInter]

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

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Tactic:
cases l₂ with grind [List.bagInter]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
⊢ ∀ (a b : List α) (p_1 : a ≈ b),
    Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ =
      fun ex_unique ↦ List.chooseX p b ⋯

Tactic:
intro a b _

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
⊢ Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ =
    fun ex_unique ↦ List.chooseX p b ⋯
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ a ::ₘ (s.erase a - t + t ∩ s.erase a) = s

Tactic:
IH,

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : a ∈ s
⊢ a ::ₘ s.erase a = s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ (countP p (map f t) + if p (f a) then 1 else 0) = (filter (fun a ↦ p (f a)) (a ::ₘ t)).card

Tactic:
IH,

Goal state after:
case refine_2
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
a : α
t : Multiset α
IH : countP p (map f t) = (filter (fun a ↦ p (f a)) t).card
⊢ ((filter (fun a ↦ p (f a)) t).card + if p (f a) then 1 else 0) = (filter (fun a ↦ p (f a)) (a ::ₘ t)).card
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
h : ¬x = y
⊢ min (if x = y then n else 0) (count y s) = if x = y then min n (count x s) else 0

Tactic:
simp only [h, if_false, Nat.zero_min]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a (s + t) = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0

Tactic:
count_add,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a s + count a t = count a (s ∪ t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = count a 0

Tactic:
count_zero,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = 0
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ ndinsert a s ≤ t

Tactic:
rw [ndinsert_of_notMem h, ← cons_erase m, cons_le_cons_iff, ← le_cons_of_notMem h,
          cons_erase m]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : ¬a ∈ s
⊢ s ≤ t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse l.inits).reverse

Tactic:
by
  rw [inits_eq_tails l]
  simp [← map_reverse]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse l.inits = l.reverse.tails.reverse

Tactic:
by
  rw [inits_eq_tails l]
  simp [← map_reverse]

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.tails.length
⊢ l.tails[n] = drop n l

Tactic:
induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

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

Goal state before:
pp: α : Type u_1
l : List α
n : ℕ
h : n < l.inits.length
⊢ l.inits[n] = take n l

Tactic:
induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

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

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

Tactic:
by
  dsimp [predAbove]
  split_ifs with ha hb hb
  · rfl
  · exact pred_le _
  · have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
    exact absurd H this.not_ge
  · rfl

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

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

Tactic:
cases n

Goal state after:
case zero
inst✝ : NeZero 0
⊢ succ 0 = 1

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 0 = 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ succ 1 = 2

Tactic:
cases n

Goal state after:
case zero
inst✝ : NeZero 0
⊢ succ 1 = 2

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
← Nat.lt_succ_iff

Goal state after:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a ≤ ↑b ↔ a ≤ b
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ ↑a < ↑b ↔ a < b

Tactic:
← Nat.lt_succ_iff

Goal state after:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a < ↑b ↔ a < b
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i + 1)) % n = (m * n - (↑i / n * n + ↑i % n + 1)) % n

Tactic:
rw [Nat.div_add_mod']

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
cases n

Goal state after:
case zero
p i : Fin 0
h : p < i
⊢ i.castSucc ≠ 0

case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : p < i
⊢ i.castSucc ≠ 0
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
val_zero,

Goal state after:
n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ 1 % (n + 1) - 1 = 0
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
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
let f' : s → β := fun a ↦ f a a.2

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha
Module: Mathlib.Data.Fin.Basic

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

Tactic:
cases n

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

case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ a + 1 ≤ b

Tactic:
cases n

Goal state after:
case zero
a b : Fin (0 + 1)
h : a < b
⊢ a + 1 ≤ b

case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ a + 1 ≤ b
Module: Mathlib.Data.Fin.Basic

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

Tactic:
cases n

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

case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ castPred 1 ⋯ = 1

Tactic:
cases n

Goal state after:
case zero
inst✝ : NeZero 0
⊢ castPred 1 ⋯ = 1

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ castPred 1 ⋯ = 1
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₂
⊢ a₁ = a₂

Tactic:
let f' : s → β := fun a ↦ f a a.2

Goal state after:
α : 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 ⋯
⊢ a₁ = a₂
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ (f 0 :: ofFn fun i ↦ f i.succ) = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
IH,

Goal state after:
case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n).succ) =
    (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last (n + 1)))
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
succAbove_lt_iff_castSucc_lt,

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ↔ i.succ ≤ p
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
cases n

Goal state after:
case zero
inst✝ : NeZero 0
i : Fin 0
⊢ i.predAbove 0 = 0

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
i : Fin (n✝ + 1)
⊢ i.predAbove 0 = 0
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case zero.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ cons x₀ x 0 = cons x₀ x 0 → 0 = 0

Tactic:
aesop (add simp [hx.eq_iff])

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

Goal state before:
pp: case zero.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x 0 = cons x₀ x i✝.succ → 0 = i✝.succ

Tactic:
aesop (add simp [hx.eq_iff])

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

Goal state before:
pp: case succ.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x 0 → i✝.succ = 0

Tactic:
aesop (add simp [hx.eq_iff])

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

Goal state before:
pp: case succ.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝¹ i✝ : Fin n
⊢ cons x₀ x i✝¹.succ = cons x₀ x i✝.succ → i✝¹.succ = i✝.succ

Tactic:
aesop (add simp [hx.eq_iff])

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + Fintype.card α - #s = Fintype.card α

Tactic:
Nat.add_sub_cancel_left

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ Fintype.card α = Fintype.card α
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ #{x | p x}ᶜ.toFinset = card α - card { x // p x }

pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x

Tactic:
Set.toFinset_compl,

Goal state after:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ #{x | p x}.toFinsetᶜ = card α - card { x // p x }

case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ P α

Tactic:
apply hstep

Goal state after:
case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ ∀ (β : Type u_4) [inst : Fintype β], card β < card α → P β
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
z : α (last n)
motive : ((i : Fin n.succ) → α i) → Sort u_2
snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (last n)) → motive (Fin.snoc xs x)
x : (i : Fin n.succ) → α i
⊢ motive (Fin.snoc (init x) (x (last n))) = motive x

Tactic:
rw [Fin.snoc_init_self]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : card α ≤ 1
⊢ False

Tactic:
rw [← ha] at h

Goal state after:
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
by
  simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff_castSucc_lt]
  split_ifs with hlt
  · generalize_proofs H₁ H₂; revert H₂
    generalize hk : castPred ((succAbove i) j) H₁ = k
    rw [castPred_succAbove _ _ hlt] at hk; cases hk
    intro; rfl
  · generalize_proofs H₀ H₁ H₂; revert H₂
    generalize hk : pred (succAbove i j) H₁ = k
    rw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk; cases hk
    intro; rfl

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedGT ↔ Pairwise (fun x1 x2 ↦ x1 > x2) l

Tactic:
by
  simp only [sortedGT_iff_strictAnti_get, StrictAnti, Fin.forall_iff]
  grind [pairwise_iff_getElem]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
rw [← insert_erase h]
    simp [← ha.assoc, hi.idempotent]

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ r c (f a) ∧ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
IH,

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)
⊢ (r c (f a) ∧ r c b ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ r c (f a) ∨ r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)

Tactic:
IH,

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : a ∉ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
⊢ (r c (f a) ∨ r c b ∨ ∃ x ∈ s, r c (f x)) ↔ r c b ∨ ∃ x ∈ insert a s, r c (f x)
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b

Tactic:
by
  have : Std.Symm fun x y ↦ x ≠ y → R x y := { symm a b h hne := symm <| h hne.symm }
  apply Pairwise.forall_of_forall
  · exact fun _ _ ↦ absurd rfl
  · exact hl.imp @fun a b h _ ↦ by exact h

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ IsChain r (a :: range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
range_succ_eq_map,

Goal state after:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ IsChain r (a :: 0 :: map succ (range n)) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ