mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 1 / a ^ n ≤ 1 / a ^ m

Tactic:
by
  refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn) <;>
    exact pow_pos (zero_lt_one.trans_le a1) _

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

Goal state before:
pp: case mp.cons
α : Type u_1
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x1 x2 ↦ x1 = x2) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝

Tactic:
simp only [*]

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₁) []

pp: case cons.cons
α : 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₂
b : β
l₂ : List β
h₁ : (a :: l₁).length = (b :: l₂).length
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)

Tactic:
· simp at h₁

Goal state after:
case cons.cons
α : 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₂
b : β
l₂ : List β
h₁ : (a :: l₁).length = (b :: l₂).length
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
n✝ : ℕ
⊢ Forall₂ R (drop (n✝ + 1) []) (drop (n✝ + 1) [])

Tactic:
simp only [Forall₂.nil, drop]

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

Goal state before:
pp: case swap.cons.cons
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
b✝¹ : β
h₁ : r a₁ b✝¹
b✝ : β
l₂✝ : List β
h₂ : r a₂ b✝
h₁₂ : Forall₂ r h₂₃ l₂✝
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) (b✝¹ :: b✝ :: l₂✝)

Tactic:
exact ⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
P : α → Prop
inst✝ : DecidablePred P
l : List α
a : α
⊢ count a l = count a (filter (fun b ↦ decide (P b)) l) + count a (filter (fun x ↦ decide ¬P x) l)

Tactic:
unfold count
  convert countP_eq_countP_filter_add l _ P
  simp only [decide_not]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
p : l₁ ~ l₂
b : β
⊢ foldr f b l₁ = foldr f b l₂

Tactic:
induction p using Perm.recOnSwap' generalizing b with
  | nil => rfl
  | cons _ _ r => simp [r b]
  | swap' _ _ _ r => simp only [foldr_cons]; rw [lcomm.left_comm, r b]
  | trans _ _ r₁ r₂ => exact Eq.trans (r₁ b) (r₂ b)

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Bijective (map f) ↔ Bijective f

Tactic:
by
  simp_rw [Function.Bijective, map_injective_iff, map_surjective_iff]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
l : List α
⊢ filterMap f l = flatMap (fun a ↦ (f a).toList) l

Tactic:
induction l with | nil => ?_ | cons a l ih => ?_ <;> simp [filterMap_cons]

Goal state after:
case cons
α : Type u
β : Type v
f : α → Option β
a : α
l : List α
ih : filterMap f l = flatMap (fun a ↦ (f a).toList) l
⊢ (match f a with
    | none => filterMap f l
    | some b => b :: filterMap f l) =
    (f a).toList ++ flatMap (fun a ↦ (f a).toList) l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map ((fun a ↦ ↑a) ∘ Subtype.map id ⋯) (filter p l).attach

Tactic:
comp_def,

Goal state after:
α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun x ↦ ↑(Subtype.map id ⋯ x)) (filter p l).attach
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ a ∈ t

Tactic:
hf a a' (hs a ha) (ht a' ha') ha''.symm

Goal state after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
a : α
ha : a ∈ s
a' : α
ha' : a' ∈ t
ha'' : f a' ⋯ = f a ⋯
⊢ a' ∈ t
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ a ^ ↑n.succ = a ^ ↑n * a

Tactic:
ext; apply Field.zpow_succ'

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a⁻¹ * (b * a) = b

Tactic:
by
  rw [← mul_assoc, h.inv_mul_cancel]

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
by
  rw [← Int.cast_natCast, cast_intCast, Int.cast_natCast]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
⊢ rhs ≥ x

Tactic:
have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
x : α✝
hr : rhs < x
hl : x < lhs
this : ∀ (a : α), ∃ b, x < g a b
⊢ rhs ≥ x
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
⊢ ⨆ i ∈ s ∩ t, f i = (⨆ i ∈ s, f i) ⊓ ⨆ i ∈ t, f i

Tactic:
rw [biSup_inf_biSup]
  refine le_antisymm
    (iSup₂_le fun i ⟨his, hit⟩ ↦ le_iSup₂_of_le ⟨i, i⟩ ⟨his, hit⟩ (le_inf le_rfl le_rfl))
    (iSup₂_le fun ⟨i, j⟩ ⟨his, hjs⟩ ↦ ?_)
  by_cases hij : i = j
  · exact le_iSup₂_of_le i ⟨his, hij ▸ hjs⟩ inf_le_left
  · simp [h hij |>.eq_bot]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
⊢ sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a

Tactic:
by
  have : OrderBot α := WellFoundedLT.toOrderBot α
  constructor
  · intro rfl
    exact ⟨csInf_mem hs, fun _ ↦ csInf_le (OrderBot.bddBelow s)⟩
  · intro ⟨hn, hle⟩
    exact le_antisymm (csInf_le (OrderBot.bddBelow s) hn) (le_csInf hs hle)

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

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
hb₂ : ¬∃ a₂, e a₂ = b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Tactic:
simpa only [onFun, extend_apply' _ _ _ hb₂] using! disjoint_bot_right

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

Goal state before:
pp: case inl.inl.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b

Tactic:
exact le_of_lt ‹_›

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

Tactic:
exact le_of_lt ‹_›

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

Goal state before:
pp: case inl.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b

Tactic:
exact le_of_lt ‹_›

Goal state after:
case inl.inr.a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a

Tactic:
exact le_of_lt ‹_›

Goal state after:
case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨i, _hi, j, _hj, h⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h

Goal state after:
α : Type u_1
ι : Type u_4
f : ι → Set α
h✝ : ¬univ.Pairwise (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑e '' s).OrdConnected

Tactic:
(e : α ≃o β).image_eq_preimage_symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑(↑e).symm ⁻¹' s).OrdConnected
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'
⊢ IsAntichain r' (⇑φ '' s)

Tactic:
intro b hb b' hb' h₁ h₂
  rw [Set.mem_image] at hb hb'
  obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
  exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
a : α
ha : a ≠ 0
lt : 0 < a
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
exact ⟨0, ⟨a, lt.le⟩, Subtype.coe_ne_coe.mp ha.symm⟩

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)

Tactic:
exact (Subtype.mono_coe (· ∈ s)).le_csSup_image hct ⟨B, hB⟩

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
g : M → N
hg : g 1 = 1
f : ι → M
x : ι
h : f x = 1
⊢ (g ∘ f) x = 1

Tactic:
simp only [(· ∘ ·), *]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ (a⁺ᵐ / a⁻ᵐ)⁻¹ = a⁻¹

Tactic:
oneLePart_div_leOnePart

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁻¹ = a⁻¹
Module: Mathlib.Algebra.Order.Group.PosPart

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

Tactic:
oneLePart_div_leOnePart

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ * a = |a|ₘ * a
Module: Mathlib.Algebra.Order.Group.PosPart

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

Tactic:
oneLePart_div_leOnePart

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ |a|ₘ / a = |a|ₘ / a
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
← succ_add_eq_add_succ,

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

Goal state before:
pp: a b : ℕ+
h : b < a
⊢ a - b + b = a

Tactic:
by
  rw [add_comm, add_sub_of_lt h]

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Tactic:
obtain rfl | ha := ha.eq_or_lt

Goal state after:
case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
ha : 1 ≤ 1
⊢ ⌈↑⌈(1 - 1)⁻¹⌉ / 1⌉ = ⌈(1 - 1)⁻¹⌉

case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 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.den - q.num * ⌊q_inv⌋ < q.num
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num

Tactic:
have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using! tmp
    rwa [this]

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

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
h : p₁ /ₛ p₂ = 1
⊢ p₁ = p₂

Tactic:
by
  rw [← sdiv_smul p₁ p₂, h, one_smul]

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

Goal state before:
pp: case h.left
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
sublist : w <+ map f l₂
x : List α
perm : map f x ~ map f l₁
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁

Tactic:
exact (map_perm_map_iff hf).mp perm

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

Goal state before:
pp: case mpr.inr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
left✝ : a ≠ b
cs : Multiset α
eq₁ : as = b ::ₘ cs
eq₂ : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs

Tactic:
simp [*, cons_swap a b]

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

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.pmap (fun a_1 h ↦ ⟨↑⟨a_1, h⟩, ⋯⟩) l ⋯

Tactic:
exact List.pmap_congr_left _ fun _ _ _ _ => Subtype.ext rfl

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ x :: xs ∪ ys = (x :: xs).dedup ++ ys

Tactic:
cons_union

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ count a (dedup (Quot.mk (⇑(isSetoid α)) x✝)) = if a ∈ Quot.mk (⇑(isSetoid α)) x✝ then 1 else 0

Tactic:
simp only [quot_mk_to_coe'', coe_dedup, mem_coe, coe_count]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ List.count a x✝.dedup = if a ∈ x✝ then 1 else 0
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ (List.take n xs).Disjoint (List.drop (n + m) xs)

Tactic:
exact disjoint_take_drop h₂ this

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

Goal state before:
pp: α : Type u_1
s✝ : List α
a : α
t : List α
o : s✝ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝
s r : List α
hr : r ∈ t.inits
hs : a :: r = s
⊢ s <+: a :: t

Tactic:
let ⟨s, ht⟩ := (mem_inits _ _).1 hr
        rw [← hs, ← ht]; exact ⟨s, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ≤ t.ndinter u ↔ s ≤ t ∧ s ⊆ u

Tactic:
by
  simp [ndinter, le_filter, subset_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ ↑s = Set.univ ↔ s = univ

Tactic:
← coe_univ,

Goal state after:
α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ ↑s = ↑univ ↔ s = univ
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ s = t

Tactic:
← insert_erase hs,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ insert a (s.erase a) = t
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ finsetEquivSet.symm s = s.toFinset

Tactic:
simp [finsetEquivSet]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image (f ∘ g) s = image (g' ∘ f') s

Tactic:
comp_def,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image (fun x ↦ f (g x)) s = image (fun x ↦ g' (f' x)) s
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
  | zero => exact m.zero_le
  | succ n ihn =>
    obtain ⟨e⟩ := h
    rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (Nonempty.map e inferInstance)).ne'
      with ⟨m, rfl⟩
    refine Nat.succ_le_succ <| ihn ⟨?_⟩
    refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩
    simpa only [pred_inj, EmbeddingLike.apply_eq_iff_eq, succ_inj] using h

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
⊢ a < last n ↔ a ≠ last n

Tactic:
by
  simp [Fin.lt_iff_le_and_ne, le_last]

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

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

Tactic:
rw [← val_fin_lt, val_zero]

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

Goal state before:
pp: n : ℕ
⊢ Nontrivial (Fin n) ↔ 2 ≤ n

Tactic:
simp [← not_subsingleton_iff_nontrivial, subsingleton_iff_le_one]; lia

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ ≤ b ↔ a < b

Tactic:
succ_castPred_eq_castPred_succ ha,

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ a.succ.castPred ⋯ ≤ b ↔ a < b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ b < (a.castPred ha).succ ↔ b ≤ a

Tactic:
succ_castPred_eq_castPred_succ ha,

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ b < a.succ.castPred ⋯ ↔ b ≤ a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ (p.pred ⋯).predAbove i = i.castPred ⋯

Tactic:
predAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h)

Goal state after:
n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ i.castPred ⋯ = i.castPred ⋯
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ 1

Tactic:
← card_singleton x

Goal state after:
case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ #{x}
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case pos
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : j < l.length
⊢ i + l'.length < ↑(f ⟨j, hj⟩)

pp: case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length

Tactic:
· exact absurd (h.trans hj) hi

Goal state after:
case neg
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
i j : ℕ
h : i < j
hi : ¬i < l.length
hj : ¬j < l.length
⊢ i + l'.length < j + l'.length
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)
j : Fin n
⊢ p j = removeNth 0 (cons x fun j ↦ cast ⋯ (p j)) j

Tactic:
convert! (cons_succ x p j).symm

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

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
⊢ motive s hs

Tactic:
lift s to Finset α using hs

Goal state after:
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
s : Finset α
hs : (↑s).Finite
⊢ motive (↑s) hs
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
hba : r b a
⊢ a :: orderedInsert r x as <+ x :: b :: bs

Tactic:
exact absurd (trans_of _ ‹r x b› hba) hr

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l c : List α
hs : Pairwise r c
d : List α
hc : d ~ c
hd : d <+ l
⊢ c <+ insertionSort r l

Tactic:
induction l generalizing c d with

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

Goal state before:
pp: case refine_2.cons
α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r l₁ l₂
⊢ r a a ∨ a = a ∧ Lex r l₁ l₂

Tactic:
exact Or.inr ⟨rfl, h⟩

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a : M
⊢ {a}.prod = a

Tactic:
by
  simp only [mul_one, prod_cons, ← cons_zero, prod_zero]

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

Goal state before:
pp: G : Type u_7
inst✝ : Group G
a : G
l : List G
hl : (a :: l).prod = 1
n : ℕ
⊢ ((a :: l).rotate n).prod = 1

Tactic:
by
    have : n % List.length (a :: l) ≤ List.length (a :: l) := le_of_lt (Nat.mod_lt _ (by simp))
    rw [← List.take_append_drop (n % List.length (a :: l)) (a :: l)] at hl
    rw [← rotate_mod, rotate_eq_drop_append_take this, List.prod_append, mul_eq_one_iff_inv_eq,
      ← one_mul (List.prod _)⁻¹, ← hl, List.prod_append, mul_assoc, mul_inv_cancel, mul_one]

Goal state after: