mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case succ
α : Type u
m n✝ : ℕ
a✝ : ∀ (xs : List α), dropSlice n✝ m xs = take n✝ xs ++ drop (n✝ + m) xs
xs : List α
⊢ dropSlice (n✝ + 1) m xs = take (n✝ + 1) xs ++ drop (n✝ + 1 + m) xs

Tactic:
cases xs with grind [dropSlice]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a + (-(a / 2) + b / 2) < b

Tactic:
← add_assoc,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a + -(a / 2) + b / 2 < b
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
l : List α
hl : ∀ (x : α), x ∈ l → p x
⊢ (pmap f l hl).insertIdx (n + 1) (f a ha) = pmap f (l.insertIdx (n + 1) a) ⋯

Tactic:
cases l <;> simp_all

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

Goal state before:
pp: α : Type u_4
inst✝³ : CommRing α
inst✝² : NoZeroDivisors α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b : α
a0 : 0 ≤ a
b0 : 0 ≤ b
⊢ a * a = b * b ↔ a = b

Tactic:
by
  have := fun h ↦ le_antisymm (neg_nonneg.mp h) b0
  grind [sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * (ε * a) * b * ε⁻¹ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹

Tactic:
by gcongr; exact inv_nonneg.mpr hε.le

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

Goal state before:
pp: α : Type u_1
o₁ o₂ : Option α
⊢ o₁.toList ~ o₂.toList ↔ o₁ = o₂

Tactic:
refine ⟨fun p => ?_, fun e => e ▸ Perm.refl _⟩

Goal state after:
α : Type u_1
o₁ o₂ : Option α
p : o₁.toList ~ o₂.toList
⊢ o₁ = o₂
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : L ≠ 0
⊢ (e₁ = e₂) = (f₁ = f₂)

Tactic:
subst H₁ H₂
  rw [mul_right_inj' HL]

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

Goal state before:
pp: α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
⊢ a :: (b :: l).tail = b :: l

Tactic:
have : b = a := by simpa using h

Goal state after:
α : Type u
b : α
l : List α
a : α
h : a ∈ (b :: l).head?
this : b = a
⊢ a :: (b :: l).tail = b :: l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
h : ∀ (a : α), (∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1) → (map f as).prod = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Tactic:
| cons a' as h =>

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

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

Tactic:
simp only [← h, eval_cons, div_eq_mul_inv, mul_inv, ← zpow'_neg, sub_eq_add_neg, zpow'_add]

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval / l₂.eval = l.eval
⊢ l₁.eval * zpow' x r₁ * (l₂.eval⁻¹ * zpow' x (-r₂)) = l₁.eval * l₂.eval⁻¹ * (zpow' x r₁ * zpow' x (-r₂))
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (map (fun a ↦ if p a then f a else g a) (x :: xs)).prod =
    (map f (filter (fun b ↦ decide (p b)) (x :: xs))).prod * (map g (filter (fun a ↦ decide ¬p a) (x :: xs))).prod

Tactic:
simp only [map_cons, filter_cons, prod_cons] at ih ⊢

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) * (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
l : List α
⊢ filterMap (fun x ↦ none) l = []

Tactic:
by
  induction l <;> simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f l) ↔ Forall (p ∘ f) l

Tactic:
by
  induction l <;> simp [*]

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

Goal state before:
pp: q : ℚ
⊢ 0 < q.toNNRat ↔ 0 < q

Tactic:
by simp [toNNRat, ← coe_lt_coe]

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

Goal state before:
pp: case refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ↑q.den ≠ 0

Tactic:
exact Int.natCast_ne_zero.mpr (Rat.den_nz _)

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

Goal state before:
pp: case inr.refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ n = n / q.num * q.num

Tactic:
Int.ediv_mul_cancel hqdn

Goal state after:
case inr.refine_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ n = n
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q : ℚ
⊢ ↑(-q) = -↑q

Tactic:
by simp [cast_def, neg_div]

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

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (Int.negOfNat a).pow b = Int.negOfNat c

Tactic:
rw [← hb, Int.negOfNat_eq, Int.negOfNat_eq, Int.pow_eq, pow_succ, pow_mul, neg_pow_two, ← pow_mul,
    two_mul, pow_add, ← hc, ← h1]

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β ⊕ γ → α
c : α
⊢ ⨆ x, f x ≤ c ↔ (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j) ≤ c

Tactic:
simp only [sup_le_iff, iSup_le_iff, Sum.forall]

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

Goal state before:
pp: α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → SupSet (β i)
s : Set ((a : α) → β a)
a : α
⊢ sSup s a = sSup (eval a '' s)

Tactic:
simp [sSup_apply, iSup, image_eq_range]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i

Tactic:
refine (le_iSup_inf_iSup f g).antisymm ?_
  rw [iSup_inf_iSup]
  refine iSup_mono' fun i => ?_
  rcases directed_of (· ≤ ·) i.1 i.2 with ⟨j, h₁, h₂⟩
  exact ⟨j, inf_le_inf (hf h₁) (hg h₂)⟩

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : CompletelyDistribLattice.MinimalAxioms β
f : α → β
hf : Injective f
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
ι✝ : Type u
κ✝ : ι✝ → Type u
g : (a : ι✝) → κ✝ a → α
⊢ f (⨅ a, ⨆ b, g a b) = f (⨆ g_1, ⨅ a, g a (g_1 a))

Tactic:
by
    simp_rw [iInf, map_sInf, iInf_range, iSup, map_sSup, iSup_range, map_sInf, iInf_range,
      minAx.iInf_iSup_eq']

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

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)

Tactic:
· rintro ⟨z, hz⟩ x hx y hy _
    exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (symm <| hz _ hy)

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α
⊢ (Pairwise fun i j ↦ ¬f i = f j) ↔ Injective f

Tactic:
simp [Pairwise, Function.Injective, not_imp_not]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ∉ uIoo a b

Tactic:
simp +contextual [uIoo, le_of_lt]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ∉ uIoo a b

Tactic:
simp +contextual [uIoo, le_of_lt]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : LE A
inst✝ : IsConcreteLE A B
p q : A
⊢ ¬p ≤ q ↔ ∃ x, x ∈ p ∧ ¬x ∈ q

Tactic:
simpa [← coe_subset_coe] using! Set.not_subset

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
⊢ t ∩ u ⊆ t ∩ f ⁻¹' s

Tactic:
· rintro x ⟨xt, ⟨y, yt, yx, ys⟩, ⟨z, zt, xz, zs⟩⟩
    refine ⟨xt, ?_⟩
    apply hs.out ys zs
    exact ⟨hf yt xt yx, hf xt zt xz⟩

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

Goal state before:
pp: m n : ℕ
h : 1 < n ∨ 1 < m
⊢ n ! = m ! ↔ n = m

Tactic:
by
  obtain hn | hm := h
  · exact factorial_inj hn
  · rw [eq_comm, factorial_inj hm, eq_comm]

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

Goal state before:
pp: n l k : ℕ
⊢ n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k)

Tactic:
cases n with

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

Goal state before:
pp: n k : ℕ
⊢ (n - k) * n.descFactorial k = 0 ↔ n < k.succ

Tactic:
mul_eq_zero,

Goal state after:
n k : ℕ
⊢ n - k = 0 ∨ n.descFactorial k = 0 ↔ n < k.succ
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(n + 1))⁻¹ = (↑(n + 1))⁻¹

Tactic:
rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(x - ↑z)

Tactic:
conv_rhs => rw [← fract_add_floor x]

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(fract x + ↑⌊x⌋ - ↑z)
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ -(↑⌊x⌋ - ↑z) + -fract x

Tactic:
neg_sub,

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ ↑z - ↑⌊x⌋ + -fract x
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:
Int.cast_sub,

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) - ↑⌊b⌋ ≤ a
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) - a ≤ ↑⌊b⌋

Tactic:
Int.cast_sub,

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_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
hn : 0 < n
a : R
⊢ ⌊a * ↑n⌋ / n = ⌊a⌋

Tactic:
by
  refine eq_of_forall_le_iff fun m ↦ ?_
  rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, cast_mul,
    mul_le_mul_iff_of_pos_right (cast_pos.mpr 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 : a - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)

Tactic:
Int.cast_sub,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : a - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ a - b = ↑⌊a⌋ - ↑⌊b⌋
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = ↑(z - y)

Tactic:
Int.cast_sub,

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z - ↑y
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z

Tactic:
by
  rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff,
    and_comm]

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 ≤ ↑(⌈a + b⌉ + 1 - ⌈b⌉)

Tactic:
Int.cast_sub,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a ≤ ↑(⌈a + b⌉ + 1) - ↑⌈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
a b : R
⊢ a + (b + 1) ≤ ↑⌈a + b⌉ + 1

Tactic:
← add_assoc,

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⌉ + 1
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✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
| f x - n • b

Tactic:
rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]

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✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
| f (x - n • a)
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)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
⊢ R (f x) (f y)

Tactic:
rcases existsUnique_sub_zsmul_mem_Ico ha x l with ⟨m, hm, -⟩

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)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
⊢ R (f x) (f y)
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:
by
  rw [← sdiv_smul_eq_sdiv_div, sdiv_smul]

Goal state after:
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
k : ℤ
⊢ R (f (l + k • a)) (f (l + (1 • a + k • a)))

Tactic:
← add_assoc,

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
k : ℤ
⊢ R (f (l + k • a)) (f (l + 1 • a + k • a))
Module: Mathlib.Data.List.Count

Goal state before:
pp: α : Type u_1
l : List α
p : α → Bool
⊢ countP p l < l.length ↔ ∃ a, a ∈ l ∧ p a = false

Tactic:
by
  simp [Nat.lt_iff_le_and_ne, countP_le_length]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
rw [← cons_erase m] at h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t
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₁
b : β
hab : r a b
bs₀ bs₁ : Multiset β
h₀ : Rel r s bs₀
h₁ : Rel r as₁ bs₁
⊢ ∃ bs₀_1 bs₁_1,
    (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀_1 = b ::ₘ bs') ∧ Rel r as₁ bs₁_1 ∧ b ::ₘ (bs₀ + bs₁) = bs₀_1 + bs₁_1

Tactic:
exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩

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

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
⊢ m.toList = [a] ↔ m = {a}

Tactic:
by
  rw [← perm_singleton, ← coe_eq_coe, coe_toList, coe_singleton]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
ih : map f (filter p s) = filterMap (fun a ↦ if p a then some (f a) else none) s
⊢ map f (filter p (a ::ₘ s)) = filterMap (fun a ↦ if p a then some (f a) else none) (a ::ₘ s)

Tactic:
| cons a s ih =>

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

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

Tactic:
cases n with

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

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

Tactic:
cases n with

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

Goal state before:
pp: α : Type u_4
H : ∀ (s : Finset α), s = ∅
a : α
⊢ False

Tactic:
specialize H {a}; aesop

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

Goal state before:
pp: n : ℕ
k : Fin n.succ
this : NeZero n.succ
hk : k ≠ 0
⊢ 1 ≤ k

Tactic:
cases n with

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

Goal state before:
pp: n : ℕ
y : Fin n
h : y.castSucc ≠ last n
⊢ (y.castSucc.castPred h).castSucc = y.castSucc

Tactic:
castPred_castSucc

Goal state after:
n : ℕ
y : Fin n
h : y.castSucc ≠ last n
⊢ y.castSucc = y.castSucc
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
⊢ j.castSucc.castPred ⋯ = j

Tactic:
castPred_castSucc

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : i ≤ p
⊢ i.castSucc.castPred ⋯ = i

Tactic:
castPred_castSucc

Goal state after:
n : ℕ
p i : Fin n
h : i ≤ p
⊢ i = i
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i.castSucc.castPred ⋯ = i

Tactic:
castPred_castSucc

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ i = i
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
inst✝ : DecidableEq α
h : #s = n + 1
a : α
has : a ∈ s
⊢ #(s.erase a) = n

Tactic:
simp only [h, card_erase_of_mem has, Nat.add_sub_cancel_right]

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc.castPred ⋯ = j

pp: case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc ≤ (i.pred ⋯).castSucc

Tactic:
castPred_castSucc

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j = j

case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc ≤ (i.pred ⋯).castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1.refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ append a b (natAdd m lr) = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))

Tactic:
· rw [append_right]
      simp [castAdd_natAdd]

Goal state after:
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
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
let g (i : ℕ) : Finset α := s.image f^[i]
  have (i : ℕ) : 0 < #(g i) := (hs₀.image _).card_pos
  have hg : Antitone g := antitone_nat_of_succ_le <| fun i ↦ by
    simp_rw [g, Function.iterate_succ, ← image_image]
    grw [hs.finsetImage_subset]
  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⟩
  have hG : Antitone (fun i ↦ #(g i) - 1) := fun i j h ↦ by dsimp; gcongr #?_ - 1; exact hg h
  rcases Nat.stabilises_of_antitone hG (by grind [=_ image_image, iterate_succ']) with ⟨n, hn, hn'⟩
  exact ⟨n, by grind⟩

Goal state after: