mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
⊢ DenselyOrdered α ↔ Nontrivial αˣ ∧ DenselyOrdered αˣ

Tactic:
refine ⟨fun H ↦ ⟨?_, ?_⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
  · obtain ⟨x, hx, hx'⟩ := exists_between (zero_lt_one' α)
    exact ⟨Units.mk0 x hx.ne', 1, by simpa [Units.ext_iff] using hx'.ne⟩
  · refine ⟨fun x y h ↦ ?_⟩
    obtain ⟨z, hz⟩ := exists_between (Units.val_lt_val.mpr h)
    refine ⟨Units.mk0 z (ne_zero_of_lt hz.1), by simp [← Units.val_lt_val, hz]⟩
  · refine ⟨fun x y h ↦ ?_⟩
    lift y to αˣ using (ne_zero_of_lt h).isUnit
    obtain rfl | hx := eq_zero_or_pos x
    · obtain ⟨z, hz⟩ := exists_one_lt' (α := αˣ)
      exact ⟨(y * z⁻¹ : αˣ), by simp, Units.val_lt_val.mpr <| by simp [hz]⟩
    · lift x to αˣ using hx.ne'.isUnit
      obtain ⟨z, hz, hz'⟩ := H₂.dense x y (Units.val_lt_val.mpr h)
      exact ⟨z, by simp [hz, hz']⟩

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

Goal state before:
pp: x : ℤ
⊢ fract x = 0 x

Tactic:
by simp [fract]

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌊a⌋ ≤ z ↔ a < ↑z + 1

Tactic:
by rw [← lt_add_one_iff, floor_lt]; norm_cast

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n : α
⊢ f m ≤ g n

Tactic:
obtain ⟨k, hkm, hkn⟩ := exists_ge_ge m n
  calc
    f m ≤ f k := hf hkm
    _ ≤ g k := h _
    _ ≤ g n := hg hkn

Goal state after:
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
h : a * c = b * c
⊢ a = b

Tactic:
simpa using congr_arg (· * ⅟c) h

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
⊢ Subsingleton (FloorSemiring R)

Tactic:
refine ⟨fun H₁ H₂ => ?_⟩

Goal state after:
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
⊢ H₁ = H₂
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ (b : β), b ∈ t → (fun a ↦ f a b) '' s ⊆ u

Tactic:
simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_comm α]

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

Goal state before:
pp: γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
⊢ j = i ∨ Iio i = Iic j

Tactic:
by
  rcases eq_or_lt_of_le (le_of_isLUB_Iio i hj) with hj_eq_i | hj_lt_i
  · exact Or.inl hj_eq_i
  · right
    exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

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

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

Tactic:
by
  simpa [← map_eq_flatMap] using flatMap_append_perm l (fun x => [f x]) g

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

Goal state before:
pp: α : Type u
a b : α
l : List α
c : α
hc : c ∈ (a :: b :: l).getLast?
⊢ (a :: b :: l).dropLast ++ [c] = a :: b :: l

Tactic:
by
    rw [getLast?_cons_cons] at hc
    rw [dropLast_cons_cons, cons_append, dropLast_append_getLast? _ hc]

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

Goal state before:
pp: α : Type u
k : ℕ
l : List α
h : k ≠ 0
hk : k < l.length
⊢ l[k] ∈ l.tail

Tactic:
by
  cases l <;> grind

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l.dropLast
⊢ idxOf a l + 1 < l.length

Tactic:
by
  have := idxOf_lt_length_of_mem ha
  grind [IsPrefix.idxOf_eq_of_mem]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ q.num ≤ ↑q.den ↔ q ≤ 1

Tactic:
simp [Rat.le_iff]

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

Goal state before:
pp: case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq

Goal state after:
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ 0

Tactic:
exact ⟨0, by simp⟩

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

Goal state before:
pp: m : ℕ
⊢ ↑(m + 1).toPNat' = if 0 < m + 1 then m + 1 else 1

Tactic:
rw [if_pos (succ_pos m)]

Goal state after:
m : ℕ
⊢ ↑(m + 1).toPNat' = m + 1
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c ∧ b = d

Tactic:
apply And.intro

Goal state after:
case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c

case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : a.natAbs.Coprime b.natAbs
h2 : c.natAbs.Coprime d.natAbs
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
inst✝ : a.AtLeastTwo
⊢ (OfNat.ofNat a)⁻¹.num = 1

Tactic:
have : 2 ≤ a := Nat.AtLeastTwo.prop
  simp only [num_inv, num_ofNat, den_ofNat, Nat.cast_one, mul_one, Int.sign_eq_one_iff_pos,
    gt_iff_lt]
  change 0 < (a : ℤ)
  lia

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

Goal state before:
pp: h : nil ≠ nil
⊢ node () nil.left nil.right = nil

Tactic:
by trivial

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

Goal state before:
pp: R : Type u_2
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : SMul R α
r : R
a b t c : α
x✝² : a = b
x✝¹ : ∀ (x : α), r • x = t * x
x✝ : t * b = c
⊢ r • a = c

Tactic:
subst_vars
  simp [*]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : IsLUB s a₀
hb₀ : IsLUB t b₀
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
simp_rw [isLUB_iff_le_iff, mem_upperBounds] at ha₀ hb₀
  simp_rw [isLUB_iff_le_iff, mem_upperBounds, forall_mem_image2, (h₂ _).le_iff_le,
    ← hb₀, ← (h₂ _).le_iff_le, (h₁ _).le_iff_le, ← ha₀, forall_true_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j = ⨆ i, f i

Tactic:
by
  apply le_antisymm
  · exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _
  · refine iSup_le fun j ↦ ?_
    obtain ⟨i, jlt⟩ := exists_lt j
    exact le_iSup_of_le i (le_iSup₂_of_le j jlt le_rfl)

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
y : β
hy : f i y = ⟨x, hx⟩
⊢ ∃ i, x ∈ range fun x ↦ ↑(f x i)

Tactic:
exact ⟨y, i, congr_arg Subtype.val hy⟩

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ Injective fun a ↦ ↑a

pp: case hnc
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ⊤ ∉ (fun a ↦ ↑a) '' s

Tactic:
· exact Option.some_injective _

Goal state after:
case hnc
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ⊤ ∉ (fun a ↦ ↑a) '' s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : (fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s)
⊢ ↑(sInf s) = ⊤

pp: case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s))
⊢ ↑(sInf s) = ↑(sInf ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s))

Tactic:
· rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim

Goal state after:
case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s))
⊢ ↑(sInf s) = ↑(sInf ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f b

Tactic:
have : Icc a b = Icc (α := αᵒᵈ) (toDual b) (toDual a) := by rw [Icc_toDual]; rfl
  rw [this] at h' ⊢
  exact h'.dual_left.sInf_image_Icc (α := αᵒᵈ) hab

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y

Tactic:
suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
    refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)
    rw [h]
    exact mem_image_of_mem _ hy.2

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a b : α
⊢ (a ⊔ b)⁺ᵐ = a⁺ᵐ ⊔ b⁺ᵐ

Tactic:
simp [oneLePart, sup_sup_distrib_right]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : x ∈ {i}
⊢ x ∈ mulSupport (mulSingle i a)

Tactic:
rwa [mem_mulSupport, hx, mulSingle_eq_same]

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

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2

pp: case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
· rw [Int.floor_eq_zero_iff.mpr, Int.floor_eq_zero_iff.mpr]
    · simp
    · simp [h]
    · suffices fract x < 1 by simpa
      refine lt_of_le_of_lt ?_ h
      apply le_mul_of_one_le_left <;> simp

Goal state after:
case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2
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
⊢ fract 1 = 0

Tactic:
by simp [fract]

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 : ℕ
⊢ fract ↑n = 0

Tactic:
by simp [fract]

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 b : R
⊢ (∃ z, a - b = ↑z) → fract a = fract b

Tactic:
rintro ⟨z, hz⟩
    refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩
    rw [eq_add_of_sub_eq hz, add_comm, Int.cast_add]
    exact add_sub_sub_cancel _ _ _

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
a : R
inst✝ : IsOrderedRing R
z : ℤ
⊢ z ≤ ⌊-a⌋ ↔ z ≤ -⌈a⌉

Tactic:
rw [le_neg, ceil_le, le_floor, Int.cast_neg, le_neg]

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

Goal state before:
pp: n : ℤ
d : ℕ
⊢ n % ↑d = n - ↑d * ⌊↑n / ↑d⌋

Tactic:
Int.emod_def,

Goal state after:
n : ℤ
d : ℕ
⊢ n - ↑d * (n / ↑d) = n - ↑d * ⌊↑n / ↑d⌋
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
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
this : q_inv.num = ↑q.den ∧ q_inv.den = q.num.natAbs
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num

Tactic:
q_inv_eq,

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

Goal state before:
pp: R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
⊢ Subsingleton (FloorRing R)

Tactic:
refine ⟨fun H₁ H₂ => ?_⟩

Goal state after:
R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
H₁ H₂ : FloorRing R
⊢ H₁ = H₂
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case mpr
α : Type u_1
l : List α
a : α
⊢ l = [] ∨ l = [a] → l <+~ [a]

Tactic:
rintro (rfl | rfl)
    exacts [nil_subperm, Subperm.refl _]

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

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

Tactic:
rw [range_list_map, Subtype.range_coe]

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

Goal state before:
pp: α : Type u
l : List α
hne : l ≠ []
hnd : l.Nodup
⊢ l.head hne = l.getLast hne ↔ ∃ x, l = [x]

Tactic:
by
  cases l <;> grind

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

Goal state before:
pp: case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a ∈ map f s

Tactic:
ha,

Goal state after:
case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
a : α
ha : s = {a}
⊢ f a ∈ map f {a}
Module: Mathlib.Data.List.Dedup

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

Tactic:
· rw [dedup_cons_of_notMem hx, insert_of_not_mem, ih h.2, cons_append]
      rw [mem_union_iff, not_or]
      exact ⟨hx, h.1⟩

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.take n' xs.reverse ~ ys ∩ List.take n' xs.reverse

Tactic:
apply Perm.take_inter _ _ h'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ xs.reverse ~ ys
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 : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)

Tactic:
exact ⟨s, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndinter t = s

Tactic:
by
  induction s, t using Quot.induction_on₂
  rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ (filter p s).Nonempty ↔ ∃ a, a ∈ s ∧ p a

Tactic:
simp only [nonempty_iff_ne_empty, Ne, filter_eq_empty_iff, Classical.not_not, not_forall,
    exists_prop]

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

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

Tactic:
exact ⟨notMem_erase _ _, hst⟩

Goal state after:
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)
⊢ a ∉ t.erase a ∧ Disjoint s (t.erase a)

Tactic:
exact ⟨notMem_erase _ _, hst⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
by
  simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]

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

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

Tactic:
simp [Fin.lt_iff_le_and_ne, le_last]

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

Goal state before:
pp: n m : ℕ
a b : Fin n
ha : ↑a < m
hab : b ≤ a
⊢ ↑(a - b) < m

Tactic:
rw [Fin.sub_val_of_le hab]

Goal state after:
n m : ℕ
a b : Fin n
ha : ↑a < m
hab : b ≤ a
⊢ ↑a - ↑b < m
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

Tactic:
exact pred_le _

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

Goal state after:
n : ℕ
u v : Fin n
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v

pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v - ↑n

Tactic:
· rw [natCast_emod, Int.emod_eq_of_lt] <;> lia

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v - ↑n
Module: Mathlib.Data.Fin.Basic

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

Tactic:
Fin.val_add,

Goal state after:
n : ℕ
a b : Fin n
⊢ (↑a + ↑b) % n = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ #s = #t

Tactic:
refine card_nbij' e e.symm ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.MapsTo ⇑e ↑s ↑t

case refine_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.MapsTo ⇑e.symm ↑t ↑s

case refine_3
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.LeftInvOn ⇑e.symm ⇑e ↑s

case refine_4
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.RightInvOn ⇑e.symm ⇑e ↑t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
by
  grind [card_le_one]

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m + n = m

Tactic:
by rw [hv, Nat.add_zero]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card α = card β

Tactic:
by
  rw [← ofEquiv_card f]; congr!

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
h : Fintype { _a // True }
⊢ card { _a // True } = card α

Tactic:
apply Fintype.card_of_subtype
  simp

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

Goal state before:
pp: case cons_mem
α : Type u_1
l : List α
x y : α
l✝ : List α
h : x ∈ l✝
⊢ x :: l✝ ≠ [y]

Tactic:
| cons_mem h =>

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

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ card { i // ↑i < m } = m

Tactic:
conv_rhs => rw [← Fintype.card_fin m]
  apply Fintype.card_congr
  exact { toFun := fun ⟨⟨i, _⟩, hi⟩ ↦ ⟨i, hi⟩
          invFun := fun ⟨i, hi⟩ ↦ ⟨⟨i, lt_of_lt_of_le hi h⟩, hi⟩ }

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

Goal state before:
pp: case refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) (last n) = snoc (f ∘ natAdd m) a (last n)

Tactic:
simp only [Function.comp_apply]

Goal state after:
case refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (natAdd m (last n)) = snoc (f ∘ natAdd m) a (last n)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ orderedInsert r a (b :: m) = a :: b :: m

Tactic:
orderedInsert_cons_of_le

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ a :: b :: m = a :: b :: m

case cons.h
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ r a b
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)

Tactic:
simp only [Function.comp_apply]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
hi : Std.IdempotentOp op
x : γ
xs : Finset γ
hx : x ∉ xs
ih : fold op b f (image g xs) = fold op b (f ∘ g) xs
this : DecidableEq γ
⊢ op (f (g x)) (fold op b (f ∘ g) xs) = op ((f ∘ g) x) (fold op b (f ∘ g) xs)

Tactic:
simp only [Function.comp_apply]

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

Goal state before:
pp: case inl
α : Type u
r : α → α → Prop
inst✝¹ : IsOrderConnected α r
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
exact Or.inl (rel ab)

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

Goal state before:
pp: M : Type u_3
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
⊢ a ^ count a s = (filter (Eq a) s).prod

Tactic:
rw [filter_eq, prod_replicate]

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

Goal state before:
pp: α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate' n.succ = (l ++ [a]).rotate' n

Tactic:
simp [rotate']

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
have hnl : n ≤ l.length := le_of_succ_le_succ h

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).length = l.length

Tactic:
rw [rotate_eq_rotate', length_rotate']

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

Goal state before:
pp: α : Type u_3
R : α → α → Prop
l : List α
v : α
hl : IsChain R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ IsChain R (v :: l)

Tactic:
by
  cases l <;> grind

Goal state after: