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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ f b * f a < f c * f a

Tactic:
refine mul_lt_mul_of_pos_right (lt.2 hbc) ?_

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ 0 < f a
Module: Mathlib.Algebra.Order.Nonneg.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : { x // 0 ≤ x }
⊢ 0 ≤ q • ↑a

Tactic:
rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg a.2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)

Tactic:
have : range f ⊆ insert 1 (f '' k) :=
    (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_mono h))
  grind

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

Goal state before:
pp: case inr
m n : ℕ
hm : 1 < m
⊢ n ! = m ! ↔ n = m

Tactic:
eq_comm,

Goal state after:
case inr
m n : ℕ
hm : 1 < m
⊢ m ! = n ! ↔ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1) * (n + 1) ^ n = (n + 1) ^ (n + 1)

Tactic:
pow_succ'

Goal state after:
n : ℕ
⊢ (n + 1) * (n + 1) ^ n = (n + 1) * (n + 1) ^ n
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n.succ.descFactorial n.succ = n.succ !

Tactic:
succ_descFactorial_succ,

Goal state after:
n : ℕ
⊢ (n + 1) * n.descFactorial n = n.succ !
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + k).succ.descFactorial k.succ = (n + 1).ascFactorial k.succ

Tactic:
succ_descFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + k + 1) * (n + k).descFactorial k = (n + 1).ascFactorial k.succ
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k.succ ≤ n.succ
⊢ (n.succ - k.succ)! * n.succ.descFactorial k.succ = n.succ !

Tactic:
succ_descFactorial_succ,

Goal state after:
n k : ℕ
h : k.succ ≤ n.succ
⊢ (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a + 1) = round a + 1

Tactic:
rw [← round_add_intCast a 1, cast_one]

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

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

Tactic:
exact Int.sub_one_lt_floor (x + 1 / 2)

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

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℤ
hn✝ : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / ↑n⌋ = ⌊a⌋ / n

Tactic:
← div_mul_cancel₀ (a := a) (ne_of_gt (Int.cast_pos.mpr hn))

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℤ
hn✝ : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / ↑n⌋ = ⌊a / ↑n * ↑n⌋ / n
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
⊢ a - ↑⌊a⌋ = b

Tactic:
eq_comm,

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
⊢ b = a - ↑⌊a⌋
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
r : α
n d : ℕ
⊢ IsNNRat r n d → IsNat ⌊r⌋ (n / d)

Tactic:
rintro ⟨inv, rfl⟩
  constructor
  simp only [invOf_eq_inv, ← div_eq_mul_inv]
  rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, cast_natCast]

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

Goal state before:
pp: q : ℚ
this : ↑q.num < (q - fract q + 1) * ↑q.den
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den

Tactic:
by
    have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
    rwa [this]

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 : β
⊢ x = g⁻¹ • h • x → g = h

Tactic:
eq_comm,

Goal state after:
α : 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
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
inst✝ : AddMonoid G
a : G
x✝² x✝¹ : Multiplicative G
x✝ : G
⊢ (Multiplicative.toAdd (x✝² * x✝¹) +ᵥ AddConstMap.id) x✝ =
    ((Multiplicative.toAdd x✝² +ᵥ AddConstMap.id) * (Multiplicative.toAdd x✝¹ +ᵥ AddConstMap.id)) x✝

Tactic:
apply add_assoc

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ p₄ : P
⊢ (p₁ /ₛ p₂) / (p₃ /ₛ p₄) = (p₁ /ₛ p₃) / (p₂ /ₛ p₄)

Tactic:
by
  rw [← sdiv_smul_eq_sdiv_div, sdiv_smul_comm, sdiv_smul_eq_sdiv_div]

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

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

Tactic:
simp only [quot_mk_to_coe'', coe_eq_coe] at hs
      apply hs.countP_congr
      simpa using hp

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

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ (x -ᵥ y) +ᵥ x = y ↔ y = x

Tactic:
eq_comm,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ y = (x -ᵥ y) +ᵥ x ↔ y = x
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ y -ᵥ x = x -ᵥ y ↔ y = x

Tactic:
← neg_vsub_eq_vsub_rev,

Goal state after:
G : Type u_3
P : Type u_4
inst✝ : AddGroup G
T : AddTorsor G P
x y : P
h : Injective fun x ↦ 2 • x
⊢ -(x -ᵥ y) = x -ᵥ y ↔ y = x
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : x₂ -ᵥ x₁ = x₁ -ᵥ x₂
⊢ x₁ = x₂

Tactic:
← neg_vsub_eq_vsub_rev,

Goal state after:
G : Type u_5
P : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x ↦ 2 • x
y x₁ x₂ : P
hy : -(x₁ -ᵥ x₂) = x₁ -ᵥ x₂
⊢ x₁ = x₂
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
⊢ Rel r (a ::ₘ as) bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Tactic:
generalize hm : a ::ₘ as = m

Goal state after:
case mp
α : Type u_1
β : Type v
r : α → β → Prop
a : α
as : Multiset α
bs : Multiset β
m : Multiset α
hm : a ::ₘ as = m
⊢ Rel r m bs → ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ (a ::ₘ s).erase a = a ::ₘ s.erase a

Tactic:
simp [cons_erase h]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
H : l.Nodup
i : Fin l.length
⊢ idxOf (l.get i) l = ↑i

Tactic:
simp [H]

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

Goal state before:
pp: case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, l₂.Nodup → (l₁ ∪ l₂).Nodup
l₂ : List α
h : l₂.Nodup
⊢ (a :: l₁ ∪ l₂).Nodup

Tactic:
| cons a l₁ ih =>

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ 0 = map f s ↔ s = 0

Tactic:
eq_comm,

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ map f s = 0 ↔ s = 0
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t

Tactic:
have : b ∈ s.map f := by
      rw [h]
      exact mem_cons_self _ _

Goal state after:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
this : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b ∧ map f (s.erase a) = t
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ a, map f a = f y ::ₘ map f t

Tactic:
exact ⟨y ::ₘ t, map_cons _ _ _⟩

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

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ filter p (map f (Quot.mk (⇑(isSetoid β)) l)) = map f (filter (p ∘ f) (Quot.mk (⇑(isSetoid β)) l))

Tactic:
simp [List.filter_map]

Goal state after:
α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ List.map f (List.filter ((fun b ↦ decide (p b)) ∘ f) l) ~ List.map f (List.filter (fun b ↦ decide (p (f b))) l)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s - t) + count a (s ∩ t) = count a (s - t) + min (count a s) (count a t)

Tactic:
rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
x✝ : List α
d : Nodup (Quot.mk (⇑(isSetoid α)) x✝)
⊢ x✝.erase a = List.filter (fun b ↦ decide ((fun x ↦ x ≠ a) b)) x✝

Tactic:
by simpa using! List.Nodup.erase_eq_filter d a

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (↑l₁).ndinter ↑l₂ = ↑(l₁ ∩ l₂)

Tactic:
simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]
  apply Perm.refl

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

Goal state before:
pp: α : Type u_1
m : Multiset α
hm : m.Nodup
⊢ { val := m, nodup := hm }.Nonempty ↔ m ≠ 0

Tactic:
induction m using Multiset.induction_on <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = s ∪ t ↔ t ⊆ s

Tactic:
eq_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∪ t = s ↔ t ⊆ s
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = t ∪ s ↔ t ⊆ s

Tactic:
eq_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ∪ s = s ↔ t ⊆ s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ∅ = map f s ↔ s = ∅

Tactic:
eq_comm,

Goal state after:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ map f s = ∅ ↔ s = ∅
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ ∅ = image f s ↔ s = ∅

Tactic:
eq_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ image f s = ∅ ↔ s = ∅
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
constructor
  · intro h
    let : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩
    lift t to Finset s using h
    refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩
    ext y; simp
  · grind

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

Goal state before:
pp: α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : #s < #t + #u
⊢ (t ∩ u).Nonempty

Tactic:
contrapose! hstu

Goal state after:
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ #t + #u ≤ #s
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ #s ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
refine ⟨fun H => ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
⊢ ∃ x, s ⊆ {x}

case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → #s ≤ 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
lt_iff_add_one_le,

Goal state after:
α : Type u_1
s : Finset α
⊢ 2 + 1 ≤ #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
⊢ ∃ a, f a = x

Tactic:
have := Classical.propDecidable

Goal state after:
α : Type u_1
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
⊢ ∃ a, f a = x
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 3 < #s ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
lt_iff_add_one_le,

Goal state after:
α : Type u_1
s : Finset α
⊢ 3 + 1 ≤ #s ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ x i = cons (x₀ 0) x (i.addNat 1)

Tactic:
eq_comm,

Goal state after:
case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x (i.addNat 1) = x i
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ card { i // ↑i < m } = card (Fin m)

Tactic:
apply Fintype.card_congr

Goal state after:
m n : ℕ
h : m ≤ n
⊢ { i // ↑i < m } ≃ Fin m
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:
eq_comm,

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 : l'[f 0]? = some hd
⊢ hd :: tl <+ l'
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.6
inst✝ : Fintype α
⊢ Trunc { f // Bijective f }

Tactic:
unfold card Finset.card
  refine
    Quot.recOnSubsingleton
      (motive := fun s : Multiset α =>
        (∀ x : α, x ∈ s) → s.Nodup → Trunc {f : Fin (Multiset.card s) → α // Bijective f})
      univ.val
      (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getBijectionOfForallMemList _ h))
      mem_univ_val univ.2

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

Goal state before:
pp: n : ℕ
P : Fin (n + 1) → Prop
i : Fin (n + 1)
hi : P i
⊢ P (last n) ∨ ∃ i, P i.castSucc

Tactic:
cases i using lastCases with

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

Goal state before:
pp: case p
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j✝ : Fin n
hi : P (p.succAbove j✝)
⊢ P p ∨ ∃ i, P (p.succAbove i)

Tactic:
· exact .inr ⟨_, hi⟩

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

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : some l[i] = l'[f i]?
⊢ f i < l'.length

Tactic:
eq_comm,

Goal state after:
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
hf : l'[f i]? = some l[i]
⊢ f i < l'.length
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)

Tactic:
· rintro ⟨n, m, hnm, h, h'⟩
      refine ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) ?_, ?_⟩
      · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
        · simp
        · simp [hnm]
        · simp
        · simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
          simp [hi, hj]
      · rintro ⟨⟨_ | i⟩, hi⟩
        · simpa using h
        · simpa using h'

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

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ u n = c (u '' Iio n)

Tactic:
rw [image_eq_range]

Goal state after:
γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ u n = c (range fun x ↦ u ↑x)
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 : α
⊢ (decide (r a b) || decide (r b a)) = true

Tactic:
simpa using Std.Total.total a b

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedLE ↔ l.SortedGE

Tactic:
grind [OrderDual.ofDual_le_ofDual]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedGE ↔ l.SortedLE

Tactic:
grind [OrderDual.ofDual_le_ofDual]

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ (l ++ l').rotate' l.length = l' ++ l

Tactic:
induction l generalizing l'

Goal state after:
case nil
α : Type u
l' : List α
⊢ ([] ++ l').rotate' [].length = l' ++ []

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ [] = l.rotate n ↔ [] = l

Tactic:
eq_comm,

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n = [] ↔ [] = l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ [] = l.rotate n ↔ [] = l

Tactic:
by
  rw [eq_comm, rotate_eq_nil_iff, eq_comm]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ [x] = l.rotate n ↔ [x] = l

Tactic:
eq_comm,

Goal state after:
α : Type u
l : List α
n : ℕ
x : α
⊢ l.rotate n = [x] ↔ [x] = l
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
⊢ (s.bind fun x ↦ 0) = 0

Tactic:
simp [bind, join, nsmul_zero]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (S.bind f)

Tactic:
obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx

Goal state after:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b ↦ count a (f b)) S = count a (f x) ::ₘ m'
⊢ count a (f x) ≤ count a (S.bind f)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)

Tactic:
by
  simp_rw [← card_pos, ← one_lt_card_iff_nontrivial, card_product]; apply Nat.one_lt_mul_iff

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n ! / ((n - k)! * (n - (n - k))!) = n ! / (k ! * (n - k)!)

Tactic:
Nat.sub_sub_self hk,

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ n ! / ((n - k)! * k !) = n ! / (k ! * (n - k)!)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a

Tactic:
simp only [piFinset, mem_map, and_imp, forall_prop_of_true, mem_univ, exists_imp,
      mem_pi]

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ ∀ (x : (a : α) → a ∈ univ → δ a),
    (∀ (a : α), x a ⋯ ∈ t a) → { toFun := fun f a ↦ f a ⋯, inj' := ⋯ } x = f → ∀ (a : α), f a ∈ t a
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ Quotient.lift conjugatesOf ⋯ (ConjClasses.mk b) ↔ ConjClasses.mk a = ConjClasses.mk b

Tactic:
eq_comm,

Goal state after:
α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ Quotient.lift conjugatesOf ⋯ (ConjClasses.mk b) ↔ ConjClasses.mk b = ConjClasses.mk a
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ sᶜ = f '' f ⁻¹' sᶜ ↔ (range f)ᶜ ⊆ s

Tactic:
eq_comm,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' f ⁻¹' sᶜ = sᶜ ↔ (range f)ᶜ ⊆ s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x default ∈ s i

Tactic:
by
    rw [this]
    apply hx

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

Goal state before:
pp: case mem
M : Type u_1
inst✝ : Mul M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y : M
hy : y ∈ closure s
z : M
hz : z ∈ s
⊢ p z y ⋯ hy

Tactic:
| mem z hz =>

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j

Tactic:
rcases eq_or_ne i j with (rfl | h)

Goal state after:
case inl
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
⊢ Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i

case inr
I : Type u
f : I → Type v
i : I
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Group (f i)
g : (i : I) → f i
x : f i
j : I
h : i ≠ j
⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ image2 f s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i)

Tactic:
simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i => mem_image2_of_mem hx (hy _)

Goal state after: