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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
x y : WithBot α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
⊢ (∀ (z : α), ↑z < x → ↑z ≤ y) ↔ x ≤ y

Tactic:
by
  cases x <;> cases y <;> simp [exists_lt, forall_lt_imp_le_iff_le_of_dense]

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
a : α
b : β
⊢ f a ∣ b ↔ a ∣ (↑f).symm b

Tactic:
obtain ⟨c, rfl⟩ : ∃ c, f c = b := EquivLike.surjective f b

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Semigroup α
inst✝² : Semigroup β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
a c : α
⊢ f a ∣ f c ↔ a ∣ (↑f).symm (f c)
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
by
  rw [← not_nonempty_iff_eq_empty, image2_nonempty_iff, not_and_or]
  simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Ioc a b

Tactic:
rw [← Icc_sdiff_left]

Goal state after:
case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
h₃ : a ≤ c
h₄ : d ≤ b
⊢ a = c ∧ b = d

Tactic:
exact ⟨le_antisymm h₃ h₂, le_antisymm h₁ h₄⟩

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

Goal state before:
pp: α : Type ?u.3
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : ↑k * b * c = 1
⊢ Invertible b

Tactic:
Nat.cast_commute k,

Goal state after:
α : Type ?u.3
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : b * ↑k * c = 1
⊢ Invertible b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ ≤ (a ^ m)⁻¹

Tactic:
convert one_div_pow_le_one_div_pow_of_le a1 mn

Goal state after:
case e'_3
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

case e'_4
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ m)⁻¹ = 1 / a ^ m
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
l : List α
n : ℕ
hn : n ≠ l.length
a : α
⊢ (l.eraseIdx n).insertIdx n a = l.set n a

Tactic:
induction n generalizing l <;> cases l

Goal state after:
case zero.nil
α : Type u
a : α
hn : 0 ≠ [].length
⊢ ([].eraseIdx 0).insertIdx 0 a = [].set 0 a

case zero.cons
α : Type u
a head✝ : α
tail✝ : List α
hn : 0 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx 0).insertIdx 0 a = (head✝ :: tail✝).set 0 a

case succ.nil
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
hn : n✝ + 1 ≠ [].length
⊢ ([].eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = [].set (n✝ + 1) a

case succ.cons
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
head✝ : α
tail✝ : List α
hn : n✝ + 1 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = (head✝ :: tail✝).set (n✝ + 1) a
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
cases Nat.lt_or_ge m l₁.length with
  | inl hm =>
    rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h
    cases h with
    | intro hn hnm =>
      rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
        rel_congr_right (getElem_cons_eraseIdx_perm ..)]
  | inr hm =>
    rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h
    rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ flatMap f l ++ (g a ++ flatMap g l) ~ g a ++ (flatMap f l ++ flatMap g l)

Tactic:
rw [← append_assoc, ← append_assoc]

Goal state after:
case cons
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun x ↦ f x ++ g x) l
⊢ flatMap f l ++ g a ++ flatMap g l ~ g a ++ flatMap f l ++ flatMap g l
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝³ : MonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : PosMulStrictMono M
inst✝ : PosMulReflectLT M
e₁ e₂ f₁ f₂ L : M
H₁ : e₁ = L * f₁
H₂ : e₂ = L * f₂
HL : 0 < L
⊢ (e₁ < e₂) = (f₁ < f₂)

Tactic:
subst H₁ H₂
  apply Iff.eq
  exact mul_lt_mul_iff_of_pos_left HL

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ (x :: xs).prod * (y :: ys).prod =
    (zipWith (fun x1 x2 ↦ x1 * x2) (x :: xs) (y :: ys)).prod * (drop (y :: ys).length (x :: xs)).prod *
      (drop (x :: xs).length (y :: ys)).prod

Tactic:
simp only [zipWith_cons_cons, prod_cons]
    conv =>
      lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
    simp [mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a * b⁻¹ * (c * d⁻¹) = a * c * (d⁻¹ * b⁻¹)

Tactic:
hbd.inv_inv.symm.eq,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a * b⁻¹ * (c * d⁻¹) = a * c * (b⁻¹ * d⁻¹)
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 * ↑d * (↑b)⁻¹ = ↑{ num := n, den := d, den_nz := h, reduced := c }.num

Tactic:
this,

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
⊢ ↑n * ↑b * (↑b)⁻¹ = ↑{ num := n, den := d, den_nz := h, reduced := c }.num
Module: Mathlib.Data.Tree.Basic

Goal state before:
pp: case node
α : Type u
β : Type u_1
γ : Type u_2
f : α → β
g : β → γ
v : α
l r : BinaryTree α
hl : map (g ∘ f) l = map g (map f l)
hr : map (g ∘ f) r = map g (map f r)
⊢ map (g ∘ f) (node v l r) = map g (map f (node v l r))

Tactic:
rw [map, map, map, hl, hr, Function.comp_apply]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨆ x ∈ {0} ∪ range Nat.succ, u x = ⨆ i, u i

Tactic:
Nat.zero_union_range_succ,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨆ x ∈ univ, u x = ⨆ i, u i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a

Tactic:
have : Nonempty { i // p i } :=
    let ⟨i, hi⟩ := h
    ⟨⟨i, hi⟩⟩
  rw [iSup_subtype', iSup_subtype', iSup_sup]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
⊢ sSup s = sSup t

Tactic:
have Bs : BddAbove s := by
      rcases B with hB | ⟨b, hb⟩
      · exact hB
      · refine ⟨b, fun x hx ↦ ?_⟩
        rcases hs x hx with ⟨y, hy, hxy⟩
        exact hxy.trans (hb hy)

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
⊢ sSup s = sSup t
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rcases exists_between h₁ with ⟨x, xa, xb⟩
    constructor <;> refine le_of_not_gt fun h' => ?_
    · have ab := (h ⟨xa, xb⟩).1.trans xb
      exact lt_irrefl _ (h ⟨h', ab⟩).1
    · have ab := xa.trans (h ⟨xa, xb⟩).2
      exact lt_irrefl _ (h ⟨ab, h'⟩).2

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

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ s.OrdConnected

Tactic:
rw [ordConnected_iff]
  intro x hx y hy hxy
  rcases eq_or_lt_of_le hxy with (rfl | hxy'); · simpa
  rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']
  exact insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩

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

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

Tactic:
refine ⟨xt, ?_⟩

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
y : β
yt : y ∈ t
yx : y ≤ x
ys : f y ∈ s
z : β
zt : z ∈ t
xz : x ≤ z
zs : f z ∈ s
⊢ x ∈ f ⁻¹' s
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : ⇑e '' c ⊆ t
⊢ ⇑e '' c = t

Tactic:
rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, ← Equiv.image_symm_eq_preimage]
    exact hc.2 (ht.image _ fun _ _ ↦ e.symm.map_rel_iff.mp)
      ((e.toEquiv.subset_symm_image _ _).2 hf)

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ IsEmpty α ↔ s = ∅

Tactic:
refine ⟨fun _ ↦ s.eq_empty_of_isEmpty, fun h' ↦ ?_⟩
  constructor
  intro x
  simp only [IsMaxAntichain, h', IsAntichain.empty, empty_subset, forall_const, true_and] at h
  exact singleton_ne_empty x (h IsAntichain.singleton).symm

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
| |x - ↑z|

Tactic:
abs_eq_self.mpr (sub_nonneg.mpr hx),

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : ↑z ≤ x
| x - ↑z
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
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ -↑l₀
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

Tactic:
Right.nonneg_neg_iff,

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : ↑l₀ ≤ 0
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n d : ℕ
⊢ ⌊↑n / ↑d⌋₊ = n / d

Tactic:
rw [← Int.ofNat_inj, Int.natCast_floor_eq_floor (by positivity)]
  push_cast
  exact floor_intCast_div_natCast n d

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 : R
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - ↑⌈a⌉

Tactic:
this,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
this : ↑⌈a⌉ = ↑⌊a⌋ + 1
⊢ fract a = a + 1 - (↑⌊a⌋ + 1)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
y : R
inst✝ : ExistsAddOfLE R
x : R
hy1 : 1 < y
⊢ ∃ n, x < y ^ n

Tactic:
by
  obtain ⟨z, hz, rfl⟩ := exists_pos_add_of_lt' hy1
  rw [add_comm]
  exact add_one_pow_unbounded_of_pos _ hz

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

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

Tactic:
suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den from mod_cast this
  suffices (q.num : ℚ) < (q - fract q + 1) * q.den by
    have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
    rwa [this]
  suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den by
    have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
      calc
        (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
        _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
        _ = q.num + (1 - fract q) * q.den := by simp
    rwa [this]
  suffices 0 < (1 - fract q) * q.den by
    rw [← sub_lt_iff_lt_add']
    simpa
  have : 0 < 1 - fract q := by
    have : fract q < 1 := fract_lt_one q
    have : 0 + fract q < 1 := by simp [this]
    rwa [lt_sub_iff_add_lt]
  exact mul_pos this (by exact mod_cast q.pos)

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

Goal state before:
pp: case inr.inr.inr
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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
· have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
        obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁
        refine ⟨-n, ?_, ?_⟩
        · rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂
        · rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

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

Goal state before:
pp: case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x' ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x

Tactic:
this,

Goal state after:
case mp
α : Type u_1
m : Multiset α
x : α
n : ℕ
x' : α
hx' : x ::ₘ m ≤ replicate (n + 1) x
this : x' = x
⊢ m ≤ replicate n x
Module: Mathlib.Data.Set.List

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

Tactic:
rw [← Set.mem_range, Set.range_list_map]
    exact fun a ha => CanLift.prf a (H a ha)

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

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

Tactic:
by
  induction s using Multiset.induction with
  | empty => simpa
  | cons a s ihs =>
    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: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ a ∈ l.dedup ↔ a ∈ l

Tactic:
have := not_congr (@forall_mem_pwFilter α (· ≠ ·) _ ?_ a l)

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
this : (¬∀ (b : α), b ∈ pwFilter (fun x1 x2 ↦ x1 ≠ x2) l → a ≠ b) ↔ ¬∀ (b : α), b ∈ l → a ≠ b
⊢ a ∈ l.dedup ↔ a ∈ l

case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, x ≠ z → x ≠ y ∨ y ≠ z
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
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 : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map g t

Tactic:
this,

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
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 : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map g (map (fun x ↦ i ↑x ⋯) s.attach)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: 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

Tactic:
dedup_cons_of_notMem' h,

Goal state after:
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.List.Lattice

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
⊢ (head✝ :: tail✝).bagInter l₂ <+ (head✝ :: tail✝) ∩ l₂

Tactic:
rw [cons_bagInter]

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
⊢ (if head✝ ∈ l₂ then head✝ :: tail✝.bagInter (l₂.erase head✝) else tail✝.bagInter l₂) <+ (head✝ :: tail✝) ∩ l₂
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList.length = s.card

Tactic:
rw [← coe_card, coe_toList]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l l₁✝ l₂ l₃ : List α
a✝ b : α
inst✝ : DecidableEq α
a : α
l₁ : List α
x✝ : a :: l₁ <:+: []
s t : List α
te : s ++ a :: l₁ ++ t = []
⊢ False

Tactic:
simp at te

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
· rw [ndinsert_of_notMem h] at ht
      subst ht
      simp [attach_cons, h]

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
⊢ x✝ ⊆ filter (fun x ↦ p x ∧ ¬q x) s → x✝ ⊆ filter (fun x ↦ q x ∧ ¬p x) s → x✝ ⊆ ⊥

Tactic:
htp

Goal state after:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ⊆ filter (fun x ↦ p x ∧ ¬q x) s
⊢ x✝ ⊆ filter (fun x ↦ q x ∧ ¬p x) s → x✝ ⊆ ⊥
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
by
  rw [val_add]
  simp [Nat.mod_eq_of_lt huv]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ image f^[i] (image f s) ⊆ image f^[i] s

Tactic:
grw [hs.finsetImage_subset]

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

Goal state before:
pp: case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ append x x₀ (castAdd 1 i) = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
Fin.append_left

Goal state after:
case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (castAdd 1 i)
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]?
⊢ hd :: tl <+ l'

Tactic:
| cons hd tl IH =>

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]?
⊢ hd :: tl <+ l'
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
simp only [insertNth, succAboveCases, dif_neg (succAbove_ne _ _), succAbove_lt_iff_castSucc_lt]
  split_ifs with hlt
  · generalize_proofs H₁ H₂; revert H₂
    generalize hk : castPred ((succAbove i) j) H₁ = k
    rw [castPred_succAbove _ _ hlt] at hk; cases hk
    intro; rfl
  · generalize_proofs H₀ H₁ H₂; revert H₂
    generalize hk : pred (succAbove i j) H₁ = k
    rw [pred_succAbove _ _ (Fin.not_lt.1 hlt)] at hk; cases hk
    intro; rfl

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
xₚ yₚ : α p
x y : (j : Fin n) → α (p.succAbove j)
h : p.insertNth xₚ x = p.insertNth yₚ y
⊢ xₚ = yₚ

Tactic:
by simpa using congr_fun h p

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

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t

Tactic:
by
  simp only [← Finset.coe_subset, Finite.coe_toFinset]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (update f p x) = p.removeNth f

Tactic:
ext i; simp [removeNth]

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ fold op (op b₁ b₂) (s₁ + s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)

Tactic:
fold_add op

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ op (fold op b₁ s₁) (fold op b₂ s₂) = op (fold op b₁ s₁) (fold op b₂ s₂)
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
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
set f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k : Iio n => g k.1 k.2)

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, ∀ (n : ℕ), P (u n) (u '' Iio n)
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 : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]

Goal state after: