mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
have hm₁ : 0 ≤ m₁ := by
    simpa [m₁, ← @cast_le k, ← div_le_iff₀ hn] using FloorRing.gc_ceil_coe.le_u_l _

Goal state after:
case inr.inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
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
b : H
inst✝² : AddCommMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℕ
x : G
⊢ f (↑n + x) = f x + n • b

Tactic:
by
  simpa using map_nsmul_add f n x

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

Goal state before:
pp: case h
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ ≤ x

Tactic:
exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉ ≤ ↑⌈(b - 1)⁻¹⌉

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + (b - 1) * (b - 1)⁻¹ ≤ a + (b - 1) * a

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num

Tactic:
by
    -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
    have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using! tmp
    rwa [this]

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

Goal state before:
pp: case inr
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✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + 1 • a)) (f y)

Tactic:
trans f (l + n • a)

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✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + 1 • a)) (f (l + n • a))

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✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + n • a)) (f y)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ = ⌊a⌋

Tactic:
← Int.floor_toNat,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌊a⌋.toNat = ⌊a⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ = ↑⌊a⌋

Tactic:
rw [← Int.natCast_floor_eq_floor ha, Int.cast_natCast]

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
h : ∀ (x : K), ∃ n, x < ↑n
⊢ ∀ (x : K), ∃ n, x < ↑n

Tactic:
x

Goal state after:
K : Type u_4
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
h : ∀ (x : K), ∃ n, x < ↑n
x : K
⊢ ∃ n, x < ↑n
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
⊢ max x 0 = y - (y - max x 0)

Tactic:
rw [sub_sub_cancel]

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

Goal state before:
pp: case coe
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
x : WithBot M
y : M
hxy : 0 < ↑y
⊢ ∃ n, x ≤ n • ↑y

Tactic:
cases x with
    | bot => refine ⟨0, bot_le⟩
    | coe x => simpa [← WithBot.coe_nsmul] using (Archimedean.arch x (by simpa using hxy))

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

Goal state before:
pp: α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : l₁ <+~ l₂
⊢ map f l₁ <+~ map f l₂

Tactic:
obtain ⟨l, hl_perm, hl_sub⟩ := a

Goal state after:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
l : List α
hl_perm : l ~ l₁
hl_sub : l <+ l₂
⊢ map f l₁ <+~ map f l₂
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
⊢ ∀ {e : ↑l₁ = s₂} {H : ∀ (a : α), a ∈ s₂ → p a},
    Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H =
      ↑(List.pmap f l₁ H₁)

Tactic:
e

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : ↑l₁ = s₂
⊢ ∀ {H : ∀ (a : α), a ∈ s₂ → p a},
    Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H =
      ↑(List.pmap f l₁ H₁)
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a ∈ map f {a}

Tactic:
map_singleton,

Goal state after:
case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a ∈ {f a}
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case pos
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x y : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
hxy : y = x
⊢ map f ((y ::ₘ s).erase x) = (map f (y ::ₘ s)).erase (f x)

Tactic:
cases hxy

Goal state after:
case pos.refl
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
x : α
s : Multiset α
ih : map f (s.erase x) = (map f s).erase (f x)
⊢ map f ((x ::ₘ s).erase x) = (map f (x ::ₘ s)).erase (f x)
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ head✝ :: tail✝.bagInter (l₂.erase head✝) <+ (head✝ :: tail✝) ∩ l₂

Tactic:
rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]
      exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])

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

Goal state before:
pp: case pos
α : 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, p.subset h, IH (p.erase _)]

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

Goal state before:
pp: α : Type u_1
n m : ℕ
l : List α
⊢ dropSlice n m l = take n l ++ drop m (drop n l)

Tactic:
dropSlice_eq,

Goal state after:
α : Type u_1
n m : ℕ
l : List α
⊢ take n l ++ drop (n + m) l = take n l ++ drop m (drop n l)
Module: Mathlib.Data.Finset.SDiff

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
h : s ⊆ t
⊢ s \ u ⊆ t \ u

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
h : s ⊆ t
⊢ u \ t ⊆ u \ s

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map f (map g s) = map g' (map f' s)

Tactic:
by
  simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
⊢ map f.toEmbedding s ⊆ t

Tactic:
x

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
⊢ x ∈ map f.toEmbedding s → x ∈ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
⊢ s ⊆ map f.symm.toEmbedding t

Tactic:
x

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
⊢ x ∈ s → x ∈ map f.symm.toEmbedding t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.val.toList.length = #s

Tactic:
← Multiset.coe_card,

Goal state after:
α : Type u_1
s : Finset α
⊢ (↑s.val.toList).card = #s
Module: Mathlib.Data.Fin.Basic

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

Tactic:
rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt] <;> omega

Goal state after:
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
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
hmapsto' : Set.MapsTo f' ↑s.attach ↑t
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
intro b hb

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 ⋯
hinj' : Set.InjOn f' ↑s.attach
hmapsto' : Set.MapsTo f' ↑s.attach ↑t
b : β
hb : b ∈ t
⊢ ∃ a, ∃ (ha : a ∈ s), b = f a ha
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
y : α
⊢ ∀ (x : α), x ∈ {y} ↔ y = x

Tactic:
by simp [eq_comm]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
y : Fin n
hi : y.succ ≠ 0
⊢ predAbove 0 y.succ = y.succ.pred hi

Tactic:
exact predAbove_zero_succ

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

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝ : Nonempty α
H : #∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}

Tactic:
exact ⟨Classical.arbitrary α, empty_subset _⟩

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
x✝ : ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n
a : α
t : Finset α
w✝ : a ∉ t
hs : cons a t w✝ = s
right✝ : #t = n
⊢ #s = n + 1

Tactic:
simpa [← hs]

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 → α
hu : m = 0
l : Fin m
⊢ append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)

pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)

Tactic:
· exact (Fin.cast hu l).elim0

Goal state after:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)
Module: Mathlib.Data.List.Duplicate

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

Tactic:
| cons y l IH =>

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

Goal state before:
pp: case neg
m n : ℕ
α : Sort u_2
as : Fin n → α
bs : Fin m → α
b : α
i : ℕ
isLt : i < n + (m + 1)
lt_n : i < n
lt_add : ¬i < n + m
⊢ as ⟨i, ⋯⟩ = b

Tactic:
have := Nat.lt_add_right m lt_n
    contradiction

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 (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
List.map,

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))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (f x :: map f xs)
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (image g (cons x xs hx)) = fold op b (f ∘ g) (cons x xs hx)

Tactic:
fold_cons,

Goal state after:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ fold op b f (image g (cons x xs hx)) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)
Module: Mathlib.Data.Fin.Tuple.Basic

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

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

Tactic:
· exact Fin.find_min hᵢ (Fin.lt_def.mpr <| (Fin.castAdd_lt _ _).trans_le hm)

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ (find? fun x ↦ decide (p x)).get ⋯ = Fin.find p h

Tactic:
find?_decide_eq_dite,

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
⊢ (if h : ∃ i, p i then some (Fin.find p h) else none).get ⋯ = Fin.find p h
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : a = b
⊢ R a b

Tactic:
cases heq

Goal state after:
case refl
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a : α
hab : [a, a] <+ l
⊢ R a a
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
⊢ r c d →
    Relation.ReflTransGen r d b →
      (∃ l, IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b) → ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
e

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
⊢ Relation.ReflTransGen r d b →
    (∃ l, IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b) → ∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons.e_a
α : 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
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = countP p as

Tactic:
refine _root_.trans ?_ h

Goal state after:
case cons.e_a
α : 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
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).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:
rw [← singleton_add, nsmul_add]

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

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

Tactic:
mod_eq_of_lt this

Goal state after:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
hm' : l.length ≤ n % l.length + m
this : n % l.length + m - l.length < l.length
| n % l.length + m - l.length
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ ∀ (a_1 : α), a_1 ∈ n • {a} → p a_1

Tactic:
intro b hb

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
b : α
hb : b ∈ n • {a}
⊢ p b
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ ∀ (a_1 : α), a_1 ∈ n • {a} → ¬p a_1

Tactic:
intro b hb

Goal state after:
case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
b : α
hb : b ∈ n • {a}
⊢ ¬p b
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ unop l.prod = (map unop l).reverse.prod

Tactic:
rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
    op_comp_unop, map_id]

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

Goal state before:
pp: case succ
α : Type u
l : List α
n : ℕ
k : ℕ := n % l.reverse.length
k' : ℕ
hk' : k = k' + 1
⊢ l.reverse =
    l.reverse.rotate
      (l.reverse.length - (l.reverse.length - n % l.reverse.length) % l.reverse.length +
        (l.reverse.length - n % l.reverse.length))

Tactic:
rcases l with - | ⟨x, l⟩
    · simp
    · rw [Nat.mod_eq_of_lt, Nat.sub_add_cancel, rotate_length]
      · exact Nat.sub_le _ _
      · exact Nat.sub_lt (by simp) (by simp_all! [k])

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

Goal state before:
pp: case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Tactic:
· simp only [hn, or_false]
    refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
    rw [← rotate_mod, h, rotate_mod]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel p (s.bind f) (t.bind g)

Tactic:
apply rel_join
  rw [rel_map]
  exact hst.mono fun a _ b _ hr => h hr

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

Goal state before:
pp: α : Type u
l : List α
k : ℕ
⊢ (l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k

Tactic:
have : (l.rotate k).cyclicPermutations.length = length (l.cyclicPermutations.rotate k) := by
    cases l
    · simp
    · rw [length_cyclicPermutations_of_ne_nil] <;> simp
  refine ext_get this fun n hn hn' => ?_
  rw [get_rotate, get_cyclicPermutations, rotate_rotate, ← rotate_mod, Nat.add_comm]
  cases l <;> simp

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

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
⊢ (n + 1).choose (k + 1) = 0

Tactic:
have hnk : n < k := lt_of_succ_lt_succ hk

Goal state after:
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ (n + 1).choose (k + 1) = 0
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : Nonempty β
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ ∃ g, f = g ∘ s.domRestrict

Tactic:
by
  rw [dependsOn_iff_factorsThrough, factorsThrough_iff]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1) * n.choose k = (n.choose (k + 1) + n.choose k) * (k + 1)

Tactic:
Nat.add_comm (choose _ _),

Goal state after:
n k : ℕ
⊢ (n + 1) * n.choose k = (n.choose k + n.choose (k + 1)) * (k + 1)