mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ∈ s

Tactic:
refine hs.out c.2 B.2 ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)

case refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: case H2
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ ↑r < ↑b'

Tactic:
simpa using h₂

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

Goal state before:
pp: case H2
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ ↑r < ↑b'

Tactic:
simpa using h₂

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ (∀ (x : ι), ¬x ∈ sᶜ → f x = 1) ↔ EqOn f 1 s

Tactic:
notMem_compl_iff,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ (∀ (x : ι), x ∈ s → f x = 1) ↔ EqOn f 1 s
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a : α
ha : 1 < a
⊢ 1 < a⁺ᵐ

Tactic:
by
  rwa [oneLePart_eq_self.2 ha.le]

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

Goal state before:
pp: i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1) * (i + n)!

Tactic:
Nat.add_mul,

Goal state after:
i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + 1 * (i + n)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + n + 1) * (1 + n)!

Tactic:
Nat.add_mul,

Goal state after:
i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + n) * (1 + n)! + 1 * (1 + n)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n * n ^ k ≤ n * n.succ.ascFactorial k

Tactic:
exact Nat.mul_le_mul (Nat.le_refl n)
      (Nat.le_trans (Nat.pow_le_pow_left (le_succ n) k) (pow_succ_le_ascFactorial n.succ k))

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

Goal state before:
pp: case inr
n k j : ℕ
hn : n > 0
⊢ (n + j) * n.ascFactorial j ≤ (j + 1) * j ! * (n * n ^ j)

Tactic:
Nat.mul_assoc (j + 1),

Goal state after:
case inr
n k j : ℕ
hn : n > 0
⊢ (n + j) * n.ascFactorial j ≤ (j + 1) * (j ! * (n * n ^ j))
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (2 * n)! ≤ (2 * n) ^ n * n !

Tactic:
by
  rw [Nat.two_mul, ← factorial_mul_ascFactorial, Nat.mul_comm]
  exact Nat.mul_le_mul_right _ (ascFactorial_le_pow_add _ _)

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

Goal state before:
pp: case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(↑a - ↑b).toPNat' = 1

Tactic:
tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)

Goal state after:
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ m = k * ⟨n.succ, ⋯⟩

Tactic:
← coe_inj,

Goal state after:
case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ ↑m = ↑(k * ⟨n.succ, ⋯⟩)
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
⊢ a < ↑⌊a⌋ + 1

Tactic:
by
  simpa only [Int.succ, Int.cast_add, Int.cast_one] using lt_succ_floor a

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Tactic:
rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]
  refine le_trans ?_ (sub_one_lt_floor _).le
  rw [sub_le_iff_le_add', ← add_sub_assoc, sub_le_sub_iff_right]
  exact floor_le _

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Tactic:
exact lt_mul_of_one_lt_right' (a ^ n) ha

Goal state after:
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 : n ≠ 0
a : R
⊢ ⌊↑n * a⌋ / ↑n = ⌊a⌋

Tactic:
rw [Nat.cast_comm, mul_natCast_floor_div_cancel 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
⊢ fract a + fract b ≤ fract (a + b) + 1

Tactic:
rw [fract, fract, fract, sub_add_sub_comm, sub_add, sub_le_sub_iff_left]
  exact mod_cast le_floor_add_floor a b

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 : fract a = fract b
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)

Tactic:
by unfold fract at h; rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]

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

Goal state before:
pp: n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * q.num ∧ ↑d = c * ↑q.den

Tactic:
rw [q_eq]

Goal state after:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hnp : 0 < n
hnsp : n.pred + 1 = n
hltn : n.pred < n
⊢ x < y ^ (n.pred + 1)

Tactic:
hnsp

Goal state after:
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hnp : 0 < n
hnsp : n.pred + 1 = n
hltn : n.pred < n
⊢ x < y ^ n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: 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
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
⊢ Nat.find this ≠ 0

Tactic:
intro hf

Goal state after:
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
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hf : Nat.find this = 0
⊢ False
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
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉ ⌊b⌋

Tactic:
simp [ceil_le, le_floor]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : Group G
inst✝ : Torsor G P
p : P
v : G
⊢ (fun x ↦ p /ₛ x) ((fun x ↦ x⁻¹ • p) v) = v

Tactic:
simp [sdiv_smul_eq_sdiv_div]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x✝² x✝¹ : List α
h : x✝² ≈ x✝¹
a✝ : α
l✝ l'✝ : List α
b✝ : C ⟦l✝⟧
b'✝ : C ⟦l'✝⟧
hl : l✝ ~ l'✝
x✝ : b✝ ≍ b'✝
⊢ C_cons a✝ ⟦l✝⟧ b✝ ≍ C_cons a✝ ⟦l'✝⟧ b'✝

Tactic:
congr 1; exact Quot.sound hl

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

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

Tactic:
rw [← card_add, Multiset.sub_add_cancel h]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ List.filter (fun x ↦ decide ¬x ∈ l₂) (List.filter (fun x ↦ x != a) l₁) = List.filter (fun x ↦ decide ¬x ∈ a :: l₂) l₁

Tactic:
filter_filter

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ List.filter (fun a_1 ↦ decide ¬a_1 ∈ l₂ && a_1 != a) l₁ = List.filter (fun x ↦ decide ¬x ∈ a :: l₂) l₁
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h₁ : a ∈ l₁
h₂ : a ∈ l₂
⊢ elem a l₂ = true

Tactic:
simpa using h₂

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
s : Multiset α
l : List α
⊢ (map f (Quot.mk (⇑(isSetoid α)) l)).dedup = map f (dedup (Quot.mk (⇑(isSetoid α)) l))

Tactic:
simp [List.dedup_map_of_injective hf l]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.take n' xs.reverse ~ ys ∩ (List.take n' xs.reverse).reverse

Tactic:
inter_reverse

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.take n' xs.reverse ~ ys ∩ List.take n' xs.reverse
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ replicate n x ∩ s = replicate (min (count x s) n) x

Tactic:
replicate_inter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x : α
⊢ replicate (min n (count x s)) x = replicate (min (count x s) n) x
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
k : α
hks : k ∈ s
hkx : f k = f x
⊢ False

Tactic:
hf hkx

Goal state after:
case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
k : α
hks : x ∈ s
hkx : f k = f x
⊢ False
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.filter (fun b_1 ↦ decide (b_1 = b)) l) = replicate (List.count b l) b

Tactic:
List.filter_eq,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
l : List α
⊢ ↑(List.replicate (List.count b l) b) = replicate (List.count b l) b
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)

Tactic:
by_cases h : p a

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : ¬p a
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)

Tactic:
by_cases h : p a

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
h : p a
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
h : ¬p a
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ a ∈ s.ndinter t ↔ a ∈ s ∧ a ∈ t

Tactic:
by
  simp [ndinter, mem_filter]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ ↑s = {a, b} ↔ s = {a, b}

Tactic:
by
  rw [← coe_pair, coe_inj]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ≠ insert a t

Tactic:
contrapose h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s = insert a t
⊢ a ∈ s
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∪ t ↔ Xor (x ∈ s) (x ∈ t)

Tactic:
rw [Finset.mem_union, Xor]

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ s.toFinset = Finset.univ ↔ s = univ

Tactic:
← coe_inj,

Goal state after:
α : Type u_1
s : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑s
⊢ ↑s.toFinset = ↑Finset.univ ↔ s = univ
Module: Mathlib.Order.Fin.Basic

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

Tactic:
intro hf

Goal state after:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
⊢ ∀ (i : Fin n), f i.castSucc ≠ f i.succ
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

Goal state after:
case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), f i.castSucc ≠ f i.succ
⊢ Injective ⇑f
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < b ↔ a ≤ b

Tactic:
rw [pred_lt_iff, castSucc_lt_succ_iff]

Goal state after:
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:
Nat.add_mul,

Goal state after:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
⊢ ↑i * n + n = ↑i * n + 1 * n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : j.succ < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

Tactic:
cases hj <| Nat.lt_trans j.castSucc_lt_succ hi

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
obtain h | h := i.lt_or_ge (succ j)
  · rw [succAbove_of_lt_succ _ _ h, succAbove_succ_of_lt _ _ h]
  · rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]

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

Goal state before:
pp: case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
      succAbove_pred_of_lt _ _ h]

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ [hd] <+ take (f 0 + 1) l'

Tactic:
List.singleton_sublist,

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ hd ∈ take (f 0 + 1) l'
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
⊢ p.removeNth (p.insertNth a f) = f

Tactic:
ext; unfold removeNth; simp

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
⊢ x :: a :: as <+ b :: orderedInsert r x bs

pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
· have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
        simp only [hr, orderedInsert_cons, ite_true] at ih
        exact .trans ih <| .cons _ (.refl _)

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
rw [insert_val, ndinsert_of_notMem h, Multiset.map_cons, fold_cons_left]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r b c

Tactic:
simpa using h₂

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : ¬Injective (codRestrict (s.domRestrict f) (f '' s) ⋯)
⊢ ¬InjOn f s

Tactic:
contrapose h

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ Injective (codRestrict (s.domRestrict f) (f '' s) ⋯)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : l.length = 0
⊢ l.rotate n = l.rotate' n

Tactic:
by simp_all [length_eq_zero_iff]

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

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

Tactic:
| cons a as h =>

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l₁ l₂ : List G
⊢ (a :: l₁ ++ l₂).alternatingProd = (a :: l₁).alternatingProd * l₂.alternatingProd ^ (-1) ^ (a :: l₁).length

Tactic:
by
    simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ s ⊆ t → s ≤ s.card • t

Tactic:
refine fun hsub ↦ le_iff_count.mpr fun a ↦ ?_

Goal state after:
α : Type u_1
s t : Multiset α
hsub : s ⊆ t
a : α
⊢ count a s ≤ count a (s.card • t)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
⊢ (map g1 S).prod ∣ (map g2 S).prod

Tactic:
apply Multiset.induction_on' S
  · simp
  intro a T haS _ IH
  simp [mul_dvd_mul (h a haS) IH]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f g : α → Finset β
hfg : ∀ (a : α), Disjoint (f a) (g a)
hfg' : (↑s).Pairwise fun a₁ a₂ ↦ Disjoint (f a₁) (g a₂)
hf : (↑s).PairwiseDisjoint f
hg : (↑s).PairwiseDisjoint g
⊢ (↑s).PairwiseDisjoint fun a ↦ (f a).disjUnion (g a) ⋯

Tactic:
intros i hi j hj hij
  simp [hf hi hj hij, hg hi hj hij, hfg' hi hj hij, (hfg' hj hi hij.symm).symm]

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
⊢ (s.dedup.bind f).dedup = (s.bind f).dedup

Tactic:
ext x
  -- Porting note: was `simp_rw [count_dedup, mem_bind, mem_dedup]`
  simp_rw [count_dedup]
  congr 1
  simp

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

Goal state before:
pp: n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = (n * (n - 1) + n * 2) / 2

pp: case H
n : ℕ
⊢ 0 < 2

Tactic:
← Nat.mul_add,

Goal state after:
n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1 + 2) / 2

case H
n : ℕ
⊢ 0 < 2
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
← Nat.mul_add,

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