mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ (↑m * δ) ^ n - (y - max x 0) < (↑m * δ) ^ n - ((↑m * δ) ^ n - q ^ n)

Tactic:
by
        refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _
        rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul,
          add_sub_cancel_left, one_mul, abs_eq_self.mpr (by positivity)]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
obtain ⟨q₂, hx₂, hy₂⟩ := exists_rat_btwn (max_lt h hy)

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case h.left
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁

Tactic:
rw [mapₓ] at perm
      exact (map_perm_map_iff hf).mp perm

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ Rel r 0 b ↔ b = 0

Tactic:
rel_iff

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ Rel r a 0 ↔ a = 0

Tactic:
rel_iff

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨ ∃ a_1 b as bs, r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔ a = 0
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
l : List α
⊢ (range fun x ↦ l[x]?) = insert none (range (some ∘ l.get))

Tactic:
refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)

Goal state after:
case refine_1
α : Type u_1
l : List α
n : ℕ
⊢ l[n]? ∈ insert none (range (some ∘ l.get))

case refine_2
α : Type u_1
l : List α
⊢ none ∈ range fun x ↦ l[x]?

case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x ↦ l[x]?
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') →
    ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁) →
    ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'

Tactic:
· intro h
        rcases h with ⟨b, bs', hab, h, rfl⟩
        rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩
        exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩

Goal state after:
case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁) →
    ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ ∀ (a b : α), a ∈ m' → b ∈ t → r a b

pp: case refine_2.refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ m'.card = t.card

Tactic:
· exact fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)

Goal state after:
case refine_2.refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ m'.card = t.card
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ (l.dropLast ++ [l.getLast hl]).Nodup

Tactic:
List.nodup_append_comm

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ ([l.getLast hl] ++ l.dropLast).Nodup
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
⊢ map f s = b ::ₘ t → ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t

Tactic:
· intro h
    have : b ∈ s.map f := by
      rw [h]
      exact mem_cons_self _ _
    obtain ⟨a, h1, rfl⟩ := mem_map.mp this
    obtain ⟨u, rfl⟩ := exists_cons_of_mem h1
    rw [map_cons, cons_inj_right] at h
    refine ⟨a, mem_cons_self _ _, rfl, ?_⟩
    rw [Multiset.erase_cons_head, h]

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

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

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : ¬a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
simp [h, mt p.mem_iff.2 h, IH p]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
t s : Multiset α
⊢ ∀ {u : Multiset α}, s ≤ 0 → s ≤ u → s ≤ 0 ∩ u

Tactic:
u

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
t s u : Multiset α
⊢ s ≤ 0 → s ≤ u → s ≤ 0 ∩ u
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s : Multiset α
⊢ ∀ {u : Multiset α}, s ≤ a ::ₘ t → s ≤ u → s ≤ (a ::ₘ t) ∩ u

Tactic:
u

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
s u : Multiset α
⊢ s ≤ a ::ₘ t → s ≤ u → s ≤ (a ::ₘ t) ∩ u
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ filter (fun x ↦ x = b) ⟦l⟧ = replicate (count b ⟦l⟧) b

Tactic:
simp only [quot_mk_to_coe, filter_coe, coe_count]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.filter (fun b_1 ↦ decide (b_1 = b)) l) = replicate (List.count b l) b
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}

Tactic:
rw [← val_inj]

Goal state after:
α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s.val = {a}.val
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ List.range a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False

Tactic:
List.mem_range

Goal state after:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ : Finset α
a b : α
s : Finset α
l : List α
head✝ : α
h : Nodup ⟦[head✝]⟧
⊢ ¬{ val := ⟦[head✝]⟧, nodup := h }.Nontrivial

Tactic:
simp [SetLike.coe]

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

Goal state before:
pp: case empty
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
hs : ∅.Nonempty
⊢ motive ∅ hs

Tactic:
exact (not_nonempty_empty hs).elim

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
⊢ s.PairwiseDisjoint fun x ↦ filter (fun x_1 ↦ f x_1 = x) t

Tactic:
rintro i - j - h u hi hj x hx
  obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx
  obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx
  contradiction

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ⊆ insert a t ↔ s ⊆ t

Tactic:
subset_insert_iff,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s.erase a ⊆ t ↔ s ⊆ t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a = ∅ ↔ s = ∅ ∨ s = {a}

Tactic:
← sdiff_singleton_eq_erase,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s \ {a} = ∅ ↔ s = ∅ ∨ s = {a}
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g ((Finset.union s t h).symm ⟨i, hi'⟩) = f ⟨i, hi⟩

Tactic:
rw! [Finset.union_symm_left h hi hi']

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ ⋯ ▸ Sum.rec f g (Sum.inl ⟨i, hi⟩) = f ⟨i, hi⟩
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s

Tactic:
by
  ext x
  simp [@and_comm _ (_ = _), @and_comm (p x) (x ∈ s)]

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

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

Tactic:
constructor <;> intro h <;>
    simp only [Finset.mem_map, Finset.mem_attach, Subtype.exists, Embedding.coeFn_mk,
      Subtype.impEmbedding] at * <;>
    grind

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

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ i.pred ⋯ = i.rev.rev.pred ⋯

Tactic:
pred_inj,

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ i = i.rev.rev
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ ∀ ⦃a₂ : Fin n⦄, i.predAbove = a₂.predAbove → i = a₂

Tactic:
j

Goal state after:
n : ℕ
i j : Fin n
⊢ i.predAbove = j.predAbove → i = j
Module: Mathlib.Data.Fin.Basic

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

Tactic:
Int.emod_eq_sub_self_emod,

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ (↑(n - ↑v + ↑u) - ↑n) % ↑n = ↑↑u - ↑↑v
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:
Int.emod_eq_sub_self_emod,

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ (↑(↑u + ↑v) - ↑n) % ↑n = ↑↑u + ↑↑v - ↑n
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: m n : ℕ
e : Fin n ≃o Fin m
i : Fin n
⊢ ↑(e i) = ↑i

Tactic:
rcases i with ⟨i, hi⟩
  dsimp only
  induction i using Nat.strong_induction_on with | _ i h
  refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)
  · have := e.symm.lt_symm_apply.1 (mk_lt_of_lt_val hj)
    specialize h _ this (e.symm _).is_lt
    simp only [Fin.eta, OrderIso.apply_symm_apply] at h
    rwa [h]
  · rwa [← h j hj (hj.trans hi), ← lt_def, e.lt_iff_lt]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ 0 < i.castSucc ↔ 0 < i

Tactic:
by simp [← val_pos_iff]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ consCases cons (Fin.cons x₀ x) = cons x₀ x

Tactic:
consCases,

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
motive : ((i : Fin n.succ) → α i) → Sort v
cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)
x₀ : α 0
x : (i : Fin n) → α i.succ
⊢ cast ⋯ (cons (Fin.cons x₀ x 0) (tail (Fin.cons x₀ x))) = cons x₀ x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i : Fin (n + 1)
⊢ ∀ ⦃a₂ : Fin (n + 1)⦄, cons x₀ x i = cons x₀ x a₂ → i = a₂

Tactic:
j

Goal state after:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin (n + 1)
⊢ cons x₀ x i = cons x₀ x j → i = j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : ¬j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

Tactic:
· simp [tail, (Fin.succ_injective n).ne h, h]

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

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
rw [append_left, Function.comp_apply]

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ s.strongInductionOn H = H s fun t x ↦ t.strongInductionOn H

Tactic:
dsimp only [strongInductionOn]
  rw [strongInduction]

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

Goal state before:
pp: case refine_2.inr
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l

Tactic:
exact h.cons_duplicate

Goal state after:
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)
⊢ i.insertNth x p i = x

Tactic:
simp [insertNth, succAboveCases]

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

Goal state before:
pp: case mpr.refine_1
α : 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 : ℕ
⊢ ∀ ⦃b : ℕ⦄,
    i < b →
      (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) i <
        (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) b

Tactic:
j

Goal state after:
case mpr.refine_1
α : 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 : ℕ
⊢ i < j →
    (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) i <
      (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_3
n : ℕ
a : α
f : Fin n → α
⊢ cons a f ∘ rev = snoc (f ∘ rev) a

Tactic:
funext i; exact cons_rev ..

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

Goal state before:
pp: case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]
    · exact Fin.le_iff_val_le_val.2 (le_of_lt h)

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
⊢ R (l.get a) (l.get b)

Tactic:
by
  obtain rfl | hlt := Fin.eq_or_lt_of_le hab; exacts [refl _, (pairwise_iff_get.1 h) _ _ hlt]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
x : α
l : List α
y : α
h : IsChain R (x :: y :: l.tail)
hy : y ∈ l.head?
⊢ R x y

Tactic:
exact h.rel

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ IsChain R (a :: b :: l₁ ++ l₂) ↔
    IsChain R (a :: b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
rw [cons_append, cons_append, isChain_cons_cons, isChain_cons_cons,
      ← cons_append, isChain_append, and_assoc]

Goal state after:
α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ (R a b ∧ IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    R a b ∧
      IsChain R (b :: l₁) ∧ IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (map f ↑(m.toList.erase a)).prod = (map f ↑m.toList).prod

Tactic:
map_coe,

Goal state after:
ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (↑(List.map f (m.toList.erase a))).prod = (map f ↑m.toList).prod
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (↑(List.map f (m.toList.erase a))).prod = (map f ↑m.toList).prod

Tactic:
map_coe,

Goal state after:
ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (↑(List.map f (m.toList.erase a))).prod = (↑(List.map f m.toList)).prod
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ (0 • m).prod = m.prod ^ 0

Tactic:
zero_nsmul,

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
⊢ prod 0 = m.prod ^ 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % (hd :: tl).length ≤ (hd :: tl).length

Tactic:
refine (Nat.mod_lt _ ?_).le

Goal state after:
case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ 0 < (hd :: tl).length
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

Tactic:
rw [Pi.cons_ne _ h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : a = a✝
⊢ r (⋯ ▸ b₁) (⋯ ▸ b₂)

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : ¬a = a✝
⊢ r (f₁ a ⋯) (f₂ a ⋯)

Tactic:
· cases H
    exact hb

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
H : ¬a = a✝
⊢ r (f₁ a ⋯) (f₂ a ⋯)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
rw [choose_succ_succ, Nat.add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
        Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ piFinset s = ∅ ↔ ∃ i, s i = ∅

Tactic:
by simp [piFinset]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ (piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty

Tactic:
by simp [piFinset]

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

Goal state before:
pp: case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (univ.pi fun i ↦ ↑(t i)).Finite

Tactic:
← Fintype.coe_piFinset

Goal state after:
case intro
ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
val✝ : Fintype ι
t : (i : ι) → Finset (κ i)
⊢ (↑(Fintype.piFinset t)).Finite
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

Tactic:
rw [Pi.cons_ne _ h]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ f' a' ⋯ ∈ t a'
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ (Pi.cons m a (f a ⋯) fun a_1 ha ↦ f a_1 ⋯) = f

Tactic:
Pi.cons_eta

Goal state after:
case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
hf : ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
⊢ f = f