mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) ⋯).den ∣ q₁.den * q₂.den

Tactic:
normalize_eq

Goal state after:
q₁ q₂ : ℚ
⊢ { num := q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.den ∣
    q₁.den * q₂.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) ⋯).num =
    q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

Tactic:
normalize_eq

Goal state after:
q₁ q₂ : ℚ
⊢ { num := q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.num =
    q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (normalize (q₁.num * q₂.num) (q₁.den * q₂.den) ⋯).den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
normalize_eq

Goal state after:
q₁ q₂ : ℚ
⊢ { num := q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯, reduced := ⋯ }.den =
    q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ ((-Int.ofNat a) ^ 2) ^ b' = Int.ofNat c

Tactic:
neg_pow_two,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ (Int.ofNat a ^ 2) ^ b' = Int.ofNat c
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ ((-Int.ofNat a) ^ 2) ^ b' * -Int.ofNat a = -Int.ofNat c

Tactic:
neg_pow_two,

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (Int.ofNat a ^ 2) ^ b' * -Int.ofNat a = -Int.ofNat c
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
e : R
h : (a + 0) ^ b * Nat.rawCast 1 = e
⊢ a ^ b = e

Tactic:
simp [← h]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
b : ℕ
e : R
h : a ^ b * Nat.rawCast 1 = e
⊢ a ^ b = e + 0

Tactic:
simp [← h]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: k e : ℕ
h : Nat.rawCast 1 = e
⊢ k.rawCast = e * k

Tactic:
simp [← h]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a e : R
h : Nat.rawCast 1 = e
⊢ a ^ 0 = e + 0

Tactic:
simp [← h]

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:
by
  simp_rw [gc.l_iSup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
p : β → Prop
⊢ ⨆ i, f i = (⨆ i, ⨆ (_ : p i), f i) ⊔ ⨆ i, ⨆ (_ : ¬p i), f i

Tactic:
simpa [Classical.em] using @iSup_union _ _ _ f { i | p i } { i | ¬p i }

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ

Tactic:
simp_rw [compl_iUnion]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≤ i), f j = (⨆ j, ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
rw [iSup_split_single _ i]
  -- Squeezed for a ~10x speedup, though it's still reasonably fast unsqueezed.
  simp only [le_refl, iSup_pos, iSup_and', lt_iff_le_and_ne, and_comm, sup_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : BddAbove univ
⊢ BddAbove s

Tactic:
exact hs.mono (subset_univ _)

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

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

pp: 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

Tactic:
· exact hB

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
rw [← le, ← sSup_image, map_inf, map_sSup s, minAx.inf_iSup₂_eq]
    simp_rw [← map_inf]
    exact ((map_sSup _).trans iSup_image).ge

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

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

Tactic:
· exact hB

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : a < sSup s
⊢ ∃ b ∈ s, a < b

Tactic:
contrapose! h

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
h : ∀ b ∈ s, b ≤ a
⊢ sSup s ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
contrapose! h

Goal state after:
case neg.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha : Option.some a ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
⊢ s ⊆ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
intro b hb
          rw [← coe_le_coe]
          exact ha hb

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

Goal state before:
pp: case refine_2
α : 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}
⊢ t ∩ f ⁻¹' s ⊆ t ∩ u

Tactic:
rintro x ⟨xt, xs⟩

Goal state after:
case refine_2
α : 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
xs : x ∈ f ⁻¹' s
⊢ x ∈ t ∩ u
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
haa' : a = a'
⊢ φ a = φ a'

Tactic:
rw [haa']

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ / a = a⁻ᵐ * a⁻ᵐ

Tactic:
← mul_div_div_cancel,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ / a = ?a * a⁻ᵐ / (?a / a⁻ᵐ)

case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ α
Module: Mathlib.Algebra.Order.Group.PosPart

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

Tactic:
← maxDefault,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ max a 1 = maxDefault 1 a
Module: Mathlib.Algebra.Order.Group.PosPart

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

Tactic:
← maxDefault,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = maxDefault 1 a⁻¹
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n m : ℕ
hnm : n ≤ m
⊢ n ! * n ^ (m - n) ≤ m !

Tactic:
calc
    _ ≤ n ! * (n + 1) ^ (m - n) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left n.le_succ _)
    _ ≤ _ := by simpa [hnm] using @Nat.factorial_mul_pow_le_factorial n (m - n)

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

Goal state before:
pp: k n m : ℕ
h : n ≤ m
⊢ n.ascFactorial k ≤ m.ascFactorial k

Tactic:
induction k with

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

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

Tactic:
succ_descFactorial_succ _ k,

Goal state after:
n k : ℕ
⊢ (n + 1 - (k + 1)) * ((n + 1) * n.descFactorial k) = (n + 1) * n.descFactorial k.succ
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ f 1 ≤ f a + f a

Tactic:
← div_self' a

Goal state after:
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ f (a / a) ≤ f a + f a
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
H : ⌊2 * fract x⌋ = 1
⊢ 0 < fract x

Tactic:
contrapose! h

Goal state after:
case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * fract x < 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
let h₀ := Nat.mod_add_div (m : ℕ) (k : ℕ)

Goal state after:
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
⊢ 0 < fract x

Tactic:
replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 0 < fract x + fract x
⊢ 0 < fract x
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
z : ℤ
⊢ ⌊a - ↑z⌋ = ⌊a + ↑(-z)⌋

Tactic:
rw [Int.cast_neg, sub_eq_add_neg]

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
z : ℤ
⊢ ⌈a - ↑z⌉ = ⌈a + ↑(-z)⌉

Tactic:
rw [Int.cast_neg, sub_eq_add_neg]

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

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
have he : ∃ m : ℤ, y ^ m ≤ x := by
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    use -N
    rw [zpow_neg y ↑N, zpow_natCast]
    exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm
  obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  exact ⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : Group G
inst✝ : Torsor G P
v : G
p : P
⊢ (fun x ↦ v⁻¹ • x) ((fun x ↦ v • x) p) = p

Tactic:
by simp [smul_smul]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : Group G
inst✝ : Torsor G P
v : G
p : P
⊢ (fun x ↦ v • x) ((fun x ↦ v⁻¹ • x) p) = p

Tactic:
by simp [smul_smul]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = f a ::ₘ map f (s.erase a)

Tactic:
← map_cons,

Goal state after:
case mp
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
a : α
ha : a ∈ s
⊢ map f s = map f (a ::ₘ s.erase a)
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (replicate n.succ x).dedup = [x]

Tactic:
replicate_dedup n.succ_ne_zero

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ [x] = [x]
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
by_cases h : a ∈ t₁

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : ¬a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by_cases p a <;> by_cases q a <;> simp [*]

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

Goal state before:
pp: case mpr
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a) → (filter P s).card ≤ n

Tactic:
· contrapose!
    exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
x✝ : α
⊢ x✝ ∈ s ∪ (t ∪ u) ↔ x✝ ∈ t ∪ (s ∪ u)

Tactic:
simp only [mem_union, or_left_comm]

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

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

Tactic:
by rw [eq_comm, union_eq_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a✝ b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi✝ : P a✝ s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
⊢ P ({a} ∪ t) {x}

Tactic:
exact union_of singletons (symm hi)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

Tactic:
by rw [inter_comm, insert_inter_of_mem h, inter_comm]

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

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

Tactic:
by
  obtain h | h := (rev i).succ_le_or_le_castSucc p
  · rw [predAbove_of_succ_le _ _ h, rev_pred,
      predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]
  · rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
⊢ Set.range ⇑(natAdd_castLEEmb hmn) = {i | m - n ≤ ↑i}

Tactic:
simp only [natAdd_castLEEmb, Nat.sub_le_iff_le_add]

Goal state after:
n m : ℕ
hmn : n ≤ m
⊢ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) = {i | m ≤ ↑i + n}
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < a ↔ a ≠ 0

Tactic:
← val_pos_iff,

Goal state after:
n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < ↑a ↔ a ≠ 0
Module: Mathlib.Data.Fin.Basic

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

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

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i = i.succ.castPred ⋯
⊢ i = j

Tactic:
← Fin.castSucc_inj,

Goal state after:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.castSucc = (i.succ.castPred ⋯).castSucc
⊢ i = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ k, k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩

Tactic:
simp_rw [← Fin.val_ne_iff]

Goal state after:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f' a₁ = f' a₂
⊢ a₁ = a₂

Tactic:
simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa

Goal state after:
case inr.f_inj
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β := fun a ↦ ↑(f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩))
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f (if h : True then ⟨a₁, ⋯⟩ else ⟨a₀, ha₀⟩) = f (if h : True then ⟨a₂, ⋯⟩ else ⟨a₀, ha₀⟩)
⊢ a₁ = a₂
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = c :: replicate n c

Tactic:
← ofFn_const n

Goal state after:
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = c :: ofFn fun x ↦ c
Module: Mathlib.Data.Finset.Card

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

Tactic:
rw [← card_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

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

Goal state before:
pp: case refine_1.refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ append a b (natAdd m lr) = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))

Tactic:
append_right

Goal state after:
case refine_1.refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ b lr = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.succAbove j).succAbove (j.predAbove i) = i

Tactic:
rw [succAbove_of_le_castSucc _ _ h,
      succ_succAbove_predAbove (Fin.ne_of_lt <| le_castSucc_iff.mp h)]

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

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ append (append a b) c (natAdd (m + n) r) = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))

Tactic:
append_right

Goal state after:
case refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ c r = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: n : ℕ
s : Finset (Fin n)
⊢ #s ≤ n

Tactic:
by
  simpa only [Fintype.card_fin] using s.card_le_univ

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

Goal state before:
pp: n : ℕ
β : Sort u_2
q : Fin (n + 2) → β
⊢ tail (init q) = init (tail q)

Tactic:
ext i
  simp [tail, init]

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

Goal state before:
pp: case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
this : ∃ h, l'[f 0] = hd
⊢ hd :: tl <+ l'

Tactic:
obtain ⟨w, h⟩ := this

Goal state after:
case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
⊢ hd :: tl <+ l'
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ h.toFinset.Nontrivial ↔ s.Nontrivial

Tactic:
rw [Finset.Nontrivial, h.coe_toFinset]

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

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j : Fin (n + 1)
⊢ i.insertNth a f j.rev = i.rev.insertNth a (f ∘ rev) j

Tactic:
by
  induction j using Fin.succAboveCases
  · exact rev i
  · simp
  · simp [rev_succAbove]

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

Goal state before:
pp: case mpr.refine_2
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ix)

Tactic:
rintro ⟨⟨_ | i⟩, hi⟩

Goal state after:
case mpr.refine_2.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨0, hi⟩ = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨0, hi⟩)

case mpr.refine_2.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
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)