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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
x✝ : List α
⊢ Forall₂ R x✝ (map f []) ↔ Forall₂ (fun a c ↦ R a (f c)) x✝ []

Tactic:
by simp only [map, forall₂_nil_right_iff]

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

Goal state before:
pp: case cons.nil
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
h₁ : (a :: l₁).length = [].length
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ (a :: l₁).zip [] → R a_1 b
⊢ Forall₂ R (a :: l₁) []

Tactic:
simp at h₁

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

pp: case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂

Tactic:
· induction h with
    | nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
    | @cons a b l1 l2 rab _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
    | cons_right _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ l, Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []

Tactic:
rw [forall₂_nil_right_iff.1 hl1]

Goal state after:
case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []
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 * (ε * ε⁻¹) = 2 * (ε * a) * b * ε⁻¹

Tactic:
by simp_rw [mul_assoc, mul_comm ε, mul_assoc]

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

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
cases Nat.lt_or_ge (length l₂) n with
    | inl hn₂ => rw [insertIdx_of_length_lt hn₂]
    | inr hn₂ =>
      apply iff_of_false
      · intro h
        rw [h.length_eq] at hn₁
        grind
      · grind [Perm.length_eq]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
by
  by_cases hab : a = b
  · exact Or.inl hab
  · exact ((List.mem_cons.1 h).elim Or.inl (fun h => Or.inr ⟨hab, h⟩))

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

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
x : α
l : List α
⊢ (∃ y, y ∈ l ∧ f y = x) → f x ∈ l

Tactic:
by rintro ⟨y, h, rfl⟩; rwa [hf y]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
intro h
    rcases h with ⟨l₂, h₁₂, h₂₃⟩
    have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip
    rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩
    exact ⟨l', h₂.symm, h₁.flip⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
ha : a ≠ 0
⊢ zpow' a n = a ^ n

Tactic:
by
  simp [zpow', ha]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ idxOf a l = 0 ↔ l = [] ∨ l.head? = some a

Tactic:
cases l
  · simp
  · grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl : l₁ <+: l₂
a : α
⊢ a ∈ l₁ ↔ idxOf a l₂ < l₁.length

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · exact hl.idxOf_eq_of_mem h ▸ idxOf_lt_length_of_mem h
  · have := hl.idxOf_le a
    grind [List.idxOf_lt_length_iff]

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

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α → M
l : List α
⊢ (map f (filter (fun b ↦ decide (p b)) l)).prod * (map f (filter (fun x ↦ decide ¬p x) l)).prod = (map f l).prod

Tactic:
by
  rw [← prod_map_ite]
  simp only [ite_self]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ ⟨a, ha⟩ < toNonneg b ↔ ↑⟨a, ha⟩ < b

Tactic:
simp [toNonneg, ha.not_gt]

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

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ l.sum % n = (map (fun x ↦ x % n) l).sum % n

Tactic:
by
  induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

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

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ l.prod % n = (map (fun x ↦ x % n) l).prod % n

Tactic:
induction l with
  | nil => simp only [map_nil]
  | cons a l ih =>
    simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)

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

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d

Tactic:
by_cases hd : d = 0
  · rw [hd]
    simp
  rw [divInt_mul_divInt, x.mul_comm, divInt_mul_right hx]

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ q⁻¹ = divNat q.den q.num

Tactic:
ext; simp [Rat.inv_def, num_coe, den_coe]

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a * ((↑b)⁻¹ * ↑d) = ↑{ num := n, den := d, den_nz := h, reduced := c }.num

Tactic:
(d.commute_cast _).eq,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a * (↑d * (↑b)⁻¹) = ↑{ num := n, den := d, den_nz := h, reduced := c }.num
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ ⊤ ≤ iSup f ↔ ∀ b < ⊤, ∃ i, b < f i

Tactic:
le_iSup_iff_forall_lt

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ (∀ b < ⊤, ∃ i, b < f i) ↔ ∀ b < ⊤, ∃ i, b < f i
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
a : α
s : Set α
⊢ a ⊓ sSup s =
    ⨅ i,
      ⨆ j,
        match i, j with
        | { down := true }, j => a
        | { down := false }, j => ↑j

Tactic:
simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
hκ : Nonempty κ
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i

Tactic:
by
  rcases hκ with ⟨j⟩
  simp_rw [iInf_iSup_eq, mem_iInter]
  refine le_antisymm
    (iSup₂_le fun i hi ↦ le_iSup₂_of_le (fun _ ↦ i) hi (le_iInf fun _ ↦ le_rfl))
    (iSup₂_le fun I hI ↦ ?_)
  by_cases! H : ∀ k, I k = I j
  · exact le_iSup₂_of_le (I j) (fun k ↦ (H k) ▸ (hI k)) (iInf_le _ _)
  · rcases H with ⟨k, hk⟩
    calc ⨅ l, f (I l)
    _ ≤ f (I k) ⊓ f (I j) := le_inf (iInf_le _ _) (iInf_le _ _)
    _ = ⊥ := (h hk).eq_bot
    _ ≤ _ := bot_le

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y ∈ {x}
⊢ False

Tactic:
mem_singleton_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y = x
⊢ False
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ SuperChain r s (SuccChain r s)

Tactic:
by
  have : IsChain r s ∧ SuperChain r s h.choose := h.choose_spec
  simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ {x}
⊢ z ∈ s

Tactic:
mem_singleton_iff

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑(num✝¹ * ↑db) * ⅟↑db * ⅟↑da < ⅟↑db * ((fun x ↦ ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
simp? at h says simp only [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑num✝¹ * ⅟↑da < ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
apply Nat.mul_left_cancel (factorial_pos n')

Goal state after:
case succ
l k n' : ℕ
⊢ n' ! * ((n' + 1).ascFactorial l * (n' + 1 + l).ascFactorial k) = n' ! * (n' + 1).ascFactorial (l + k)
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⌋ + fract x) < 1 then ⌊↑⌊x⌋ + fract x⌋ else ⌈↑⌊x⌋ + fract x⌉) = (⌊2 * (↑⌊x⌋ + fract x)⌋ + 1) / 2

Tactic:
fract_intCast_add,

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

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

Tactic:
← div_zpow

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 < n
a b : α
hab : a < b
⊢ 1 < (b / a) ^ n
Module: Mathlib.Algebra.Order.Group.Basic

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

Tactic:
← div_zpow

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
n : ℤ
hn : 0 ≤ n
a b : α
hab : a ≤ b
⊢ 1 ≤ (b / a) ^ n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
have h_ne : s.Nonempty := ⟨-k, by simpa [s] using inv_le_inv' hk⟩

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
h_ne : s.Nonempty
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
⊢ q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den

Tactic:
right_distrib,

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + 1 * ↑q⁻¹.den
⊢ q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
Module: Mathlib.Algebra.Order.Floor.Ring

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

Tactic:
by
  ext
  simp [floor_lt, le_floor]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
← map_intCast f,

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ f ↑n ≤ f a ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ f a ≤ ↑n ↔ a ≤ ↑n

Tactic:
← map_intCast f,

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ f a ≤ f ↑n ↔ a ≤ ↑n
Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t

Tactic:
ext; simp [mem_smul, mem_smul_set, h]

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

Goal state before:
pp: case neg
α : Type u_1
a b : α
as bs : Multiset α
this✝ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this : a ∈ b ::ₘ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
have : a ∈ bs := by simpa [h]

Goal state after:
case neg
α : Type u_1
a b : α
as bs : Multiset α
this✝¹ : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝ : a ∈ b ::ₘ bs
this : a ∈ bs
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0

Tactic:
intros
    apply Rel.zero

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ range (map Subtype.val) = {l | ∀ (x : α), x ∈ l → x ∈ s}

Tactic:
by
  rw [range_list_map, Subtype.range_coe]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
⊢ ∀ (x : Multiset α), (∀ (x_1 : α), x_1 ∈ x → p x_1) → ∃ y, map c y = x

Tactic:
rintro ⟨l⟩ hl

Goal state after:
case mk
α : Type u_1
β : Type v
γ : Type u_2
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
x✝ : Multiset α
l : List α
hl : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x
⊢ ∃ y, map c y = Quot.mk (⇑(isSetoid α)) l
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
f : α → β
x : α
y : β
⊢ map (update f x y) l = if x ∈ l then (map f l).set (idxOf x l) y else map f l

Tactic:
by
  induction l with | nil => simp | cons hd tl ihl => ?_
  rw [nodup_cons] at hl
  simp only [mem_cons, map, ihl hl.2]
  by_cases H : hd = x
  · subst hd
    simp [hl.1]
  · simp [Ne.symm H, H, ← apply_ite (cons (f hd))]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
by_cases h : a ∈ dedup (l₁ ++ l₂)

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup

case neg
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : ¬a ∈ (l₁ ++ l₂).dedup
⊢ (a :: (l₁ ++ l₂)).dedup = List.insert a (l₁ ++ l₂).dedup
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ filter p (a ::ₘ s) = 0 + filter p s

Tactic:
· rw [filter_cons_of_neg _ h, Multiset.zero_add]

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

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : α → Option β
s : Multiset α
l : List α
⊢ List.filterMap f (List.filter (fun b ↦ decide (p b)) l) = List.filterMap (fun x ↦ if p x then f x else none) l

Tactic:
simpa using List.filterMap_filter (f := f) (p := p)

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

Goal state before:
pp: a b : ℕ
⊢ range (a + b) = range a ∪ map (fun x ↦ a + x) (range b)

Tactic:
by
  rw [range_add, add_eq_union_iff_disjoint]
  apply range_disjoint_map_add

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ Disjoint (s.erase a) (insert a t)

Tactic:
disjoint_insert_right

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ a ∉ s.erase a ∧ Disjoint (s.erase a) t
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: n m : ℕ
h : Nonempty (Fin n ↪ Fin m)
⊢ n ≤ m

Tactic:
induction n generalizing m with

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ n = 0 ∨ n = 1 ↔ n = 1

Tactic:
or_iff_right (NeZero.ne n)

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ n = 1 ↔ n = 1
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

Tactic:
rw [Fin.add_def]
  split
  · rw [natCast_emod, Int.emod_eq_of_lt] <;> lia
  · rw [natCast_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> lia

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

Goal state before:
pp: n : ℕ
k : Fin n
⊢ k ≠ 0 → 1 ≤ k

Tactic:
by
  have : NeZero n := k.neZero
  intro hk
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
  cases n with
  | zero => simp only [Fin.isValue, Fin.zero_le]
  | succ n => rwa [Fin.le_iff_val_le_val, Fin.val_one, Nat.one_le_iff_ne_zero, val_ne_zero_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #s = #t

Tactic:
calc
    #s = #s.attach := card_attach.symm
    _ = #(s.attach.image fun a ↦ i a.1 a.2) := Eq.symm ?_
    _ = #t := ?_
  · apply card_image_of_injective
    intro ⟨_, _⟩ ⟨_, _⟩ h
    simpa using i_inj _ _ _ _ h
  · congr 1
    ext b
    constructor <;> intro h
    · obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi
    · obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩

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

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n

Tactic:
Nat.mul_sub_right_distrib,

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n) * n - 1 * n + (n - (↑i % n + 1))) % n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n) * n - (↑i % n + 1)) % n

pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n

Tactic:
Nat.mul_sub_right_distrib,

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = (m * n - ↑i / n * n - (↑i % n + 1)) % n

n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ ofFn (f ∘ ⇑σ) ~ ofFn f

Tactic:
rw [ofFn_eq_map, ofFn_eq_map, ← map_map]

Goal state after:
n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ map f (map (⇑σ) (finRange n)) ~ map f (finRange n)
Module: Mathlib.Data.Fin.SuccPred

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

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

Tactic:
· rw [predAbove_of_le_castSucc _ _ (Fin.le_of_lt h), succAbove_castPred_of_lt _ _ h]

Goal state after:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.castSucc
h : p.castSucc < i
⊢ p.castSucc.succAbove (p.predAbove i) = i
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
cases j.castSucc.lt_or_le i with
  | inl h =>
    rw [predAbove_of_castSucc_lt _ _ h, succAbove_of_castSucc_lt _ _ h, predAbove_of_le_castSucc,
      castPred_castSucc]
    rwa [le_castSucc_iff, succ_pred]
  | inr h =>
    rw [predAbove_of_le_castSucc _ _ h, succAbove_of_le_castSucc _ _ h, predAbove_of_castSucc_lt,
      pred_succ]
    rwa [castSucc_castPred, ← le_castSucc_iff]

Goal state after:
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:
classical
    simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_four,
      ← exists_and_left, exists_comm (α := Finset α)]
    constructor
    · rintro ⟨a, b, c, d, t, hsub, hab, hac, had, hbc, hbd, hcd, rfl⟩
      exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩
    · rintro ⟨a, b, c, d, ha, hb, hc, hd, hab, hac, had, hbc, hbd, hcd⟩
      exact ⟨a, b, c, d, {a, b, c, d}, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ {z | r z x} ⊆ {z | r z y} ∧ ¬{z | r z y} ⊆ {z | r z x}

Tactic:
Finset.subset_iff,

Goal state after:
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, x_1 ∈ {z | r z x} → x_1 ∈ {z | r z y}) ∧ ¬∀ ⦃x_1 : α⦄, x_1 ∈ {z | r z y} → x_1 ∈ {z | r z x}