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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ↪o β
⊢ ⇑f = ⇑g ↔ f = g

Tactic:
DFunLike.coe_fn_eq

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ↪o β
⊢ f = g ↔ f = g
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedLT β
inst✝ : Preorder α
⊢ Subsingleton (α ≃o β)

Tactic:
by
  refine ⟨fun f g ↦ ?_⟩
  change f.symm.symm = g.symm.symm
  rw [Subsingleton.elim f.symm]

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ a < b

Tactic:
rw [div_lt_iff₀ hb, one_mul]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, one_lt_div_of_neg]
  · simp [zero_le_one]
  · simp [hb, hb.not_gt, one_lt_div]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x y
⊢ R x y

Tactic:
| =>

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x y
⊢ R x y
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
x✝¹ : β
x✝ : α
h₃ : (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x✝ x✝¹
⊢ R x y

Tactic:
| =>

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) = (a✝, b✝) ∨ (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
x✝¹ : β
x✝ : α
h₃ : (x, y) ∈ zipWith Prod.mk l₁✝ l₂✝
h₁ : R x✝ x✝¹
⊢ R x y
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
l : List α
n : ℕ
a : α
⊢ l <+ l.insertIdx n a

Tactic:
by
  simpa only [eraseIdx_insertIdx_self] using eraseIdx_sublist (l.insertIdx n a) n

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
hn : n < l.length
⊢ (l.eraseIdx n).insertIdx n l[n] = l

Tactic:
simp [Nat.ne_of_lt hn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁ l₂

Tactic:
rw [← reverse_reverse l₁, ← reverse_reverse l₂]

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂.reverse.reverse
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
x : ι
xs : List ι
hl : x :: xs ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: xs)).prod = f (map f₁ (x :: xs)).prod (map f₂ (x :: xs)).prod

Tactic:
| =>

Goal state after:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
x : ι
xs : List ι
hl : x :: xs ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: xs)).prod = f (map f₁ (x :: xs)).prod (map f₂ (x :: xs)).prod
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
rw [perm_iff_count, ← Decidable.and_forall_ne a, ← Decidable.and_forall_ne b]
  suffices l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l by
    simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]
  trans ∀ c, c ∈ l → c = b ∨ c = a
  · simp [subset_def, or_comm]
  · exact forall_congr' fun _ => by rw [← and_imp, ← not_or, not_imp_not]

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

Goal state before:
pp: L : List ℕ
⊢ L.tail.sum = L.tail.sum + L.headI - L.headI

Tactic:
Nat.add_sub_cancel_right

Goal state after:
L : List ℕ
⊢ L.tail.sum = L.tail.sum
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: α : Type u_2
L : List (List α)
i : ℕ
⊢ drop (take i (map length L)).sum L.flatten = (drop i L).flatten

Tactic:
by
  induction L generalizing i
  · simp
  · cases i <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: case inl
α : Type u_1
inst✝ : CommMonoid α
x : α
⊢ x ∣ x ^ 0 ↔ 0 ≠ 0 ∨ IsUnit x

pp: case inr
α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
hn : n ≠ 0
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x

Tactic:
· simp [isUnit_iff_dvd_one]

Goal state after:
case inr
α : Type u_1
inst✝ : CommMonoid α
x : α
n : ℕ
hn : n ≠ 0
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑d₂ = ↑n₂ * ↑↑d₁
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
← Int.cast_mul,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑d₂ = ↑(n₂ * ↑d₁)
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ * ↑↑d₂ = ↑(n₂ * ↑d₁)
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
← Int.cast_mul,

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑(n₁ * ↑d₂) = ↑(n₂ * ↑d₁)
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑nr * ↑nr / (↑dr * ↑dr)

Tactic:
← Int.cast_mul,

Goal state after:
case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑(nr * nr) / (↑dr * ↑dr)
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = a * a + b * a - a * b - b * b

Tactic:
mul_comm b a,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : AddLeftReflectLE R
a b : R
⊢ a * a - b * b = a * a + a * b - a * b - b * b
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
⊢ ⨆ i, f ↑i = ⨆ i, f i

Tactic:
refine (iSup_comp_le f _).antisymm (iSup_mono' fun i => ?_)

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
⊢ ∃ i', f i ≤ f ↑i'
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x.2 = y.2

Tactic:
refine ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, ?_⟩)

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ f x.1 x.2 ∈ (fun a ↦ f a y.2) '' s
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

Tactic:
exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

Tactic:
exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α}, b ∈ [[a, c]] → a ≤ c → Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ b ∈ [[c, a]]

Tactic:
rwa [uIcc_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑e '' s).OrdConnected

Tactic:
erw [(e : α ≃o β).image_eq_preimage_symm]
  apply ordConnected_preimage (e : α ≃o β).symm

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

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

Tactic:
rwa [oneLePart_eq_self.2 ha.le]

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

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

Tactic:
| =>

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

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

Tactic:
| =>

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

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

Tactic:
| =>

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

Goal state before:
pp: case zero.succ
k n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) * (0 + (n✝ + 1)).ascFactorial k = ascFactorial 0 (n✝ + 1 + k)

Tactic:
· simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]

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

Goal state before:
pp: case succ
l k n' : ℕ
⊢ (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!

Tactic:
Nat.add_comm 1 l,

Goal state after:
case succ
l k n' : ℕ
⊢ (n' + l)! * (n' + (l + 1)).ascFactorial k = (n' + (l + k))!
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommGroup β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ |f x - f y| ≤ f (x / y)

Tactic:
by
  rw [abs_sub_le_iff, sub_le_iff_le_add', sub_le_iff_le_add']
  exact ⟨le_map_add_map_div _ _ _, le_map_add_map_div' _ _ _⟩

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if ↑2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌈↑⌊x⌋ + fract x⌉) = (⌊↑2 * ↑⌊x⌋ + ↑2 * fract x⌋ + 1) / 2

Tactic:
← Int.cast_mul,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if ↑2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌈↑⌊x⌋ + fract x⌉) = (⌊↑(2 * ⌊x⌋) + ↑2 * fract x⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ round x = ⌊x + 1 / 2⌋

Tactic:
rw [← cast_mul_floor_div_cancel_of_pos two_pos, round_eq_div]

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (⌊2 * x⌋ + 1) / 2 = ⌊↑2 * (x + 1 / 2)⌋ / 2
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
hn0 : n = 0
⊢ False

Tactic:
rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx

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

Goal state before:
pp: n d : ℕ
n_coprime_d : n.Coprime d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : d.gcd n = 1
⊢ (↑n % ↑d).natAbs.Coprime d

Tactic:
Nat.gcd_rec

Goal state after:
n d : ℕ
n_coprime_d : n.Coprime d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : (n % d).gcd d = 1
⊢ (↑n % ↑d).natAbs.Coprime d
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 ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉ ⌈b⌉

Tactic:
simp [ceil_le, lt_ceil]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ (g⁻¹ * h) • x = x → g⁻¹ * h = 1

Tactic:
exact H (g⁻¹ * h) x

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
⊢ {a} ⊆ s ↔ a ∈ s

Tactic:
by simp [subset_iff]

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

Goal state before:
pp: α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
⊢ r a x

Tactic:
obtain ⟨b, hb1, hb2⟩ := exists_mem_of_rel_of_mem (rel_flip.2 h) hx

Goal state after:
α : Type u_1
m : Multiset α
a : α
r : α → α → Prop
n : ℕ
h : Rel r (replicate n a) m
x : α
hx : x ∈ m
b : α
hb1 : b ∈ replicate n a
hb2 : flip r x b
⊢ r a x
Module: Mathlib.Data.List.Nodup

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

Tactic:
by simpa [ne_nil_of_mem hy]

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

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

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

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β → β
inst✝ : LeftCommutative f
x : β
q : α → Prop
p : β → Prop
hpqf : ∀ (a : α) (b : β), q a → p b → p (f a b)
px : p x
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → q a) → p (foldr f x s)
q_s : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → q a_1
⊢ p (foldr f x (a ::ₘ s))

Tactic:
simp only [forall_mem_cons, foldr_cons] at q_s ⊢
    exact hpqf _ _ q_s.1 (ihs q_s.2)

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ x :: xs ∪ ys = (x :: xs).dedup ++ ys

Tactic:
rw [cons_union]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs ∪ ys = xs.dedup ++ ys

Tactic:
induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [cons_union]
    rw [disjoint_cons_left] at h
    by_cases hx : x ∈ xs
    · rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]
    · rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]
      rw [mem_union_iff, not_or]
      exact ⟨hx, h.1⟩

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
⊢ count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card

Tactic:
· rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
    · simp
    · simp only [mem_filter, and_imp, @eq_comm _ (f x), imp_self, implies_true]

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

Goal state before:
pp: α : Type u_1
xs : List α
x : α
⊢ [] <:+: [x] ↔ [] = [] ∨ [] = [x]

Tactic:
| =>

Goal state after:
α : Type u_1
xs : List α
x : α
⊢ [] <:+: [x] ↔ [] = [] ∨ [] = [x]
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
xs : List α
x head✝ : α
⊢ [head✝] <:+: [x] ↔ [head✝] = [] ∨ [head✝] = [x]

Tactic:
| =>

Goal state after:
α : Type u_1
xs : List α
x head✝ : α
⊢ [head✝] <:+: [x] ↔ [head✝] = [] ∨ [head✝] = [x]
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] ↔ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]

Tactic:
| =>

Goal state after:
α : Type u_1
xs : List α
x head✝¹ head✝ : α
tail✝ : List α
⊢ head✝¹ :: head✝ :: tail✝ <:+: [x] ↔ head✝¹ :: head✝ :: tail✝ = [] ∨ head✝¹ :: head✝ :: tail✝ = [x]
Module: Mathlib.Data.Finset.Range

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (↑(range n)).Nontrivial

Tactic:
Finset.coe_range

Goal state after:
n : ℕ
hn : 1 < n
⊢ (Set.Iio n).Nontrivial
Module: Mathlib.Data.Fintype.Sets

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

Tactic:
rw [← s.coe_toFinset, h, t.coe_toFinset]

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

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

Tactic:
conv_rhs => rw [range_add_one]

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

Goal state before:
pp: n : ℕ
j : Fin (n + 1)
⊢ ↑j + ↑j.rev = n

Tactic:
obtain ⟨j, hj⟩ := j
  simp [Nat.add_sub_cancel' <| le_of_lt_succ hj]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ {x ∈ s | f x = y}.Nonempty ↔ y ∈ image f s

Tactic:
fiber_nonempty_iff_mem_image

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ y ∈ image f s ↔ y ∈ image f s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr.refine_2.inr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
H : ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
i : Fin (n + 1)
j : Fin n
ihj : (fun x1 x2 ↦ x1 < x2) i j.castSucc → r (f i) (f j.castSucc)
hij✝ : i ≤ j.castSucc
hij : ↑i < ↑j.castSucc
⊢ r (f i) (f j.succ)

Tactic:
exact _root_.trans (ihj hij) (H j)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
⊢ ↑(image f s) = ↑t

Tactic:
simp [hsurj.image_eq_of_mapsTo hf]

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b

Tactic:
simp_rw [ofFn_add]
  simp [Fin.append_left', Fin.append_right]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1

Tactic:
obtain (rfl | h') := Fin.eq_or_lt_of_le h
  · simp [val_sub, Nat.sub_add_cancel a.is_le]
  grind [castPred, val_sub_castLT_of_lt]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #(t \ s) + #s - #s

Tactic:
Nat.add_sub_cancel_right

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #(t \ s)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s \ t) + #(s ∩ t) = #s

Tactic:
← card_union_of_disjoint (disjoint_sdiff_inter _ _),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s \ t ∪ s ∩ t) = #s
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
f : Fin n → α
⊢ image f univ = (List.ofFn f).toFinset

Tactic:
by
  simp [Finset.image]

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

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

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_le_castSucc _ _ (le_castSucc_iff.2 h),
      succAbove_castPred_of_lt _ _ h]

Goal state after:
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
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
succAbove_castSucc_of_lt _ _ h,

Goal state after:
case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove i.castSucc = i
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
inst✝ : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
m n : ℕ
hmn : m ≠ n
⊢ (r on f) m n

Tactic:
grind +splitIndPred

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

Goal state before:
pp: case left
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin m
⊢ append xs ys (castAdd n i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (castAdd n i✝).rev)

Tactic:
simp [rev_castAdd]

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

Goal state before:
pp: case refine_1
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
obtain hm | hm := h
    · exact Or.inl ⟨rfl, hm⟩
    · exact Or.inr hm

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

Goal state before:
pp: case cons
α : 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]?
this : some hd = l'[f 0]?
⊢ hd :: tl <+ l'

Tactic:
rw [eq_comm, List.getElem?_eq_some_iff] at this

Goal state after:
case cons
α : 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]?
this : ∃ h, l'[f 0] = hd
⊢ hd :: tl <+ l'
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case cast
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
hx : Injective x
hx₀ : ¬x₀ ∈ Set.range x
j : Fin (n + 1)
i : Fin n
h : snoc x x₀ i.castSucc = snoc x x₀ j
⊢ i.castSucc = j

Tactic:
| cast i =>

Goal state after: