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

Goal state before:
pp: case inr.inl
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)
hny : y - 0 • a ∈ Ioc l (l + a)
⊢ R (f x) (f y)

Tactic:
exact hf x (Ico_subset_Icc_self hx) y (by simpa using Ioc_subset_Icc_self hny) hxy

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

Goal state before:
pp: case inr.inr.inr.refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ c ^ (-↑n) < b

Tactic:
rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

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

Goal state before:
pp: G : Type u_1
inst✝ : AddMonoid G
a x✝ : G
⊢ (Multiplicative.toAdd 1 +ᵥ AddConstMap.id) x✝ = 1 x✝

Tactic:
apply zero_add

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

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ 2 • (x -ᵥ y) = 2 • 0 ↔ y = x

Tactic:
h.eq_iff,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ x -ᵥ y = 0 ↔ y = x
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : 2 • (x₁ -ᵥ x₂) = 2 • 0
⊢ x₁ = x₂

Tactic:
h.eq_iff,

Goal state after:
G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : x₁ -ᵥ x₂ = 0
⊢ x₁ = x₂
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
inst✝ : AddCommGroup G
x x✝ : G
⊢ (pointReflection x) x✝ = (Equiv.subLeft (2 • x)) x✝

Tactic:
simp [pointReflection, sub_add_eq_add_sub, two_nsmul]

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ s + t = a ::ₘ (s + t)

Tactic:
← singleton_add,

Goal state after:
α : Type u_1
a : α
s t : Multiset α
⊢ {a} + s + t = a ::ₘ (s + t)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ {a} + s + t = a ::ₘ (s + t)

Tactic:
← singleton_add,

Goal state after:
α : Type u_1
a : α
s t : Multiset α
⊢ {a} + s + t = {a} + (s + t)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ (a ::ₘ s).erase a = a ::ₘ s.erase a

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
· simp [cons_erase h]

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case neg
α : Type u
x hd : α
tl : List α
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
h : (hd :: tl).Nodup
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

Tactic:
· rw [← Ne, hl] at hx
      rcases hx with (rfl | ⟨y, hy, hx⟩)
      · simp
      · suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]
        exact ⟨y, mem_cons_of_mem _ hy, hx⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ a ::ₘ s - t = a ::ₘ (s - t)

Tactic:
← singleton_add,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ {a} + s - t = a ::ₘ (s - t)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ {a} + s - t = a ::ₘ (s - t)

Tactic:
← singleton_add,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ {a} + s - t = {a} + (s - t)
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : α → Prop
inst✝ : DecidableEq α
⊢ (∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

Tactic:
by
  simp only [mem_union_iff, or_imp, forall_and]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
h : ¬b ∈ l₂
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
simpa [h] using bagInter_nil_iff_inter_nil l₁ l₂

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

Tactic:
Nat.min_eq_zero_iff,

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 : α), count a s = 0 ∨ count a t = 0
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case cons.succ
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.tails.length), l.tails[n] = drop n l
n : ℕ
h : n + 1 < (a :: l).tails.length
⊢ (a :: l).tails[n + 1] = drop (n + 1) (a :: l)

Tactic:
simp [ihl]

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

Goal state before:
pp: case cons.succ
α : Type u_1
a : α
l : List α
ihl : ∀ (n : ℕ) (h : n < l.inits.length), l.inits[n] = take n l
n : ℕ
h : n + 1 < (a :: l).inits.length
⊢ (a :: l).inits[n + 1] = take (n + 1) (a :: l)

Tactic:
simp [ihl]

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

Goal state before:
pp: case mk
α : Type u_5
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } t
⊢ a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } ∨ a ∈ t

Tactic:
rcases t with ⟨⟨t⟩⟩

Goal state after:
case mk.mk
α : Type u_5
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) t)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }
    { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }
⊢ a ∈
      { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }.disjUnion
        { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ } ∨
      a ∈ { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α β : Type u_4
h : α = β
s : Finset α
⊢ map (Equiv.cast h).toEmbedding s ≍ s

Tactic:
subst h
  simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ s = t

Tactic:
← s.coe_toFinset,

Goal state after:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ ↑s.toFinset = t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
| image Nat.succ (range (k + 1))

Tactic:
rw [range_add_one]

Goal state after:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
| image Nat.succ (insert k (range k))
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hab : b ≤ a
⊢ ↑(a - b) < ↑(last n)

Tactic:
exact val_sub_lt_of_lt_of_le (val_lt_last ha) hab

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

Goal state before:
pp: case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ ↑(e ⟨j, ⋯⟩) < ↑(e ⟨i, hi⟩)

Tactic:
← lt_def,

Goal state after:
case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ e ⟨j, ⋯⟩ < e ⟨i, hi⟩
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #s.attach

Tactic:
apply card_image_of_injective
    intro ⟨_, _⟩ ⟨_, _⟩ h
    simpa using i_inj _ _ _ _ h

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

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
⊢ i.rev.modNat = i.modNat.rev

Tactic:
ext
  have H₁ : i % n + 1 ≤ n := i.modNat.is_lt
  have H₂ : i / n < m := i.divNat.is_lt
  simp only [val_rev]
  calc
    (m * n - (i + 1)) % n = (m * n - ((i / n) * n + i % n + 1)) % n := by rw [Nat.div_add_mod']
    _ = ((m - i / n - 1) * n + (n - (i % n + 1))) % n := by
      rw [Nat.mul_sub_right_distrib, Nat.one_mul, Nat.sub_add_sub_cancel _ H₁,
        Nat.mul_sub_right_distrib, Nat.sub_sub, Nat.add_assoc]
      exact Nat.le_mul_of_pos_left _ <| Nat.le_sub_of_add_le' H₂
    _ = n - (i % n + 1) := by
      rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt]; exact i.modNat.rev.is_lt

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.SurjOn f ↑s ↑t
⊢ #t ≤ #s

Tactic:
unfold Set.SurjOn at hf; exact (card_le_card (mod_cast hf)).trans card_image_le

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
⊢ Injective p.succAbove

Tactic:
rintro i j hij

Goal state after:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : p.succAbove i = p.succAbove j
⊢ i = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hp : p ≠ 0
⊢ (p.pred hp).predAbove i = i.pred ⋯

Tactic:
predAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)

Goal state after:
n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hp : p ≠ 0
⊢ i.pred ⋯ = i.pred ⋯
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ image l.get univ = l.toFinset

Tactic:
by
  simp [univ_image_def]

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

Goal state before:
pp: α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs : s.Nonempty
⊢ p s hs

Tactic:
by
    obtain ⟨a, rfl⟩ | hs := hs.exists_eq_singleton_or_nontrivial
    · exact h₀ _
    · refine h₁ hs fun t ht hts ↦ ?_
      have := card_lt_card hts
      exact ht.strong_induction h₀ h₁

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

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l

Tactic:
duplicate_cons_iff_of_ne hx,

Goal state after:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ l ↔ [x, x] <+ y :: l
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
⊢ append x x₀ = snoc x (x₀ 0)

Tactic:
ext i
  refine Fin.addCases ?_ ?_ i <;> clear i
  · intro i
    rw [Fin.append_left]
    exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm
  · intro i
    rw [Subsingleton.elim i 0, Fin.append_right]
    exact (@snoc_last _ (fun _ => α) _ _).symm

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ orderedInsert r a (b :: m) = a :: b :: m

Tactic:
| cons b m =>

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ map f (orderedInsert r x (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))

Tactic:
List.map_orderedInsert _ s,

Goal state after:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ orderedInsert s (f x) (map f (insertionSort r xs)) = orderedInsert s (f x) (insertionSort s (map f xs))

case cons.hl₁
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r a x ↔ s (f a) (f x))

case cons.hl₂
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ ∀ (a : α), a ∈ insertionSort r xs → (r x a ↔ s (f x) (f a))
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
g : β → Option α
I : IsPartialInv f g
inst✝ : Fintype ↑(f '' s)
⊢ ∀ (x : α), x ∈ { val := Multiset.filterMap g (f '' s).toFinset.val, nodup := ⋯ } ↔ x ∈ s

Tactic:
simp [I.eq]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t, (t.Finite ∧ p t) ∧ t ⊆ f '' s) ↔ ∃ t, (t.Finite ∧ p (f '' t)) ∧ t ⊆ s

Tactic:
and_assoc,

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t, t.Finite ∧ p t ∧ t ⊆ f '' s) ↔ ∃ t, t.Finite ∧ p (f '' t) ∧ t ⊆ s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧
    (0 < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬False) ∧
      ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ

Tactic:
not_false_eq_true,

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ p (Fin.find (fun k ↦ p k.succ) ⋯).succ ∧
    (0 < (Fin.find (fun k ↦ p k.succ) ⋯).succ → True) ∧
      ∀ (i : Fin n), i.succ < (Fin.find (fun k ↦ p k.succ) ⋯).succ → ¬p i.succ
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ min y z < x ↔ x > y ∨ x > z

Tactic:
exact min_lt_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : List α
l₂ : List β
⊢ (l₁ ×ˢ l₂).length = l₁.length * l₂.length

Tactic:
by
  induction l₁ with
  | nil => exact (Nat.zero_mul _).symm
  | cons x l₁ IH =>
    simp only [length, product_cons, length_append, IH, Nat.add_mul, Nat.one_mul, length_map,
      Nat.add_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h✝ : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : p a = true
x✝¹ : α
h : x✝¹ ≠ a
x✝ : x✝¹ ∈ filter p (a :: as).dedup
⊢ (if a = x✝¹ then 1 else 0) = 0

Tactic:
by simp [h.symm]

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

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

Tactic:
rw [rotate'_cons_succ]

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (tl ++ [hd]).rotate' n ~ hd :: tl
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) l.ranges.flatten

Tactic:
rw [ranges_flatten]

Goal state after:
l s : List ℕ
hs : s ∈ l.ranges
⊢ Pairwise (fun x1 x2 ↦ x1 ≠ x2) (range l.sum)
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
s : Multiset α
n : ℕ
a : α
⊢ n • (a ::ₘ s) = n • {a} + n • s

Tactic:
← singleton_add,

Goal state after:
α : Type u_1
s : Multiset α
n : ℕ
a : α
⊢ n • ({a} + s) = n • {a} + n • s
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = ↑(List.flatMap f l)

Tactic:
List.flatMap,

Goal state after:
α : Type u_1
β : Type v
l : List α
f : α → List β
⊢ ((↑l).bind fun a ↦ ↑(f a)) = ↑(List.map f l).flatten
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
b : β
s : Multiset α
f : α → Multiset β
⊢ b ∈ s.bind f ↔ ∃ a, a ∈ s ∧ b ∈ f a

Tactic:
by
  simp [bind]

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

Goal state before:
pp: case h
ι : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
m : Multiset ι
f : ι → M
inst✝ : DecidableEq ι
i : ι
a✝ : List ι
hf : ∀ (i' : ι), i' ≠ i → i' ∈ ⟦a✝⟧ → f i' = 1
⊢ (map f ⟦a✝⟧).prod = f i ^ count i ⟦a✝⟧

Tactic:
simp [List.prod_map_eq_pow_single i f hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ x ∈ s, f x ∈ t
⊢ t.disjiUnion (fun a ↦ {x ∈ s | f x = a}) ⋯ = s

Tactic:
simpa [filter_eq_self]

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

Goal state before:
pp: n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n - k.succ).succ ! = (n - k.succ).succ * (n - k.succ)!

Tactic:
factorial_succ

Goal state after:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n - k.succ + 1) * (n - k.succ)! = (n - k.succ).succ * (n - k.succ)!
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 ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
h : (fun i ↦ update m i (n i)) x = (fun i ↦ update m i (n i)) y
hne : ¬x = y
⊢ False

Tactic:
simp_rw [update_eq_iff, update_of_ne hne] at h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
x y : ι
hne : ¬x = y
h : n x = m x ∧ ∀ (x_1 : ι), x_1 ≠ x → m x_1 = update m y (n y) x_1
⊢ False
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) * (m * (p + 1) + p)!

Tactic:
factorial_succ

Goal state after:
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 + 1) * (m * (p + 1) + p)!
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 + 1) * p ! * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1)! * (m + 1))

Tactic:
factorial_succ

Goal state after:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1)) =
    (m * (p + 1) + p).choose p * (m * (p + 1))! * ((p + 1) * p ! * (m + 1))
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: case mem
M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
hx : x ∈ s
⊢ p x

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n

Tactic:
have hm := congr_fun h m

Goal state after:
case refine_1
I : Type u
inst✝¹ : DecidableEq I
M : Type u_5
inst✝ : CommMonoid M
k l m n : I
u v : M
hu : u ≠ 1
hv : v ≠ 1
h : mulSingle k u * mulSingle l v = mulSingle m u * mulSingle n v
hk : (mulSingle k u * mulSingle l v) k = (mulSingle m u * mulSingle n v) k
hl : (mulSingle k u * mulSingle l v) l = (mulSingle m u * mulSingle n v) l
hm : (mulSingle k u * mulSingle l v) m = (mulSingle m u * mulSingle n v) m
⊢ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u * v = 1 ∧ k = l ∧ m = n
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case mem
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
hx : x ∈ s
⊢ p x

Tactic:
| mem x hx =>

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

Goal state before:
pp: case a.mem
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x✝ x : M
hx : x ∈ s
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set β
⊢ (⇑f ⁻¹' s) ^ 0 ⊆ ⇑f ⁻¹' s ^ 0

Tactic:
simp [Set.subset_def]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ ∨ Nontrivial ↥H

Tactic:
by
  have := nontrivial_iff_ne_bot H
  tauto

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
H : Subgroup G
f : G →* G'
inst✝ : IsMulCommutative ↥H
a : G
ha : a ∈ ↑H
b : G
hb : b ∈ ↑H
⊢ f a * f b = f b * f a

Tactic:
simpa [map_mul] using congr(f $(setLike_mul_comm ha hb))

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
⊢ f.ker = ⊤ ↔ f = 1

Tactic:
by
  simp [ker, ← top_le_iff, SetLike.le_def, f.ext_iff]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: ⊢ Countable ℕ+

Tactic:
delta PNat; infer_instance

Goal state after: