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

Goal state before:
pp: case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rw [castSucc_lt_iff_succ_le, iff_false_right (Fin.not_le.2 H), succAbove_of_lt_succ _ _ H]
    exact Fin.not_lt.2 <| Fin.le_of_lt H

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

Goal state before:
pp: n : ℕ
α : Type u
σ : Perm (Fin n)
f : Fin n → α
⊢ ofFn (f ∘ ⇑σ) ~ ofFn f

Tactic:
by
  rw [ofFn_eq_map, ofFn_eq_map, ← map_map]
  exact σ.map_finRange_perm.map f

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
⊢ cons x (update p i y) j = update (cons x p) i.succ y j

Tactic:
cases j using Fin.cases

Goal state after:
case zero
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ cons x (update p i y) 0 = update (cons x p) i.succ y 0

case succ
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
i✝ : Fin n
⊢ cons x (update p i y) i✝.succ = update (cons x p) i.succ y i✝.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
⊢ update (cons x p) 0 z j = cons z p j

Tactic:
cases j using Fin.cases

Goal state after:
case zero
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (cons x p) 0 z 0 = cons z p 0

case succ
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
i✝ : Fin n
⊢ update (cons x p) 0 z i✝.succ = cons z p i✝.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ cons (q 0) (tail q) j = q j

Tactic:
cases j using Fin.cases

Goal state after:
case zero
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
⊢ cons (q 0) (tail q) 0 = q 0

case succ
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i✝ : Fin n
⊢ cons (q 0) (tail q) i✝.succ = q i✝.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
⊢ cons x₀ x 0 = cons x₀ x j → 0 = j

Tactic:
cases j using Fin.cases

Goal state after:
case zero.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ cons x₀ x 0 = cons x₀ x 0 → 0 = 0

case zero.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x 0 = cons x₀ x i✝.succ → 0 = i✝.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
j : Fin (n + 1)
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x j → i✝.succ = j

Tactic:
cases j using Fin.cases

Goal state after:
case succ.zero
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝ : Fin n
⊢ cons x₀ x i✝.succ = cons x₀ x 0 → i✝.succ = 0

case succ.succ
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i✝¹ i✝ : Fin n
⊢ cons x₀ x i✝¹.succ = cons x₀ x i✝.succ → i✝¹.succ = i✝.succ
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove (p.castSucc.succAbove i) = i

pp: case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
· rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]

Goal state after:
case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove (p.castSucc.succAbove i) = i
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) →
    ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}

Tactic:
rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩

Goal state after:
case mpr
α : Type u_1
s : Finset α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ b b_1 b_2, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_2
f : Fin n → α
x x✝ : α
⊢ x✝ ∈ Set.range (snoc f x) ↔ x✝ ∈ insert x (Set.range f)

Tactic:
simp [Fin.exists_fin_succ', or_comm, eq_comm]

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
a b : ℕ
⊢ f (a + 1) - (f 0 + 1) ≤ f (b + 1) - (f 0 + 1) ↔ a ≤ b

Tactic:
by
      rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
      rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
      exact b.succ_pos

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.6
inst✝ : Fintype α
⊢ Trunc { f // Bijective f }

Tactic:
refine
    Quot.recOnSubsingleton
      (motive := fun s : Multiset α =>
        (∀ x : α, x ∈ s) → s.Nodup → Trunc {f : Fin (Multiset.card s) → α // Bijective f})
      univ.val
      (fun l (h : ∀ x : α, x ∈ l) (nd : l.Nodup) => Trunc.mk (nd.getBijectionOfForallMemList _ h))
      mem_univ_val univ.2

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

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ (last n).insertNth x p = snoc p x

Tactic:
by simp [insertNth_last]

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

Goal state before:
pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
⊢ cons a p j = cons a (i.insertNth x p) (i.succ.succAbove j)

Tactic:
cases j using Fin.cases

Goal state after:
case p.zero
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ cons a p 0 = cons a (i.insertNth x p) (i.succ.succAbove 0)

case p.succ
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
i✝ : Fin n
⊢ cons a p i✝.succ = cons a (i.insertNth x p) (i.succ.succAbove i✝.succ)
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : IsTrans α R
l : List α
a b : α
⊢ R a b → Pairwise R (b :: l) → Pairwise R (a :: b :: l)

Tactic:
by
  simp_rw [pairwise_cons_cons_iff_of_trans]
  exact And.intro

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p s.prod

Tactic:
rw [prod_eq_foldr]

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
p : M → Prop
s : Multiset M
p_mul : ∀ (a b : M), p a → p b → p (a * b)
p_one : p 1
p_s : ∀ (a : M), a ∈ s → p a
⊢ p (foldr (fun x1 x2 ↦ x1 * x2) 1 s)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inl
α : Type u
l : List α
n : ℕ
hl : 0 = l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
simp [eq_nil_of_length_eq_zero hl.symm]

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

Goal state before:
pp: α : Type u_1
a : α
S : Multiset (Multiset α)
⊢ ∀ (a_1 : Multiset α) (s : Multiset (Multiset α)),
    (a ∈ s.join ↔ ∃ s_1, s_1 ∈ s ∧ a ∈ s_1) → (a ∈ (a_1 ::ₘ s).join ↔ ∃ s_1, s_1 ∈ a_1 ::ₘ s ∧ a ∈ s_1)

Tactic:
by
    simp +contextual [or_and_right, exists_or]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f

Tactic:
refine le_iff_count.2 fun a ↦ ?_

Goal state after:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (S.bind f)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations.length = l.length

Tactic:
by simp [cyclicPermutations_of_ne_nil _ h]

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

Goal state before:
pp: case cons
α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ drop n (a :: l) ++ take n (a :: l) = (a :: l).rotate n

Tactic:
rw [rotate_eq_drop_append_take (by simpa using h.le)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ x, ∃ a ∈ s, x ∈ t a) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x

Tactic:
exists_comm

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
⊢ (∃ b a, b ∈ s ∧ a ∈ t b) ↔ ∃ x ∈ s, ∃ x_1, x_1 ∈ t x
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

Tactic:
subst eq

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
⊢ ((t a).bind fun b ↦ map (Pi.cons (a ::ₘ m) a b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)) ≍
    (t a).bind fun b ↦ map (Pi.cons (a ::ₘ m) a b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.offDiag = #s * #s - #s

Tactic:
by
  rw [← sq]
  rcases s with ⟨⟨s⟩, hs⟩
  apply List.length_offDiag

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi

Tactic:
by
  simp only [iInter, iInf_subtype']
  have : Nonempty { i // p i } := nonempty_subtype.2 hp
  apply InjOn.image_iInter_eq
  simpa only [iUnion, iSup_subtype'] using h

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s✝ : Set M
S : Subsemigroup M
s : Set (Subsemigroup M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ t ∈ s, ↑t
hy : b✝ ∈ ⋂ t ∈ s, ↑t
i : Subsemigroup M
h : i ∈ s
⊢ a✝ ∈ i

Tactic:
by apply Set.mem_iInter₂.1 hx i h

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
p : M → Prop
s : Set M
closure : Subsemigroup.closure s = ⊤
mem : ∀ x ∈ s, p x
mul : ∀ (x y : M), p x → p y → p (x * y)
x : M
⊢ p x

Tactic:
by
  induction closure.symm ▸ mem_top x using closure_induction with
  | mem _ h => exact mem _ h
  | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter

Goal state after:
case rs
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n

case rt
α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ t ^ n
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r ∈ S ×ˢ {t}, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ ⋂₀ {t}

Tactic:
sInter_singleton

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r ∈ S ×ˢ {t}, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t

Tactic:
rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton]

Goal state after:
α : Type u_1
β : Type u_2
S : Set (Set α)
hS : S.Nonempty
t : Set β
⊢ ⋂ r ∈ S ×ˢ {t}, r.1 ×ˢ r.2 = ⋂ s ∈ S, s ×ˢ t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, ⋂₀ {s} ×ˢ t

Tactic:
sInter_singleton

Goal state after:
α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
s : Set (Submonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ t ∈ s, ↑t
hy : b✝ ∈ ⋂ t ∈ s, ↑t
i : Submonoid M
h : i ∈ s
⊢ a✝ ∈ i

Tactic:
by apply Set.mem_iInter₂.1 hx i h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
s : Set (Subgroup G)
x : G
hx : x ∈ ((⨅ S ∈ s, S.toSubmonoid).copy (⋂ S ∈ s, ↑S) ⋯).carrier
i : Subgroup G
h : i ∈ s
⊢ x ∈ i

Tactic:
by apply Set.mem_iInter₂.1 hx i h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i ↔ ∃ i, p i ∧ x ∈ K i

Tactic:
refine ⟨?_, fun ⟨i, hi', hi⟩ ↦ ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i → ∃ i, p i ∧ x ∈ K i

case refine_2
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i✝ : ι
hp : p i✝
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
x✝ : ∃ i, p i ∧ x ∈ K i
i : ι
hi' : p i
hi : x ∈ K i
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = (g.comp f).range

Tactic:
range_eq_map

Goal state after:
G : Type u_1
inst✝² : Group G
N : Type u_5
P : Type u_6
inst✝¹ : Group N
inst✝ : Group P
g : N →* P
f : G →* N
⊢ map g (map f ⊤) = map (g.comp f) ⊤
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y₁ : C
hy₁ : y₁ ∈ s
z₁ : C
hz₁ : z₁ ∈ t
hx✝ : y₁ * z₁ ∈ closure (↑s ∪ ↑t)
y₂ : C
hy₂ : y₂ ∈ s
z₂ : C
hz₂ : z₂ ∈ t
hy✝ : y₂ * z₂ ∈ closure (↑s ∪ ↑t)
⊢ y₁ * y₂ * (z₁ * z₂) = y₁ * z₁ * (y₂ * z₂)

Tactic:
by simp [mul_assoc, mul_left_comm]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ (normalizer ↑H).unop = normalizer ↑H.unop

Tactic:
by
  rw [← op_inj, op_unop, op_normalizer, op_unop]

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

Goal state before:
pp: n : ℕ
⊢ n.succ.bodd = !n.bodd

Tactic:
simp only [bodd]

Goal state after:
n : ℕ
⊢ n.succ.testBit 0 = !n.testBit 0
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = bit b (shiftLeft' b m n) >>> (1 + k)

Tactic:
shiftRight_add

Goal state after:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = bit b (shiftLeft' b m n) >>> 1 >>> k
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
j✝ : ι
c : α j✝
hk : r i✝ j✝
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

Tactic:
exact Lex.left _ _ hk

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inr
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 : α
h : b ≤ a
⊢ f (max a b) = f a ⊔ f b

Tactic:
sup_eq_left.2 h,

Goal state after:
case inr
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 : α
h : b ≤ a
⊢ f a = f a ⊔ f b
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists.length = 2 ^ l.length

Tactic:
simp only [sublists_eq_sublists', length_map, length_sublists', length_reverse]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = sSup (f '' ↑s)

Tactic:
← Finset.coe_image,

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = sSup ↑(image f s)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
⊢ ∃ i ∈ s, s.sup' H f = f i

Tactic:
by
  induction H using Finset.Nonempty.cons_induction with
  | singleton c => exact ⟨c, mem_singleton_self c, rfl⟩
  | cons c s hcs hs ih =>
    rcases ih with ⟨b, hb, h'⟩
    rw [sup'_cons hs, h']
    cases le_total (f b) (f c) with
    | inl h => exact ⟨c, mem_cons.2 (Or.inl rfl), sup_eq_left.2 h⟩
    | inr h => exact ⟨b, mem_cons.2 (Or.inr hb), sup_eq_right.2 h⟩

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ (⋃ i, s i).Finite

Tactic:
suffices ⋃ i, s i ⊆ ⋃ i ∈ t, s i by exact (ht.biUnion hs).subset this

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ ⋃ i, s i ⊆ ⋃ i ∈ t, s i
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
this : ⨅ i ∈ s, f i ∈ f '' s
⊢ a < ⨅ i ∈ s, f i

Tactic:
simp only [mem_image] at this

Goal state after:
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
this : ∃ x ∈ s, f x = ⨅ i ∈ s, f i
⊢ a < ⨅ i ∈ s, f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
p : ι → Prop
f : Exists p → α
⊢ ⨆ (ih : Exists p), f ih = ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
refine le_antisymm ciSup_exists_le <| ciSup_le' fun i ↦ ciSup_le' fun hi ↦ ?_

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
p : ι → Prop
f : Exists p → α
i : ι
hi : p i
⊢ f ⋯ ≤ ⨆ (ih : Exists p), f ih
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Iio b = Iic a

Tactic:
by
  rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(image f (s.preimage f hf)) = ↑({x ∈ s | x ∈ Set.range f})

Tactic:
simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range,
      ← Set.sep_mem_eq]; rfl

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

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
x : α
hx : x ∈ ↑t
⊢ x ∈ Subtype.val '' Subtype.val ⁻¹' ↑t

Tactic:
simpa using ⟨hx, ht x hx⟩

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_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
⊢ { 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 } =
    { 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:
have hIoc : h₀_finset_Ioc = h₁_finset_Ioc := by
      ext a b x
      rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]

Goal state after:
α : 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
⊢ { 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 } =
    { 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 }
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case zero
a : ℕ
⊢ Set.InjOn (fun x ↦ x % a) ↑(Ico 0 (0 + a))

Tactic:
simp only [zero_add, Ico_zero_eq_range]

Goal state after:
case zero
a : ℕ
⊢ Set.InjOn (fun x ↦ x % a) ↑(range a)
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Infinite α
⊢ ∃ f, StrictMono f ∨ StrictAnti f

Tactic:
let f := Infinite.natEmbedding α
  obtain ⟨g, hg⟩ := exists_increasing_or_nonincreasing_subseq (· < ·) f
  refine ⟨f ∘ g, ?_⟩
  rcases hg with hIncreasing | hNonincreasing
  · exact Or.inl hIncreasing
  · refine Or.inr <| fun m n hmn ↦ lt_of_le_of_ne ?_ ((f.injective.comp g.injective).ne ?_)
    · grind
    · grind

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

Goal state before:
pp: α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
⊢ Iic ⊤ = univ

Tactic:
ext a; simp only [mem_Iic, le_top, mem_univ]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
a : α
b : ↑(Set.Iic a)
⊢ ↑b ∈ ↑(Iic a)

Tactic:
coe_Iic a

Goal state after:
ι : Type u_1
α : Type u_2
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
a : α
b : ↑(Set.Iic a)
⊢ ↑b ∈ Set.Iic a