mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
exact
      let n := Nat.find h
      have hn : x < y ^ n := Nat.find_spec h
      have hnp : 0 < n :=
        pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
      have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
      have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
      ⟨Nat.pred n, le_of_not_gt (Nat.find_min h hltn), by rwa [hnsp]⟩

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ (y ^ m)⁻¹

Tactic:
le_inv_comm₀ hx (zpow_pos hyp _)

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ y ^ m ≤ x⁻¹
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
inst✝ : AddMonoid G
a : G
⊢ Multiplicative.toAdd 1 +ᵥ AddConstMap.id = 1

Tactic:
ext; apply zero_add

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

Goal state before:
pp: G : Type u_5
inst✝ : AddCommGroup G
x : G
⊢ pointReflection x = Equiv.subLeft (2 • x)

Tactic:
by
  ext; simp [pointReflection, sub_add_eq_add_sub, two_nsmul]

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

Goal state before:
pp: α : Type u_1
a b : α
as bs : Multiset α
this✝² : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
this✝¹ : a ∈ b ::ₘ bs
this✝ : a ∈ bs
cs : Multiset α
hcs : bs = a ::ₘ cs
this : a ::ₘ as = b ::ₘ a ::ₘ cs
⊢ a ::ₘ as = a ::ₘ b ::ₘ cs

Tactic:
rwa [cons_swap]

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
by
  rw [← rel_flip, rel_cons_left]
  refine exists₂_congr fun a as' => ?_
  rw [rel_flip, flip]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs ⊆ ys → xs ∪ ys = ys
h : x :: xs ⊆ ys
⊢ x :: xs ∪ ys = ys

Tactic:
rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self,
      ih <| subset_of_cons_subset h]

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

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

Tactic:
disjoint_cons_left

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

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
⊢ n - t.card < n - s.card

Tactic:
have := (card_lt_card _h)

Goal state after:
α : Type u_1
n : ℕ
s t : Multiset α
ht : t.card ≤ n
_h : s < t
this : s.card < t.card
⊢ n - t.card < n - s.card
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case refine_1
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countP p (map f 0) = (filter (fun a ↦ p (f a)) 0).card

Tactic:
rw [map_zero, countP_zero, filter_zero, card_zero]

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint (a ::ₘ t) s ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
disjoint_cons_left

Goal state after:
α : Type u_1
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a✝ : α
a b c : Finset α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ⊆ a ⊔ b ⊓ c

Tactic:
simp +contextual only
        [sup_eq_union, inf_eq_inter, subset_iff, mem_inter, mem_union, and_imp,
        or_imp, true_or, imp_true_iff, true_and, or_true]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.SurjOn f ↑s ↑t
⊢ #t ≤ #s

Tactic:
classical unfold Set.SurjOn at hf; exact (card_le_card (mod_cast hf)).trans card_image_le

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i.castPred hi = j
⊢ i = j.castSucc

Tactic:
by rw [← h, castSucc_castPred]

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b

Tactic:
by
  simp_rw [ofFn_add]
  simp [Fin.append_left', Fin.append_right]

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨m * ↑i + ↑j, ⋯⟩).flatten

Tactic:
m.mul_comm,

Goal state after:
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ (ofFn fun i ↦ f (Fin.cast ⋯ i)) = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * m + ↑j, ⋯⟩).flatten
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a < n

Tactic:
by omega

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ (n - ↑b + ↑a) % n = (m - ↑b + ↑a) % m + n - m

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = (m - ↑b + ↑a) % m + n - m
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ m - ↑b + ↑a < m

Tactic:
by omega

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = (m - ↑b + ↑a) % m + n - m

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m

Tactic:
rw [Nat.mod_eq_of_lt (by omega)]

Goal state after:
n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a = m - ↑b + ↑a + n - m
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s = 1 ↔ ∃ a, s = {a}

Tactic:
cases s

Goal state after:
case mk
α : Type u_1
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ #{ val := val✝, nodup := nodup✝ } = 1 ↔ ∃ a, { val := val✝, nodup := nodup✝ } = {a}
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = pmap (fun i hi ↦ f ⟨i, hi⟩) (range n) ⋯

Tactic:
by
  ext
  grind

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (ofFn f).Nodup

Tactic:
rw [ofFn_eq_pmap]

Goal state after:
α : Type u
n : ℕ
f : Fin n → α
hf : Function.Injective f
⊢ (pmap (fun i hi ↦ f ⟨i, hi⟩) (range n) ⋯).Nodup
Module: Mathlib.Data.Finset.Card

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

Tactic:
· rintro ⟨a, b, c, d, ha, hb, hc, hd, hab, hac, had, hbc, hbd, hcd⟩
      exact ⟨a, b, c, d, {a, b, c, d}, by simp_all [insert_subset_iff]⟩

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

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

Tactic:
by simp [insertNth, succAboveCases]

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

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ 2 ≤ count x l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
← replicate_sublist_iff,

Goal state after:
α : Type u_1
l : List α
x : α
⊢ replicate 2 x <+ l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m
Module: Mathlib.Data.List.Sort

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

Tactic:
rw [orderedInsert_cons, if_neg hr] at ih

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
ih : a :: orderedInsert r x as <+ orderedInsert r x bs
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ s.Infinite

Tactic:
← range_subset_iff

Goal state after:
α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : range f ⊆ s
⊢ s.Infinite
Module: Mathlib.Data.List.Lex

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
h : l₁ ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂

Tactic:
induction l₁ generalizing l₂ <;> rcases l₂ with - | ⟨b, l₂⟩

Goal state after:
case nil.nil
α : Type u
inst✝ : DecidableEq α
H : [].length ≤ [].length
h : [] ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] []

case nil.cons
α : Type u
inst✝ : DecidableEq α
b : α
l₂ : List α
H : [].length ≤ (b :: l₂).length
h : [] ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] (b :: l₂)

case cons.nil
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
H : (head✝ :: tail✝).length ≤ [].length
h : head✝ :: tail✝ ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) []

case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ filter p (n • {a}) = n • {a}

Tactic:
simp only [filter_eq_self, nsmul_zero, filter_eq_nil]

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ ∀ (a_1 : α), a_1 ∈ n • {a} → p a_1
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (n • {a}) = n • 0

Tactic:
simp only [filter_eq_self, nsmul_zero, filter_eq_nil]

Goal state after:
case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ ∀ (a_1 : α), a_1 ∈ n • {a} → ¬p a_1
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ f ∈ piFinset t → ∀ (a : α), f a ∈ t a

pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t

Tactic:
· simp only [piFinset, mem_map, and_imp, forall_prop_of_true, mem_univ, exists_imp,
      mem_pi]
    rintro g hg hgf a
    rw [← hgf]
    exact hg a

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
f : (a : α) → δ a
⊢ (∀ (a : α), f a ∈ t a) → f ∈ piFinset t
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case zero.zero
⊢ 1 = 0! * 1

Tactic:
factorial_zero,

Goal state after:
case zero.zero
⊢ 1 = 1 * 1
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (k + 1) = k + 1 + 1

Tactic:
multichoose,

Goal state after:
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (1 + 1).multichoose k = k + 1 + 1
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 + k + 1).choose (k + 1)

Tactic:
Nat.choose_succ_succ

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).choose k + (n + k).choose k.succ
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ f '' (fun x ↦ x⁻¹) '' s = g '' s

Tactic:
Set.image_image

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ (fun x ↦ f x⁻¹) '' s = g '' s
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ closure (insert 1 s) = closure s

Tactic:
by
  rw [insert_eq, closure_union, sup_eq_right, closure_singleton_le_iff_mem]
  apply one_mem

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

Goal state before:
pp: case refine_1.inl
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑s
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

pp: case refine_1.inr
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

Tactic:
· exact ⟨y, h, 1, t.one_mem, by simp⟩

Goal state after:
case refine_1.inr
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
simp_rw [closure, op_sInf, Set.preimage_ofPred_eq, Submonoid.coe_unop]

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ (∃ x, ∃ (hx : x ∈ S), ⟨x, hx⟩ ≠ ⟨1, ⋯⟩) ↔ ∃ x ∈ S, x ≠ 1

Tactic:
by simp [Ne]

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

Goal state before:
pp: m n : ℕ
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)

Tactic:
have : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m := by
      rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]; simp
    simp [shiftLeft_eq, shiftLeft', bit_val, shiftLeft'_false, this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
s : α ⊕ β
⊢ decodeSum (encodeSum s) = some s

Tactic:
cases s

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : α
⊢ decodeSum (encodeSum (Sum.inl val✝)) = some (Sum.inl val✝)

case inr
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : β
⊢ decodeSum (encodeSum (Sum.inr val✝)) = some (Sum.inr val✝)
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
head✝ : M
xs : List M
⊢ prodAux (head✝ :: xs) = (head✝ :: xs).prod

Tactic:
by simp [prodAux, List.prod_eq_foldl]

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

Goal state before:
pp: case right
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ ↑H₂.toSubmonoid

Tactic:
· change x * y * x⁻¹ * y⁻¹ ∈ H₂
    apply H₂.mul_mem _ (H₂.inv_mem hy)
    apply hH₂.conj_mem _ hy

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

Goal state before:
pp: case inr.inl.inr.inr
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Trichotomous r
inst✝ : ∀ (i : ι), Std.Trichotomous (s i)
i : ι
a b : α i
hba : s i b a
⊢ Lex r s ⟨i, a⟩ ⟨i, b⟩ ∨ ⟨i, a⟩ = ⟨i, b⟩ ∨ Lex r s ⟨i, b⟩ ⟨i, a⟩

Tactic:
exact Or.inr (Or.inr <| Lex.right _ _ hba)

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

Goal state before:
pp: case of_mul
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), motive ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ motive (↑x * (FreeMonoid.lift Subtype.val) y) ⋯

Tactic:
refine mul_left _ x.prop (FreeMonoid.lift Subtype.val y) _ (ih ?_)

Goal state after:
case of_mul
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : { x // x ∈ s }
y : FreeMonoid { x // x ∈ s }
ih : ∀ (h : (FreeMonoid.lift Subtype.val) y ∈ closure s), motive ((FreeMonoid.lift Subtype.val) y) h
h : (FreeMonoid.lift Subtype.val) (FreeMonoid.of x * y) ∈ closure s
⊢ (FreeMonoid.lift Subtype.val) y ∈ closure s
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
y : ↥(powers x)
⊢ ↑(y ^ (n - 1) * y) = ↑1

Tactic:
obtain ⟨_, k, rfl⟩ := y

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
k : ℕ
⊢ ↑(⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ ^ (n - 1) * ⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩) = ↑1
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = map (s.subtype.coprod t.subtype) (mrange (inl ↥s ↥t)) ⊔ map (s.subtype.coprod t.subtype) (mrange (inr ↥s ↥t))

Tactic:
map_mrange,

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange ((s.subtype.coprod t.subtype).comp (inl ↥s ↥t)) ⊔ map (s.subtype.coprod t.subtype) (mrange (inr ↥s ↥t))
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange s.subtype ⊔ map (s.subtype.coprod t.subtype) (mrange (inr ↥s ↥t))

Tactic:
map_mrange,

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
⊢ s ⊔ t = mrange s.subtype ⊔ mrange ((s.subtype.coprod t.subtype).comp (inr ↥s ↥t))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
h : argmax f tl = none
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
rw [h] at hm
      simp_all

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
⊢ {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})

Tactic:
simp only [Finset.ext_iff, mem_insert, mem_range, mem_filter]

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
⊢ ∀ (a : ℕ), a < ↑(succ (ofNat s n)) ∧ a ∈ s ↔ a = ↑(ofNat s n) ∨ a < ↑(ofNat s n) ∧ a ∈ s
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
f_mono : StrictMonoOn f ↑s
⊢ #s ≤ #t + 1

Tactic:
calc
    s.card = (s.image f).card := (card_image_of_injOn f_mono.injOn).symm
    _ ≤ (insert ⊤ (t.image (↑)) : Finset (WithTop α)).card :=
      card_mono <| image_subset_iff.2 fun x _ =>
          insert_subset_insert _ (image_subset_image <| filter_subset _ _)
            (min_mem_insert_top_image_coe _)
    _ ≤ t.card + 1 := (card_insert_le _ _).trans (Nat.add_le_add_right card_image_le _)

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ map singleton ⟦l⟧ ≤ powerset ⟦l⟧

Tactic:
simp only [powerset_coe, quot_mk_to_coe, coe_le, map_coe]

Goal state after:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map singleton l <+~ List.map ofList l.sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen n l₁ <+ sublistsLen n l₂

Tactic:
by
  induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_
  induction h with
  | slnil => rfl
  | cons a _ IH =>
    refine IH.trans ?_
    rw [sublistsLen_succ_cons]
    apply sublist_append_left
  | cons_cons a s IH => simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Tactic:
by
  apply Iff.trans Multiset.sup_le
  simp only [Multiset.mem_map, and_imp, exists_imp]
  exact ⟨fun k b hb => k _ _ hb rfl, fun k a' b hb h => h ▸ k _ hb⟩

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

Goal state before:
pp: α : Type u_1
s t : Finset α
⊢ s ∈ t.powerset ↔ s ⊆ t

Tactic:
cases s

Goal state after:
case mk
α : Type u_1
t : Finset α
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ { val := val✝, nodup := nodup✝ } ∈ t.powerset ↔ { val := val✝, nodup := nodup✝ } ⊆ t
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s t : Finset α
⊢ s ∈ powersetCard n t ↔ s ⊆ t ∧ #s = n

Tactic:
cases s

Goal state after:
case mk
α : Type u_1
n : ℕ
t : Finset α
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ { val := val✝, nodup := nodup✝ } ∈ powersetCard n t ↔
    { val := val✝, nodup := nodup✝ } ⊆ t ∧ #{ val := val✝, nodup := nodup✝ } = n
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
⊢ ∃ t, ∀ (a : α), f a ≤ t.sup f

Tactic:
refine ⟨t, fun a ↦ ?_⟩

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
⊢ f a ≤ t.sup f