mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r : ℤ
x : M
t t' l' : NF M
h : t.eval = t'.eval
h' : ((r, x) ::ᵣ t').eval = l'.eval
⊢ ((r, x) ::ᵣ t).eval = l'.eval

Tactic:
by
  rw [← h', eval_cons, eval_cons, h]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : Group G
n : ℕ
f : ℕ → G
⊢ (map (fun k ↦ f k / f (k + 1)) (range n)).prod = f 0 / f n

Tactic:
induction n with
  | zero => exact (div_self' (f 0)).symm
  | succ n h => simp [range_succ, prod_append, map_append, h]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
n a : ℕ
l : List ℕ
ih : l.prod % n = (map (fun x ↦ x % n) l).prod % n
⊢ (a :: l).prod % n = (map (fun x ↦ x % n) (a :: l)).prod % n

Tactic:
simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)

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

Goal state before:
pp: α : Type u
l : List α
p q : α → Bool
h : ∀ (a : α), p a = true → q a = true
⊢ filter p l <+ filter q l

Tactic:
by
  induction l with grind

Goal state after:
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
⊢ ↑q.den * q = ↑q.num

Tactic:
by rw [mul_comm, mul_den_eq_num]

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ ↑q.den * q = ↑q.num

Tactic:
by rw [mul_comm, mul_den_eq_num]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0

Tactic:
· push_cast
    exact mul_ne_zero hp hq

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: case b0
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.num ≠ 0
⊢ ↑(↑p.den * q.num) ≠ 0

Tactic:
· push_cast
    exact mul_ne_zero hp hq

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ i, ⨅ (hi : p i), f i hi) = ⨅ i, ⨅ (hi : p i), l (f i hi)

Tactic:
by
  rw [iInf_subtype', iInf_subtype']
  exact gi.l_iInf_of_u_l_eq_self _ fun _ => hf _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : SupSet α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ a, f ↑a

Tactic:
rw [iSup, image_eq_range]

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
t : (i : α) → Set (π i)
⊢ univ.pi t = ⋂ i, eval i ⁻¹' t i

Tactic:
simp only [pi_def, iInter_true, mem_univ]

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

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
⊢ ∀ (J : Set ι), x ∈ ⋃ j ∈ J, Es j ↔ i ∈ J

Tactic:
refine fun J ↦ ⟨?_, fun i_in_J ↦ by simpa only [mem_iUnion, exists_prop] using ⟨i, i_in_J, hix⟩⟩

Goal state after:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
⊢ x ∈ ⋃ j ∈ J, Es j → i ∈ J
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b

Tactic:
by_cases hab : a = b

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : a = b
⊢ min a b = if a ≤ b then a else b

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ min a b = if a ≤ b then a else b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
⊢ max a b = if a ≤ b then b else a

Tactic:
by_cases hab : a = b

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : a = b
⊢ max a b = if a ≤ b then b else a

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
h : ConditionallyCompleteLinearOrder α
a b : α
hab : ¬a = b
⊢ max a b = if a ≤ b then b else a
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
a : α
x✝ : a ∈ s
⊢ a ∆ sSup t ≤ ⨆ b ∈ t, a ∆ b

Tactic:
by simpa [sSup_image] using symmDiff_sSup_le ht

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective fun b ↦ Ι b a

Tactic:
rintro b c h
  rw [Set.ext_iff] at h
  obtain ha | ha := le_or_gt b a
  · have hb := (h b).not
    simp only [ha, left_mem_uIoc, true_iff, notMem_uIoc, ← not_le,
      and_true, not_true, false_and, not_false_iff, or_false] at hb
    refine hb.eq_of_not_lt fun hc => ?_
    simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c
  · refine
      eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
        ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)
    simpa [ha, ha.not_ge, mem_uIoc] using h b

Goal state after:
Module: Mathlib.Tactic.NormNum.Eq

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
n₁ n₂ : ℕ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁

Tactic:
by
  rw [mul_invOf_eq_iff_eq_mul_right, ← Nat.commute_cast, mul_assoc,
    ← mul_left_eq_iff_eq_invOf_mul, Nat.commute_cast]

Goal state after:
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a b : ℤ
r : ℕ
h : IsNat (a % -b) r
⊢ a % -b = ↑r

Tactic:
h.out

Goal state after:
a b : ℤ
r : ℕ
h : IsNat (a % -b) r
⊢ ↑r = ↑r
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)

Tactic:
rw [Nat.pow_succ, ascFactorial, Nat.mul_comm]

Goal state after:
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n ≤ k ∨ n < k ↔ n ≤ k

Tactic:
Nat.lt_iff_le_and_ne,

Goal state after:
n k : ℕ
⊢ n ≤ k ∨ n ≤ k ∧ n ≠ k ↔ n ≤ k
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ ↑|q.num| / ↑q.den = ↑q.num / ↑q.den

Tactic:
rw [abs_of_nonneg (by simpa)]

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

Goal state before:
pp: k m : ℕ+
⊢ k ∣ m ↔ ↑k ∣ ↑m

Tactic:
constructor <;> intro h
  · rcases h with ⟨_, rfl⟩
    apply dvd_mul_right
  · rcases h with ⟨a, h⟩
    obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (n := a) <| by
      rintro rfl
      simp only [mul_zero, ne_zero] at h
    use ⟨n.succ, n.succ_pos⟩
    rw [← coe_inj, h, mul_coe, mk_coe]

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

Goal state before:
pp: case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0

Tactic:
exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim

Goal state after:
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
⊢ ↑(⌊a + b⌋ - 1) - ↑⌊b⌋ ≤ a

Tactic:
sub_le_comm,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑(⌊a + b⌋ - 1) - a ≤ ↑⌊b⌋
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
x : R
hx : fract x ≠ 0
⊢ fract (-x) = 1 - fract x

Tactic:
rw [fract_eq_iff]
  constructor
  · rw [le_sub_iff_add_le, zero_add]
    exact (fract_lt_one x).le
  refine ⟨sub_lt_self _ (lt_of_le_of_ne' (fract_nonneg x) hx), -⌊x⌋ - 1, ?_⟩
  simp only [sub_sub_eq_add_sub, cast_sub, cast_neg, cast_one, sub_left_inj]
  conv in -x => rw [← floor_add_fract x]
  simp [-floor_add_fract]

Goal state after:
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
⊢ ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

Tactic:
rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]
  refine (ceil_lt_add_one _).le.trans ?_
  rw [le_sub_iff_add_le', ← add_assoc, add_le_add_iff_right]
  exact le_ceil _

Goal state after:
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G✝ : Type u_1
M : Type u_2
A✝ : Type u_3
B✝ : Type u_4
α : Type u_5
β : Type u_6
G : Type u_7
A : Type u_8
B : Type u_9
inst✝¹ : DivisionMonoid G
inst✝ : MulAction G A
f : A → B
⊢ 1 • f = f

Tactic:
change (fun x => f ((1 : G)⁻¹ • x)) = f
    simp only [inv_one, one_smul]

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

Goal state before:
pp: α : Type u_1
a : α
⊢ a ∈ {a}

Tactic:
← cons_zero

Goal state after:
α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a} = {b} ↔ a = b

Tactic:
← cons_zero

Goal state after:
α : Type u_1
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mpr
α : Type u_1
s t : Multiset α
⊢ s = t → Rel (fun x1 x2 ↦ x1 = x2) s t

Tactic:
· rintro rfl
    exact rel_eq_refl

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

Goal state before:
pp: case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
exact (h j i hj hi hji hg.symm).elim

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

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

Tactic:
by_cases h : a ∈ s

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

case neg
α : 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
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 u

Tactic:
rel_zero_left.mp r2,

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
⊢ Rel r 0 0
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l ∩ [] = []

Tactic:
by
  induction l with grind

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

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

Tactic:
by_cases h : a ∈ s

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
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s

case neg
α : Type u_1
inst✝ : DecidableEq α
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), s - t + t ∩ s = s
s : Multiset α
h : ¬a ∈ s
⊢ s - a ::ₘ t + (a ::ₘ t) ∩ s = s
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
f₁ f₂ : Finset α
h : f₁.toList.Perm f₂.toList
x : α
⊢ x ∈ f₁ ↔ x ∈ f₂

Tactic:
by simp [← Finset.mem_toList, h.mem_iff]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+: l₂
⊢ l₁.flatten <+: l₂.flatten

Tactic:
rcases h with ⟨l, rfl⟩

Goal state after:
α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <+: (l₁ ++ l).flatten
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+ l₂
⊢ l₁.flatten <:+ l₂.flatten

Tactic:
rcases h with ⟨l, rfl⟩

Goal state after:
α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <:+ (l ++ l₁).flatten
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mp
α : Type u_1
x y : α
⊢ [x] <:+: [y] → x = y

Tactic:
rintro ⟨_ | _, bs, h⟩

Goal state after:
case mp.nil
α : Type u_1
x y : α
bs : List α
h : [] ++ [x] ++ bs = [y]
⊢ x = y

case mp.cons
α : Type u_1
x y head✝ : α
tail✝ bs : List α
h : head✝ :: tail✝ ++ [x] ++ bs = [y]
⊢ x = y
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 α
ht : ndinsert a s = t
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
by_cases h : a ∈ s

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

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
by
  split_ifs <;> simp [*]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
by
  split_ifs <;> simp [*]

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

Goal state before:
pp: α : Type u_1
s t u : Finset α
h : Disjoint t u
⊢ Disjoint s (t.disjUnion u h) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
simp only [disjoint_right, mem_disjUnion, or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁

Tactic:
classical
    refine ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), ?_, ?_, ?_⟩
    · grind
    · grind
    · intro x
      simp only [coe_filter, Set.mem_ofPred_eq, and_imp]
      intro hx hx₂
      exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩

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

Goal state before:
pp: α : Type u
⊢ ofFn [].get = []

Tactic:
rw [ofFn_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
hf : Set.InjOn f ↑s
hf' : Set.MapsTo f ↑s ↑t
h : #t = #s + 1
this : #(t \ image f s) = 1
⊢ ∃! x, x ∈ t ∧ x ∉ image f s

Tactic:
simpa [card_eq_one_iff_existsUnique] using this

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

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]

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

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
i : Fin (n + 1)
hi : P i
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
cases i using lastCases with
    | last => exact .inl hi
    | cast _ => exact .inr ⟨_, hi⟩

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

Goal state before:
pp: case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ i.succ.insertNth x (cons a p) i.succ = cons a (i.insertNth x p) i.succ

Tactic:
| x =>

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : 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
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
by_cases h : a ∈ s

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

case neg
α : 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)
Module: Mathlib.Data.List.Flatten

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a <+ g a
⊢ flatMap f l <+ flatMap g l

Tactic:
by
  induction l with grind

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

Goal state before:
pp: case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map length (a :: l).ranges = a :: l

Tactic:
simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
    conv_rhs => rw [← hl]
    apply map_congr_left
    intro s _
    simp only [Function.comp_apply, length_map]

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n l ++ [a] ++ take n (l ++ [a]) = drop n l ++ a :: take n l

Tactic:
take_append_of_le_length hnl

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l
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 : ℕ
hi : i < l.length
⊢ f^[i] l[0] = l[i]

Tactic:
induction i with

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
⊢ count a (n • s).dedup = count a s.dedup

Tactic:
by_cases h : a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
h : a ∈ s
⊢ count a (n • s).dedup = count a s.dedup

case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
hn : n ≠ 0
a : α
h : ¬a ∈ s
⊢ count a (n • s).dedup = count a s.dedup
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
    rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]
    · congr 1
      rw [length_drop] at hm
      have hm' := Nat.sub_le_iff_le_add'.1 hm
      have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml
      conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
      lia
    · rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ l.rotate n = [x] ↔ l = [x]

Tactic:
rw [rotate_eq_iff, rotate_singleton]

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

Goal state before:
pp: α : Type u_1
l : List α
L : List (List α)
⊢ (↑(List.map ofList (l :: L))).join = ↑(l :: L).flatten

Tactic:
exact congr_arg (fun s : Multiset α => ↑l + s) (coe_join L)

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
S : Multiset (Multiset α)
⊢ map f S.join = (map (map f) S).join

Tactic:
induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
S : Multiset (Multiset α)
⊢ S.join.prod = (map prod S).prod

Tactic:
induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u_1
S : Multiset (Multiset α)
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p S.join = (map (filter p) S).join

Tactic:
induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u_1
β : Type v
S : Multiset (Multiset α)
f : α → Option β
⊢ filterMap f S.join = (map (filterMap f) S).join

Tactic:
induction S using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
⊢ Infinite ((i : ι) → π i)

Tactic:
choose m n hm using fun i => exists_pair_ne (π i)
  refine Infinite.of_injective (fun i => update m i (n i)) fun x y h => of_not_not fun hne => ?_
  simp_rw [update_eq_iff, update_of_ne hne] at h
  exact (hm x h.1.symm).elim

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

Goal state before:
pp: α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

Tactic:
exact pi_nonempty

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ Nodup (Quotient.map List.offDiag ⋯ s.val)

Tactic:
rcases s with ⟨⟨s⟩, hs⟩

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset α
val✝ : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
⊢ Nodup (Quotient.map List.offDiag ⋯ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs }.val)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
x : α × α
⊢ x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Tactic:
rcases s with ⟨⟨s⟩, hs⟩

Goal state after:
case mk
α : Type u_1
x : α × α
val✝ : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
⊢ x ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs }.offDiag ↔
    x.1 ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs } ∧
      x.2 ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs } ∧ x.1 ≠ x.2
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.offDiag = #s ^ 2 - #s

Tactic:
rcases s with ⟨⟨s⟩, hs⟩

Goal state after:
case mk
α : Type u_1
val✝ : Multiset α
s : List α
hs : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
⊢ #{ val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs }.offDiag =
    #{ val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs } ^ 2 -
      #{ val := Quot.mk (⇑(List.isSetoid α)) s, nodup := hs }