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

Goal state before:
pp: case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorial k

Tactic:
← add_descFactorial_eq_ascFactorial'

Goal state after:
case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1 + k - 1).descFactorial k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
by
  let h₀ := Nat.mod_add_div (m : ℕ) (k : ℕ)
  have : ¬((m : ℕ) % (k : ℕ) = 0 ∧ (m : ℕ) / (k : ℕ) = 0) := by
    rintro ⟨hr, hq⟩
    rw [hr, hq, mul_zero, zero_add] at h₀
    exact (m.ne_zero h₀.symm).elim
  have := modDivAux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this
  exact this.trans h₀

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ (fun x ↦ x ^ n) a ≤ (fun x ↦ x ^ n) b

Tactic:
rw [← one_le_div', ← div_zpow]; exact one_le_zpow (one_le_div'.2 hab) hn

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
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ fract a = b

Tactic:
← self_sub_floor,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - ↑⌊a⌋ = b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌊a⌋ + 1 - 1 < a

Tactic:
add_tsub_cancel_right,

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌊a⌋ < a
Module: Mathlib.Algebra.AddConstMap.Basic

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

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:
· assumption

Goal state after:
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)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a b : R
⊢ Int.cast ⁻¹' Ico a b = Ico ⌈a⌉ ⌈b⌉

Tactic:
ext
  simp [ceil_le, lt_ceil]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ g • p₁ = g • (p₁ /ₛ p₂) • p₂

Tactic:
sdiv_smul

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ g • p₁ = g • p₁
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ p₁ = (p₁ /ₛ p₃) • p₃

Tactic:
sdiv_smul

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ p₁ = p₁
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ p₁ /ₛ (p₂ /ₛ p₃) • p₃ = p₁ /ₛ p₂

Tactic:
sdiv_smul

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ p₁ /ₛ p₂ = p₁ /ₛ p₂
Module: Mathlib.Algebra.AddConstMap.Basic

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

Tactic:
· assumption

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p /ₛ p₁ = p /ₛ p₂
⊢ (p /ₛ p₁) • p₁ = p

Tactic:
sdiv_smul

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p /ₛ p₁ = p /ₛ p₂
⊢ p = p
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
s s' : Multiset α
hs : s = s'
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
hp : ∀ (x : α), x ∈ s → p x = p' x
⊢ countP p s = countP p' s'

Tactic:
revert hs hp
  exact Quot.induction_on₂ s s'
    (fun l l' hs hp => by
      simp only [quot_mk_to_coe'', coe_eq_coe] at hs
      apply hs.countP_congr
      simpa using hp)

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

Goal state before:
pp: α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m < replicate (n + 1) x ↔ m ≤ replicate n x

Tactic:
by
  rw [lt_iff_cons_le]
  constructor
  · rintro ⟨x', hx'⟩
    have := eq_of_mem_replicate (mem_of_le hx' (mem_cons_self _ _))
    rwa [this, replicate_succ, cons_le_cons_iff] at hx'
  · intro h
    rw [replicate_succ]
    exact ⟨x, cons_le_cons _ h⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s - t ≤ u ↔ s ≤ t + u

Tactic:
rw [Multiset.sub_le_iff_le_add, Multiset.add_comm]

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

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:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset γ
f : γ → α
⊢ ∀ (a : γ) (s : Multiset γ),
    (∀ {t : Multiset β}, Rel r (map f s) t ↔ Rel (fun a b ↦ r (f a) b) s t) →
      ∀ {t : Multiset β}, Rel r (map f (a ::ₘ s)) t ↔ Rel (fun a b ↦ r (f a) b) (a ::ₘ s) t

Tactic:
simp +contextual [rel_cons_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u

Tactic:
rw [← eq_union_left h₂]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ (s ∪ t + s) ∩ (s ∪ t + t)

Tactic:
refine le_inter (Multiset.add_le_add_right le_union_right) ?_

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ s ∪ t + t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ countP (fun x ↦ a = x) s = (filter (fun x ↦ a = x) s).card

Tactic:
countP_eq_card_filter

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ (filter (fun x ↦ a = x) s).card = (filter (fun x ↦ a = x) s).card
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:
by
  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.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
rw [Finset.Nontrivial, coe_toFinset]

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ (∀ (i : Fin n), f i.castSucc ≠ f i.succ) → Injective ⇑f

Tactic:
intro hf
    refine (strictMono_iff_lt_succ (f := f).2 fun i ↦ ?_).injective
    exact lt_of_le_of_ne (f.monotone (Fin.castSucc_le_succ i)) (hf i)

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

Goal state before:
pp: α : Sort u_1
k k' l' : ℕ
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin k → Fin l' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Tactic:
subst h'

Goal state after:
α : Sort u_1
k k' : ℕ
f g : Fin k → Fin k' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
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
⊢ Injective fun a ↦ i ↑a ⋯

Tactic:
intro ⟨_, _⟩ ⟨_, _⟩ h

Goal state after:
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
val✝¹ : α
property✝¹ : val✝¹ ∈ s
val✝ : α
property✝ : val✝ ∈ s
h : (fun a ↦ i ↑a ⋯) ⟨val✝¹, property✝¹⟩ = (fun a ↦ i ↑a ⋯) ⟨val✝, property✝⟩
⊢ ⟨val✝¹, property✝¹⟩ = ⟨val✝, property✝⟩
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
⊢ ↑i * n + n = (↑i + 1) * n

Tactic:
rw [Nat.add_mul, Nat.one_mul]

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

Goal state before:
pp: n : ℕ
x✝¹ x✝ : Fin (n + 1)
h : x✝¹.succAbove = x✝.succAbove
⊢ x✝¹ = x✝

Tactic:
simpa [range_succAbove] using congr_arg (fun f : Fin n → Fin (n + 1) => (Set.range f)ᶜ) h

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

Goal state before:
pp: case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ (g ∘ cons y q) j'.succ = (g ∘ q) j'

Tactic:
comp_apply,

Goal state after:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ g (cons y q j'.succ) = (g ∘ q) j'
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ g (cons y q j'.succ) = (g ∘ q) j'

Tactic:
comp_apply,

Goal state after:
case neg
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ g (cons y q j'.succ) = g (q j')
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
⊢ ∃ a, f a = x

Tactic:
have h₁ : image f univ = univ :=
    eq_of_subset_of_card_le (subset_univ _)
      ((card_image_of_injective univ hinj).symm ▸ le_rfl)

Goal state after:
case intro
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
⊢ ∃ a, f a = x
Module: Mathlib.Data.List.Duplicate

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

pp: case neg.cons_cons
α : Type u_1
l✝ : List α
x : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = x
a✝ : [x] <+ l
⊢ [x, x] <+ l

Tactic:
· assumption

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

Goal state before:
pp: case refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
r : Fin (m * n)
⊢ «repeat» m.succ a (Fin.cast ⋯ (natAdd n r)) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd n r))

Tactic:
· simp [modNat]

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

Goal state before:
pp: case refine_1
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
l : Fin (m₁ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (castAdd (m₂ * n) l)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (castAdd (m₂ * n) l))

pp: case refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (natAdd (m₁ * n) r)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd (m₁ * n) r))

Tactic:
· simp [modNat]

Goal state after:
case refine_2
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
r : Fin (m₂ * n)
⊢ «repeat» (m₁ + m₂) a (Fin.cast ⋯ (natAdd (m₁ * n) r)) =
    (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ (natAdd (m₁ * n) r))
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
have eq_iff (i j : ℕ) : #(g i) - 1 = #(g j) - 1 ↔ g i = g j := by
    wlog hij : j ≤ i generalizing i j
    · grind
    exact ⟨fun h ↦ eq_of_subset_of_card_le (hg hij) (by grind), by grind⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
⊢ xₙ = yₙ

Tactic:
simpa using congr_fun h (last n)

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Infinite α
x : α
_hx : x ∉ ∅
y : α
hy : y ∉ {x}
⊢ y ≠ x

Tactic:
by simpa only [mem_singleton] using hy

Goal state after:
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 α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ Multiset.fold op b (Multiset.map f s.val) = Multiset.fold op b (Multiset.map g s.val)

Tactic:
map_congr rfl H

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ Multiset.fold op b (Multiset.map g s.val) = Multiset.fold op b (Multiset.map g s.val)
Module: Mathlib.Data.List.Sort

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

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

Goal state after:
α : Type u_1
l : List α
inst✝ : Preorder α
⊢ (∀ (i : ℕ) (h : i < l.length) (i_1 : ℕ) (h_1 : i_1 < l.length),
      ⟨i, h⟩ < ⟨i_1, h_1⟩ → l.get ⟨i_1, h_1⟩ < l.get ⟨i, h⟩) ↔
    Pairwise (fun x1 x2 ↦ x1 > x2) l
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case refine_1.inl
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b
⊢ Lex r (a :: l₁) (b :: l₂)

Tactic:
exact Lex.rel h

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

Goal state before:
pp: case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
⊢ (range a).Disjoint (map (fun x ↦ a + x) s')

Tactic:
intro u hu

Goal state after:
case cons.left
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
s' : List ℕ
left✝ : s' ∈ l.ranges
hs : map (fun x ↦ a + x) s' ∈ map (map fun x ↦ a + x) l.ranges
u : ℕ
hu : u ∈ range a
⊢ u ∈ map (fun x ↦ a + x) s' → False
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case succ
α : Type u_3
f : α → α
l : List α
hl : IsChain (fun x y ↦ f x = y) l
i : ℕ
h : ∀ (hi : i < l.length), f^[i] l[0] = l[i]
hi : i + 1 < l.length
⊢ f^[i + 1] l[0] = l[i + 1]

Tactic:
rw [Function.iterate_succ', Function.comp_apply, h (by lia)]
    rw [List.isChain_iff_getElem] at hl
    apply hl

Goal state after:
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
hlt : n % l.length < l.length
⊢ l[m - (drop (n % l.length) l).length]? = l[(m + n) % l.length]?

pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Tactic:
length_drop

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

case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length
Module: Mathlib.Data.List.Rotate

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

Tactic:
length_drop

Goal state after:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : l.length - n % l.length ≤ m
hlt : n % l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mpr
α : Type u
l l' : List α
⊢ l ~r l' → l ∈ l'.cyclicPermutations

Tactic:
rintro ⟨k, rfl⟩
    rw [cyclicPermutations_rotate, mem_rotate]
    apply mem_cyclicPermutations_self

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

Goal state before:
pp: m : ℕ
⊢ 2 * m + 1 = 1 + m + m

Tactic:
Nat.add_assoc 1 m m,

Goal state after:
m : ℕ
⊢ 2 * m + 1 = 1 + (m + m)
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.choose (k + 1) * (k + 1) + (n.choose k.succ * n.succ - n.choose k.succ * k.succ)

Tactic:
Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)

Goal state after:
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = n.choose (k + 1) * (n + 1)
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ S ^ n * {a} = S ^ (n + 1)

Tactic:
refine Set.eq_of_subset_of_card_le ?_ (le_trans (ge_of_eq h) ?_)

Goal state after:
case refine_1
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ S ^ n * {a} ⊆ S ^ (n + 1)

case refine_2
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(S ^ n * Set.singleton a)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑(S ^ n * {a})
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ f '' s⁻¹ = g '' s

Tactic:
rw [← Set.image_inv_eq_inv, Set.image_image]

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ (fun x ↦ f x⁻¹) '' s = g '' s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

Tactic:
intro x hz hw

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
hw : w ∈ t x
⊢ (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑↑H

Tactic:
hg

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑{g}
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ map f (H ⊔ K) = ⊤

Tactic:
codisjoint_iff.mp h,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H K : Subgroup G
h : Codisjoint H K
⊢ map f ⊤ = ⊤