mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc x x₀)
x : (i : Fin n) → init α i
x₀ : α (last n)
⊢ snoc (init (Fin.snoc x x₀)) (Fin.snoc x x₀ (last n)) ≍ snoc x x₀

Tactic:
Fin.init_snoc,

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
motive : ((i : Fin (n + 1)) → α i) → Sort u_2
snoc : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (last n)) → motive (Fin.snoc x x₀)
x : (i : Fin n) → init α i
x₀ : α (last n)
⊢ snoc x (Fin.snoc x x₀ (last n)) ≍ snoc x x₀
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
obtain ⟨x, hx⟩ := exists_notMem_finset t

Goal state after:
case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
x : α
hx : x ∉ t
⊢ ∃ t, s ⊆ t ∧ #t = n + 1
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
h : a ∉ s
⊢ fold op b f (cons a s h) = op (f a) (fold op b f s)

Tactic:
dsimp only [fold]
  rw [cons_val, Multiset.map_cons, fold_cons_left]

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

Goal state before:
pp: case cons.right
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ Pairwise Disjoint (map (map fun x ↦ a + x) l.ranges)

Tactic:
· rw [pairwise_map]
      apply Pairwise.imp _ hl
      intro u v
      apply disjoint_map
      exact fun u v => Nat.add_left_cancel

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

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

Tactic:
have hnl' : n ≤ (l ++ [a]).length := by
      rw [length_append, length_cons, List.length]; exact le_of_succ_le h

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).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
a : α
l : List α
n m : ℕ
⊢ ((a :: l).rotate' (n + 1)).rotate' m = (a :: l).rotate' (n + 1 + m)

Tactic:
rw [rotate'_cons_succ, rotate'_rotate' _ n, Nat.add_right_comm, ← rotate'_cons_succ,
      Nat.succ_eq_add_one]

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

Goal state before:
pp: α : Type u
a : α
n k : ℕ
⊢ ((replicate n a).rotate k).length = n

Tactic:
length_rotate,

Goal state after:
α : Type u
a : α
n k : ℕ
⊢ (replicate n a).length = n
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0 • s
⊢ a ∈ s

Tactic:
rw [zero_nsmul] at h
    exact absurd h (notMem_zero _)

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

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

Tactic:
length_rotate,

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse =
    l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.reverse.length - n % l.reverse.length))
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case append_singleton
α : Type u
a : List α
L : α
a✝ : ∀ (hL : a ≠ []), a.getLast hL :: a.dropLast ~r a
hL : a ++ [L] ≠ []
⊢ (a ++ [L]).getLast hL :: (a ++ [L]).dropLast ~r a ++ [L]

Tactic:
simp only [getLast_append, dropLast_concat]
    apply IsRotated.symm
    apply isRotated_concat

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ n.choose k = n ! / (k ! * (n - k)!)

Tactic:
rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ n.choose k = n.choose k * (k ! * (n - k)!) / (k ! * (n - k)!)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !

Tactic:
rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
a✝ : (a : α) → δ a
⊢ (a✝ ∈ piFinset fun a ↦ image (f a) (s a)) ↔ a✝ ∈ image (fun b a ↦ f a (b a)) (piFinset s)

Tactic:
simp only [mem_piFinset, mem_image, Classical.skolem, forall_and, funext_iff]

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

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ (univ.pi t).Finite

Tactic:
cases nonempty_fintype ι
  lift t to ∀ d, Finset (κ d) using ht
  classical
    rw [← Fintype.coe_piFinset]
    apply Finset.finite_toSet

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
g h : G
⊢ (h * g⁻¹) • g • x₀ = h • x₀

Tactic:
by simp [mul_smul]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set M
a : Subsemigroup Mᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' ↑a ↔ MulOpposite.unop ⁻¹' s ⊆ ↑a

Tactic:
exact MulOpposite.unop_surjective.forall

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set M
a : Submonoid Mᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' ↑a ↔ MulOpposite.unop ⁻¹' s ⊆ ↑a

Tactic:
exact MulOpposite.unop_surjective.forall

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ
n : ℕ
ih : n.boddDiv2 = (n.bodd, n.div2)
⊢ (match (n.bodd, n.div2) with
    | (false, m) => (true, m)
    | (true, m) => (false, m.succ)) =
    ((n + 1).bodd, (n + 1).div2)

Tactic:
cases hn : n.bodd <;> simp [hn]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (fun n ↦ (decode n).getD d) (encode x) = x

Tactic:
simp_rw [Encodable.encodek]; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
a : Subgroup Gᵐᵒᵖ
⊢ s ⊆ MulOpposite.op ⁻¹' ↑a ↔ MulOpposite.unop ⁻¹' s ⊆ ↑a

Tactic:
exact MulOpposite.unop_surjective.forall

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ (¬∀ (a : α), a ∉ decode₂ α n) ↔ ∃ y, encode y = n

Tactic:
Encodable.mem_decode₂,

Goal state after:
α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ (¬∀ (a : α), ¬encode a = n) ↔ ∃ y, encode y = n
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ (¬∀ (a : α), ¬encode a = n) ↔ ∃ y, encode y = n

Tactic:
not_forall,

Goal state after:
α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ (∃ x, ¬¬encode x = n) ↔ ∃ y, encode y = n
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
h : H ≤ f.range
⊢ comap f (normalizer ↑H) = normalizer ↑(comap f H)

Tactic:
apply le_antisymm (le_normalizer_comap f)
  rw [← map_le_iff_le_comap]
  apply (le_normalizer_map f).trans
  rw [map_comap_eq_self h]

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

Goal state before:
pp: G : Type u_5
inst✝ : Group G
s t : Set G
⊢ conjugatesOfSet (s ∪ t) = conjugatesOfSet s ∪ conjugatesOfSet t

Tactic:
simp_rw [conjugatesOfSet, Set.biUnion_union]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
⊢ normalClosure s ≤ N

Tactic:
by
  intro a w
  refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
  · exact conjugatesOfSet_subset h hx
  · exact one_mem _
  · exact mul_mem ihx ihy
  · exact inv_mem ihx

Goal state after:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a = q * a

Tactic:
← idem.eq,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
h : IsUnit a
idem : IsIdempotentElem a
q : M
eq : q * a = 1
⊢ a * a = q * (a * a)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x = y ∨ x ∈ ys
⊢ x ≤ (y :: ys).prod

Tactic:
rcases h₁ with (rfl | h₁)

Goal state after:
case cons.inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
⊢ x ≤ (x :: ys).prod

case cons.inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ (y :: ys).prod
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
by
  obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx
  exact ⟨l, h1, (Multiset.prod_coe l).trans h2⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ Option.rec (some a) (fun val ↦ if val < a then some a else some val) (argmax id l) = max (argmax id l) ↑a

Tactic:
cases argmax id l

Goal state after:
case none
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ Option.rec (some a) (fun val ↦ if val < a then some a else some val) none = max none ↑a

case some
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
val✝ : α
⊢ Option.rec (some a) (fun val ↦ if val < a then some a else some val) (some val✝) = max (some val✝) ↑a
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
⊢ f (max a b) = f a ⊔ f b

Tactic:
by
      obtain h | h := le_total a b
      · rw [sup_eq_right.2 h, sup_eq_right.2 (OrderHomClass.mono f h : f a ≤ f b)]
      · rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min = ↑a

Tactic:
by
  rw [← insert_empty_eq]
  exact min_insert

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

Goal state before:
pp: case cons.mp.inl
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t

pp: case cons.mp.inr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t

Tactic:
· exact sublist_cons_of_sublist _ h

Goal state after:
case cons.mp.inr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ (↑l₁✝).powerset ≤ (↑l₂✝).powerset

Tactic:
powerset_coe',

Goal state after:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ ↑(List.map ofList l₁✝.sublists') ≤ (↑l₂✝).powerset
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ ↑(List.map ofList l₁✝.sublists') ≤ (↑l₂✝).powerset

Tactic:
powerset_coe',

Goal state after:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ ↑(List.map ofList l₁✝.sublists') ≤ ↑(List.map ofList l₂✝.sublists')
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Tactic:
exact mem_append_left _ IH

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

Goal state before:
pp: case h
α : Type u_2
a✝ : List α
⊢ ((range ((↑a✝).card + 1)).bind fun k ↦ powersetCard k ↑a✝) = (↑a✝).powerset

Tactic:
powerset_coe',

Goal state after:
case h
α : Type u_2
a✝ : List α
⊢ ((range ((↑a✝).card + 1)).bind fun k ↦ powersetCard k ↑a✝) = ↑(List.map ofList a✝.sublists')
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case inl
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
ha : ⊥ ∈ s
⊢ id ⊥ ≤ (s.erase ⊥).sup id

Tactic:
exact bot_le

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (insert x (u.erase x))

Tactic:
powersetCard_succ_insert (notMem_erase _ _)

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (u.erase x) ∪ image (insert x) (powersetCard n (u.erase x))
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
w✝ : ι
hmem : w✝ ∈ s
hx : f w✝ = ⨅ i ∈ s, f i
⊢ a < f w✝

Tactic:
exact H _ hmem

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
have bdd : BddAbove (range f) := not_not.mp fun h ↦ gt.ne (ciSup_of_not_bddAbove h)

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
not_forall,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ (∃ x, ∃ (_ : a < x), ¬¬x < b) ↔ ∃ c, a < c ∧ c < b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ (¬∀ ⦃c : α⦄, a < c → ¬c < b) ↔ ∃ c, a < c ∧ c < b

Tactic:
not_forall,

Goal state after:
α : Type u_1
inst✝ : LT α
a b : α
h : a < b
⊢ (∃ x, ∃ (_ : a < x), ¬¬x < b) ↔ ∃ c, a < c ∧ c < b
Module: Mathlib.Order.Cover

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : LinearOrder α
a : α
inst✝ : OrderTop α
x✝ : IsTop ⊤ ∧ a ⋖ ⊤
hab : a ⋖ ⊤
⊢ Ioc a ⊤ = {⊤}

Tactic:
Ioc_eq_singleton_right_iff

Goal state after:
case top
α : Type u_1
inst✝¹ : LinearOrder α
a : α
inst✝ : OrderTop α
x✝ : IsTop ⊤ ∧ a ⋖ ⊤
hab : a ⋖ ⊤
⊢ a ⋖ ⊤
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
⊢ a ⩿ b ↔ ∃ i x, a i ⩿ x ∧ b = Function.update a i x

Tactic:
by
  rw [wcovBy_iff]
  constructor
  · rintro ⟨i, hi, h⟩
    exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩
  · rintro ⟨i, x, h, rfl⟩
    exact ⟨i, by simpa +contextual⟩

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Finset.Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
Finset.mem_Ioc

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ filter (fun x ↦ c ≤ x) (Ico a b) = Ico (max a c) b

Tactic:
rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
⊢ h₀_finset_Ici = h₁_finset_Ici

Tactic:
ext a b

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
a b : α
⊢ b ∈ h₀_finset_Ici a ↔ b ∈ h₁_finset_Ici a
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
⊢ h₀_finset_Ioi = h₁_finset_Ioi

Tactic:
ext a b

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
a b : α
⊢ b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
⊢ ¬WellFounded r

Tactic:
wellFounded_iff_isEmpty,

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
⊢ ¬IsEmpty ((fun x1 x2 ↦ x1 > x2) ↪r r)
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
      have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m
      rw [Nat.orderEmbeddingOfSet_range bad] at h
      exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
        intro n
        have h := hm _ (Nat.le_add_left m n)
        simp only [bad, exists_prop, not_not, Set.mem_ofPred_eq, not_forall] at h
        obtain ⟨n', hn1, hn2⟩ := h
        refine ⟨n + n' - n - m, by lia, ?_⟩
        convert! hn2
        lia

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
h : ∀ (n : ℕ), ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ ↑(insert b (Ico a b)) = ↑(Icc a b)

Tactic:
coe_insert,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert b ↑(Ico a b) = ↑(Icc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ ↑(insert a (Ioc a b)) = ↑(Icc a b)

Tactic:
coe_insert,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a ↑(Ioc a b) = ↑(Icc a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ ↑(insert a (Ioo a b)) = ↑(Ico a b)

Tactic:
coe_insert,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a ↑(Ioo a b) = ↑(Ico a b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ ↑(insert b (Ioo a b)) = ↑(Ioc a b)

Tactic:
coe_insert,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert b ↑(Ioo a b) = ↑(Ioc a b)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inl
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ m = n

Tactic:
refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1.inr.inr
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ m = n

Tactic:
refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction M α
g : M
x : ↥(FixedPoints.submonoid M α)
y : α
⊢ g • x • y = x • g • y

Tactic:
simp_rw [Submonoid.smul_def, smul_eq_mul, smul_mul', x.2 g]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : y ≤ x
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
exact .single <| wcovBy_of_le_of_le hxy hxy'

Goal state after: