mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t

Tactic:
rw [(_ : t \ s ∪ s ∩ t = t)]

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ t \ s ∪ s ∩ t = t
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = Ioo a b

Tactic:
by rw [Icc_eq_empty h, Ioo_eq_empty (mt le_of_lt h)]

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

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a < b
⊢ a * (1 / b) < 1

Tactic:
← div_eq_mul_one_div,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a < b
⊢ a / b < 1
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -(↑num✝ * ⅟↑denom✝) = ↑num✝.neg * ⅟↑denom✝

Tactic:
by rw [← neg_mul, ← Int.cast_neg]; rfl

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (ts.length + (t :: is).length, ts.length)
    ((t :: ts).length + is.length, (t :: ts).length)

pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (is.length + [].length, is.length)
    ((t :: ts).length + is.length, (t :: ts).length)

Tactic:
all_goals (simp_wf; grind)

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
⊢ b * (1 / a) ≤ 1

Tactic:
← div_eq_mul_one_div,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
⊢ b / a ≤ 1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a < b
⊢ b * (1 / a) < 1

Tactic:
← div_eq_mul_one_div,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a < b
⊢ b / a < 1
Module: Mathlib.Data.List.InsertIdx

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

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

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

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
ih :
  (map (fun a ↦ if p a then f a else g a) xs).prod =
    (map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

Tactic:
clear ih

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
ih : (map (fun x ↦ if x = a then f x else g x) xs).prod = (f a / g a) ^ count a xs * (map g xs).prod
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)

Tactic:
clear ih

Goal state after:
case cons
G : Type u_7
inst✝¹ : CommGroup G
A : Type u_8
inst✝ : DecidableEq A
f g : A → G
a x : A
xs : List A
⊢ (if x = a then f x else g x) * ((f a / g a) ^ count a xs * (map g xs).prod) =
    (f a / g a) ^ (count a xs + if (x == a) = true then 1 else 0) * (g x * (map g xs).prod)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
⊢ [a].alternatingProd = a * [].alternatingProd⁻¹

Tactic:
rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]

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

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ (mkRat (↑q.den) q.num).num.natAbs = q.den

Tactic:
← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq),

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ { num := ↑q.den, den := q.num, den_nz := ⋯, reduced := ?m.26 }.num.natAbs = q.den

q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
⊢ OfScientific.ofScientific m b d = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))

Tactic:
rw [NNRatCast.toOfScientific_def]

Goal state after:
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (sInf s).down = ⨅ a ∈ s, a.down

Tactic:
by rw [sInf_eq_iInf', down_iInf, iInf_subtype'']

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
κ : ι → Sort u_1
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : (i : ι) → κ i → α
⊢ l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)

Tactic:
gc.l_iSup

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
s : Set α
H : ¬BddAbove s
⊢ sSup s = sSup ∅

Tactic:
by
    rw [BddAbove] at H
    simp [sSup, H, bot_unique (WellFounded.min_le _ (mem_univ _))]

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

Goal state before:
pp: β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
have p : x ∈ ⊤ := Set.mem_univ x
  rw [← w, Set.mem_iUnion] at p
  simpa using p

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ f (sSup s) = sSup (⇑f.symm ⁻¹' s)

Tactic:
rw [map_sSup, ← sSup_image, f.image_eq_preimage_symm]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
f : ι → α
a : α
⊢ (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
by
  rw [iSup, sSup_inf_eq, iSup_range]

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

Goal state before:
pp: α : 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
⊢ BddAbove s

Tactic:
rcases B with hB | ⟨b, hb⟩

Goal state after:
case inl
α : 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
hB : BddAbove s
⊢ BddAbove s

case inr
α : 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 : α
hb : b ∈ upperBounds t
⊢ BddAbove s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ none ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))

Tactic:
exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : Set ι
f : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : s.PairwiseDisjoint f
x y : ↑s
hxy : g x ≠ g y
⊢ (Disjoint on f) (g x) (g y)

Tactic:
exact ((ht x.2 y.2) fun h => hxy <| congr_arg g <| Subtype.ext h).mono (hg x) (hg y)

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
change ¬ ∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h

Goal state after:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ∀ (t : Set α), t ⊆ f i → t ⊆ f j → t ⊆ ⊥
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
i : SetLike A B
inst✝¹ : LE A
inst✝ : OrderTop A
s : A
hs : s ≠ ⊤
h_top : ↑⊤ = Set.univ
⊢ ∃ b, ¬b ∈ s

Tactic:
simpa [-SetLike.coe_set_eq, SetLike.ext'_iff, h_top, Set.ne_univ_iff_exists_notMem] using hs

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddAbove t
⊢ sSup t = default

Tactic:
by
  simp [sSup, ht]

Goal state after:
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✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
have h := Int.cast_mono (R := α) <| of_decide_eq_true 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✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1

Tactic:
rw [leOnePart_def, ← maxDefault, ← sup_eq_maxDefault]

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = (fun x1 x2 ↦ max x1 x2) 1 a⁻¹
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
        Nat.add_le_add_iff_right]

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

Goal state before:
pp: case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = (n - m)! * n.descFactorial m

Tactic:
factorial_mul_descFactorial hmn,

Goal state after:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - m)! * ((n - k).descFactorial (m - k) * n.descFactorial k) = 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
n : ℕ
a : R
⊢ ⌊↑n + a⌋ = ↑n + ⌊a⌋

Tactic:
rw [← Int.cast_natCast, floor_intCast_add]

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
n : ℕ
a : R
⊢ fract (↑n + a) = fract a

Tactic:
rw [add_comm, fract_add_natCast]

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

Goal state before:
pp: case refine_1
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ y ^ (n + 1) < x

pp: case refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n

Tactic:
· rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n

Goal state after:
case refine_2
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ x ≤ y ^ n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inr.inr.inl
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₁ : a < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
refine ⟨0, ?_⟩
        rw [zpow_zero]
        exact ⟨ha₁, hb₁⟩

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α)) _l) = card (Quot.mk (⇑(isSetoid α)) _l) ↔
    ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → p a

Tactic:
by simp [List.countP_eq_length]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
l : List α
f : α → β
hf : Function.Injective f
x : α
⊢ count (f x) (map f l) = count x l

Tactic:
by
  simp only [count, countP_map]
  unfold Function.comp
  simp only [hf.beq_eq]

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

Goal state before:
pp: case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : m.card = card 0
⊢ card 0 = 0

Tactic:
card_zero

Goal state after:
case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : m.card = card 0
⊢ 0 = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = (a ::ₘ t).card
⊢ Rel r m (a ::ₘ t)

Tactic:
rw [card_cons] at hc

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = t.card + 1
⊢ Rel r m (a ::ₘ t)
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ List.take n xs ~ List.filter (fun a ↦ elem a (List.take n xs)) xs

Tactic:
conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
ih : map f (filter p s) = filterMap (fun a ↦ if p a then some (f a) else none) s
⊢ map (fun x ↦ f x) (if p a then {a} else 0) + filterMap (fun a ↦ if p a then some (f a) else none) s =
    (if p a then some {f a} else none).getD 0 + filterMap (fun a ↦ if p a then some (f a) else none) s

Tactic:
clear ih

Goal state after:
case cons
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ map (fun x ↦ f x) (if p a then {a} else 0) + filterMap (fun a ↦ if p a then some (f a) else none) s =
    (if p a then some {f a} else none).getD 0 + filterMap (fun a ↦ if p a then some (f a) else none) s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ map f (filter p s) = filterMap (fun a ↦ if p a then some (f a) else none) s

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons a s ih =>
    simp only [filter_cons, map_add, ih, filterMap_cons, Option.map_if]; clear ih; congr
    split_ifs <;> simp

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ 0 = card 0

Tactic:
card_zero

Goal state after:
case refine_1
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ 0 = 0
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
this : count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card
⊢ count (f x) (map f s) = count x s

Tactic:
by
    rw [count, countP_map, ← this]
    exact count_filter_of_pos <| rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
by_cases h : a ∈ s <;> simp [h]

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
h : ¬a ∈ s
ht : ndinsert a s = a ::ₘ s
⊢ (a ::ₘ s).attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
simp [attach_cons, h]

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:
by rw [eq_comm, union_eq_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) ↔ s.Nontrivial

Tactic:
refine ⟨?_, fun hs ↦ hs.exists_ne a⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) → s.Nontrivial
Module: Mathlib.Data.Finset.Basic

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

Tactic:
rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ s ⇨ t ↔ a ∈ s → a ∈ t

Tactic:
simp [himp_eq, imp_iff_or_not]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (union s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩

Tactic:
by
  simp [Equiv.symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (union s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩

Tactic:
by
  simp [Equiv.symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ s
hi' : i ∈ s.disjUnion t h
⊢ (disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩

Tactic:
by
  simp [Equiv.symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
i : α
hi : i ∈ t
hi' : i ∈ s.disjUnion t h
⊢ (disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩

Tactic:
by
  simp [Equiv.symm_apply_eq]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.toList.length = #s

Tactic:
rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]

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
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ image f s = t

Tactic:
have : s.image f ⊆ t := hf.finsetImage_subset

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
this : image f s ⊆ t
⊢ image f s = t
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
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
⊢ Set.SurjOn f ↑s ↑t

Tactic:
classical
  suffices s.image f = t by rw [Finset.surjOn_iff_subset_image, this]
  have : s.image f ⊆ t := hf.finsetImage_subset
  exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ card ↑sᶜ = card α - card ↑s

Tactic:
by
  classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]

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

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

Tactic:
rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

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

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

Tactic:
rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
⊢ ↥hs.toFinset = ↑s

Tactic:
by
  rw [← Finset.coe_sort_coe _, hs.coe_toFinset]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ insertNth 0 x p = cons x fun j ↦ cast ⋯ (p j)

Tactic:
by
  refine insertNth_eq_iff.2 ⟨by simp, ?_⟩
  ext j
  convert! (cons_succ x p j).symm

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

Goal state before:
pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length, Nat.le_zero] at hi hj
          simp [hi, hj]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)

Tactic:
simp_rw [@and_comm ((_ : Set _) ⊆ _), and_assoc, exists_finite_iff_finset, @and_comm (p _),
    Finset.subset_set_image_iff]

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, (∃ s', ↑s' ⊆ s ∧ Finset.image f s' = s_1) ∧ p ↑s_1) ↔ ∃ s_1, ↑s_1 ⊆ s ∧ p (f '' ↑s_1)