mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (ndinsert a s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))

Tactic:
ndinsert_of_notMem h,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ Multiset.fold op b (Multiset.map f (a ::ₘ s.val)) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
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
hc : c <+~ l
⊢ c <+ insertionSort r l

Tactic:
by
  classical
  obtain ⟨d, hc, hd⟩ := hc
  induction l generalizing c d with
  | nil         => grind [nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂

Tactic:
by obtain - | h | h := h; exacts [(irrefl_of r a h).elim, h]

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

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

Tactic:
rw [rotate_eq_rotate', rotate_eq_rotate', rotate'_cons_succ]

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

Goal state before:
pp: case cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate n ~r hd :: tl

Tactic:
use (hd :: tl).length * n - n
    rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]
    exact Nat.le_mul_of_pos_left _ (by simp)

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_4
l₁ : List α
l₂ : (a : α) → List (σ a)
⊢ ((↑l₁).sigma fun a ↦ ↑(l₂ a)) = ↑(l₁.sigma l₂)

Tactic:
rw [Multiset.sigma, List.sigma, ← coe_bind]
  simp

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

Goal state before:
pp: n : ℕ
⊢ n.choose 2 = n * (n - 1) / 2

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [triangle_succ n, choose, ih]
    simp [Nat.add_comm]

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

Goal state before:
pp: n k : ℕ
⊢ ¬n.choose k ≠ 0 ↔ ¬k ≤ n

Tactic:
simp [choose_eq_zero_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
⊢ ∀ (m : Multiset α) (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)

Tactic:
m

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
⊢ ∀ (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m : ℕ
⊢ 2 * m + 1 = 1 + (m + m)

Tactic:
Nat.add_comm (2 * m) 1,

Goal state after:
m : ℕ
⊢ 1 + 2 * m = 1 + (m + m)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
← Nat.mul_sub_left_distrib,

Goal state after:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose k * (n + 1 - (k + 1)) = n.choose k * (n - k)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

pp: case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
· apply choose_le_middle_of_le_half_left a

Goal state after:
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n.choose r ≤ n.choose (n / 2)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
Nat.succ_add_sub_one,

Goal state after:
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (n + 1).multichoose k + n.multichoose (k + 1) = (n + (k + 1)).choose (k + 1)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (image2 f s t).Infinite

Tactic:
rintro (⟨hs, b, hb⟩ | ⟨ht, a, ha⟩)
    · exact hs.image2_left hb (hfs _ hb)
    · exact ht.image2_right ha (hft _ ha)

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (range f)⁻¹ = range fun i ↦ (f i)⁻¹

Tactic:
rw [← image_inv_eq_inv]
  exact (range_comp ..).symm

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

Goal state before:
pp: case a.inl
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ {1}
⊢ x ∈ ↑(closure s)

pp: case a.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(Subsemigroup.closure s)
⊢ x ∈ ↑(closure s)

Tactic:
· exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)

Goal state after:
case a.inr
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(Subsemigroup.closure s)
⊢ x ∈ ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
⊢ p = q

Tactic:
have := SetLike.ext'_iff.1 h

Goal state after:
G : Type u_1
inst✝ : Group G
p q : Subgroup G
h : p.toSubmonoid = q.toSubmonoid
this : ↑p.toSubmonoid = ↑q.toSubmonoid
⊢ p = q
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
y₁ : G
hy₁ : y₁ ∈ s
z₁ : G
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : G
hy₂ : y₂ ∈ s
z₂ : G
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ y₁ * y₂ * (y₂⁻¹ * z₁ * y₂ * z₂) = y₁ * z₁ * (y₂ * z₂)

Tactic:
by simp [mul_assoc]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
y : G
hy : y ∈ s
z : G
hz : z ∈ t
hx✝ : y * z ∈ closure (↑s ∪ ↑t)
⊢ y⁻¹ * (y * z⁻¹ * y⁻¹) = (y * z)⁻¹

Tactic:
by simp [mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
a : α
⊢ a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n

Tactic:
by
  simp [decode₂, Option.bind_eq_some_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
g : G
hg : g ∈ s
⊢ ↑(MulAut.conj h) (h⁻¹ * g * h⁻¹⁻¹) = g

Tactic:
by simp [mul_assoc]

Goal state after:
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
x : N
⊢ x ∈ comap f (normalizer ↑H) → x ∈ normalizer ↑(comap f H)

Tactic:
by
  simp only [mem_normalizer_iff, mem_comap]
  intro h n
  simp [h (f n)]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
tn : N.Normal
a : G
h : a ∈ N
⊢ conjugatesOf a ⊆ ↑N

Tactic:
rintro a hc

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
tn : N.Normal
a✝ : G
h : a✝ ∈ N
a : G
hc : a ∈ conjugatesOf a✝
⊢ a ∈ ↑N
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
rw [prod_take_succ _ _ h]

Goal state after:
case inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take n L).prod * L[n]
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // p x } ⊕ { x // q x }
⊢ (subtypeOrLeftEmbedding p q)
      (Sum.elim (⇑(Subtype.impEmbedding p (fun x ↦ p x ∨ q x) ⋯)) (⇑(Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯)) x) =
    x

Tactic:
by
    cases x with
    | inl x => grind
    | inr x =>
      simp only [Sum.elim_inr]
      rw [subtypeOrLeftEmbedding_apply_right]
      · grind
      · suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩

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

Goal state before:
pp: case inl.inl
M : Type u_1
inst✝ : Monoid M
a : M
ha : IsIdempotentElem a
⊢ 1 * 1 ∈ {1, a}

pp: case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ 1 * b✝ ∈ {1, b✝}

pp: case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ * 1 ∈ {1, a✝}

pp: case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}

Tactic:
· rw [one_mul]; exact .inl rfl

Goal state after:
case inl.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ 1 * b✝ ∈ {1, b✝}

case inr.inl
M : Type u_1
inst✝ : Monoid M
a✝ : M
ha : IsIdempotentElem a✝
⊢ a✝ * 1 ∈ {1, a✝}

case inr.inr
M : Type u_1
inst✝ : Monoid M
b✝ : M
ha : IsIdempotentElem b✝
⊢ b✝ * b✝ ∈ {1, b✝}
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b : α
⊢ ∀ {m : α} {o : Option α}, b ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r b m

Tactic:
m

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
⊢ ∀ {o : Option α}, b ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r b m
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : l ≠ []
head✝ : α
tail✝ : List α
x✝ : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝).maximum ≠ ⊥

Tactic:
by simp [maximum_cons]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
head✝ : α
tail✝ : List α
x✝ : 0 < (head✝ :: tail✝).length
⊢ (head✝ :: tail✝).maximum ≠ ⊥

Tactic:
by simp [maximum_cons]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux 0 l (g ∘ f) (map g r ++ s) = map g (sublistsLenAux 0 l f r) ++ s

Tactic:
by unfold sublistsLenAux; simp

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

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

Tactic:
exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

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

Goal state before:
pp: case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]

Tactic:
apply (perm_append_comm.append_left _).trans

Goal state after:
case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)

Tactic:
refine ⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩ <;>
    rintro rfl

Goal state after:
case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
j : Finset α
hj : j ⊆ s
hi : insert a j ⊆ s
⊢ insert a j = j

case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
hj : insert a i ⊆ s
⊢ i = insert a i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b ↦ a \ f b) = a \ {a✝}.sup f

Tactic:
sup_singleton,

Goal state after:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b ↦ a \ f b) = a \ f a✝
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < s.sup f ↔ ∃ b ∈ s, a < f b

Tactic:
by
  apply Iff.intro
  · induction s using cons_induction with
    | empty => exact (absurd · not_lt_bot)
    | cons c t hc ih =>
      rw [sup_cons, lt_sup_iff]
      exact fun
      | Or.inl h => ⟨c, mem_cons.2 (Or.inl rfl), h⟩
      | Or.inr h => let ⟨b, hb, hlt⟩ := ih h; ⟨b, mem_cons.2 (Or.inr hb), hlt⟩
  · exact fun ⟨b, hb, hlt⟩ => lt_of_lt_of_le hlt (le_sup hb)

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

Goal state before:
pp: case mp.refine_1
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ BddAbove (range fun i ↦ ⨆ (_ : i ∈ s), f i)

Tactic:
classical
      refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
      intro
      simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind

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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ i, b < ↑(f i)
r : α
⊢ ∃ y ∈ range f, r < y

Tactic:
rcases hf r (WithTop.coe_lt_top r) with ⟨i, hi⟩

Goal state after:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ i, b < ↑(f i)
r : α
i : ι
hi : ↑r < ↑(f i)
⊢ ∃ y ∈ range f, r < y
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case inl.inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n = sInf {m | p m}
⊢ n = sInf {m | p m}

pp: case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ n = sInf {m | p m}

Tactic:
· exact hnp

Goal state after:
case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ n = sInf {m | p m}
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
hIoo : h₀_finset_Ioo = h₁_finset_Ioo
⊢ { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := ⋯, finset_mem_Ico := ⋯, finset_mem_Ioc := ⋯, finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }

Tactic:
hIoo

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

Goal state before:
pp: case inr.mpr.inl.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

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

Goal state before:
pp: case inr.mpr.inr.refine_3
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ (i + a * (n / a)) % a = i

Tactic:
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
⊢ a n ⋖ if ha : IsMax (a n) then a n else next ha

Tactic:
dif_neg hn

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
⊢ a n ⋖ next hn
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
⊢ ∀ m ≥ n, P m

Tactic:
m

Goal state after:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
⊢ m ≥ n → P m
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g m)) ((Prod.fst ∘ f) (g n))
m n : ℕ
h : m < n
hf : s ((Prod.snd ∘ f ∘ ⇑g) m) ((Prod.snd ∘ f ∘ ⇑g) n)
⊢ ∃ m n, m < n ∧ (fun a b ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono h, h₁ _ _ h.le, hf⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ ∀ (a : ℕ → α),
    (∃ m n, m < n ∧ r (a m) (a n)) ↔
      ∃ m n, m < n ∧ s (((Equiv.refl ℕ).arrowCongr ↑f) a m) (((Equiv.refl ℕ).arrowCongr ↑f) a n)

Tactic:
congr! with g a b

Goal state after:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
g : ℕ → α
a b : ℕ
⊢ r (g a) (g b) ↔ s (((Equiv.refl ℕ).arrowCongr ↑f) g a) (((Equiv.refl ℕ).arrowCongr ↑f) g b)
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ico ↑a ↑b) ↔ a ≤ x ∧ x < b

Tactic:
by
    simp_rw [Finset.mem_subtype, mem_Ico, Subtype.coe_le_coe, Subtype.coe_lt_coe]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Icc ↑a ↑b)) = Icc ↑a ↑b

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Icc ↑a ↑b
⊢ p x
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ico ↑a ↑b)) = Ico ↑a ↑b

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ico ↑a ↑b
⊢ p x
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioc ↑a ↑b)) = Ioc ↑a ↑b

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioc ↑a ↑b
⊢ p x
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioo ↑a ↑b)) = Ioo ↑a ↑b

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Goal state after:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioo ↑a ↑b
⊢ p x
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ g • a ∈ orbit G (h • a)

Tactic:
by
  simp only [orbit_smul, mem_orbit]

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

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : g • ↑b = ↑a
⊢ a ∈ orbit (↥H) b

Tactic:
rw [subgroup_smul_def, ← orbit.coe_smul, ← Subtype.ext_iff] at h

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : α
a b : ↑(orbit G x)
g : ↥H
h : ↑g • b = a
⊢ a ∈ orbit (↥H) b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ x.orbit = MulAction.orbit G (φ x)

Tactic:
by
  conv_lhs => rw [← hφ x]
  rfl

Goal state after: