mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ ∀ (x : β), x ∈ ↑(image f s) ↔ x ∈ f '' ↑s

Tactic:
simp only [mem_coe, mem_image, Set.mem_image, implies_true]

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
ha : a ∉ s
⊢ (cons a s ha).attach = cons ⟨a, ⋯⟩ (map { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach) ⋯

Tactic:
ext ⟨x, hx⟩

Goal state after:
α : Type u_1
a : α
s : Finset α
ha : a ∉ s
x : α
hx : x ∈ cons a s ha
⊢ ⟨x, hx⟩ ∈ (cons a s ha).attach ↔ ⟨x, hx⟩ ∈ cons ⟨a, ⋯⟩ (map { toFun := fun x ↦ ⟨↑x, ⋯⟩, inj' := ⋯ } s.attach) ⋯
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).attach = insert ⟨a, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)

Tactic:
ext ⟨x, hx⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a x : α
hx : x ∈ insert a s
⊢ ⟨x, hx⟩ ∈ (insert a s).attach ↔ ⟨x, hx⟩ ∈ insert ⟨a, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
lift t to Finset s using h

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = image (f ∘ Subtype.val) t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
⊢ t ⊆ image f s ↔ ∃ s' ⊆ s, image f s' = t

Tactic:
simp only [← coe_subset, coe_image, subset_set_image_iff]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + (Fintype.card α - #s) = Fintype.card α

Tactic:
← Nat.add_sub_assoc (card_le_univ s),

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #s + Fintype.card α - #s = Fintype.card α
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1.refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ b lr = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))

Tactic:
simp [castAdd_natAdd]

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

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
⊢ ∀ (i : Fin n), append x₀ x (natAdd 1 i) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (natAdd 1 i)

Tactic:
intro i
    rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
    exact Fin.cons_succ _ _ _

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

Goal state before:
pp: case mpr
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ l <+ l'

Tactic:
exact sublist_of_orderEmbedding_getElem?_eq f hf

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

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
s : Finset α
hs : (↑s).Finite
⊢ motive (↑s) hs

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simpa
  | cons a s ha ih => simpa using @insert a s ha (Set.toFinite _) (ih _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))

Tactic:
ha.assoc,

Goal state after:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (f a) (op (op (fold op u₁ (map f b)) (g a)) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))

Tactic:
ha.assoc,

Goal state after:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (f a) (op (fold op u₁ (map f b)) (op (g a) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons.cons_cons
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a : α
tail✝ c : List α
ih : c.erase a <+ insertionSort r tail✝
hs : Pairwise r c
l₁✝ : List α
hc : a :: l₁✝ ~ c
h : l₁✝ <+ tail✝
hm : a ∈ c
he : orderedInsert r a (c.erase a) = c
⊢ c <+ insertionSort r (a :: tail✝)

Tactic:
exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedLT ↔ l.SortedGT

Tactic:
grind [OrderDual.ofDual_lt_ofDual]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.ofDual) l).SortedGT ↔ l.SortedLT

Tactic:
grind [OrderDual.ofDual_lt_ofDual]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ IsChain R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b

Tactic:
refine ⟨fun h _ _ _ _ eq => (isChain_append_cons_cons.mp (eq ▸ h)).2.1, ?_⟩
  induction l using twoStepInduction with
  | nil | singleton => grind
  | cons_cons head head' tail _ ih =>
    refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]

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

Goal state before:
pp: case succ.cons
α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ (x :: l).reverse.length - n % (x :: l).reverse.length ≤ (x :: l).reverse.length

Tactic:
exact Nat.sub_le _ _

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

Goal state after:
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ((hd :: tl).rotate n).rotate ((hd :: tl).length * n - n) = hd :: tl
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case empty
n : ℤ
⊢ prod 0 % n = (map (fun x ↦ x % n) 0).prod % n

Tactic:
simp [Int.mul_emod, *]

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

Goal state before:
pp: case cons
n a✝¹ : ℤ
s✝ : Multiset ℤ
a✝ : s✝.prod % n = (map (fun x ↦ x % n) s✝).prod % n
⊢ (a✝¹ ::ₘ s✝).prod % n = (map (fun x ↦ x % n) (a✝¹ ::ₘ s✝)).prod % n

Tactic:
simp [Int.mul_emod, *]

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

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : ExistsAddOfLE M
inst✝³ : AddLeftMono M
inst✝² : AddLeftReflectLE M
inst✝¹ : Sub M
inst✝ : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ map (fun i ↦ f i - g i + g i) l = map f l

Tactic:
exact map_congr rfl fun x hx => tsub_add_cancel_of_le <| hfg _ hx

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

Goal state before:
pp: n : ℕ
⊢ n.choose 0 = 1

Tactic:
cases n <;> rfl

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

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

pp: case H
n : ℕ
⊢ 0 < 2

Tactic:
cases n <;> rfl

Goal state after:
case H
n : ℕ
⊢ 0 < 2
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
⊢ l.offDiag.Nodup

Tactic:
nodup_iff_count_le_one

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
this : DecidableEq α := Classical.decEq α
⊢ ∀ (a : α × α), List.count a l.offDiag ≤ 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

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:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ ∃ a, f a = x

Tactic:
obtain ⟨i, hi⟩ :=
    Set.mem_iUnion.mp
      (show x ∈ Set.iUnion U by rw [hU]; trivial)

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
i : ι
hi : x ∈ U i
⊢ ∃ a, f a = x
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

Tactic:
rintro ⟨u, rfl⟩

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Set α)ˣ
⊢ ∃ a, ↑u = {a} ∧ IsUnit a
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H : Subgroup G
S : Set G
a : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
n : G
⊢ n ∈ S ↔ a⁻¹ * n * a⁻¹⁻¹ ∈ S

Tactic:
by
    rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ closure {1} = ⊥

Tactic:
by
  simp [eq_bot_iff_forall, mem_closure_singleton]

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

Goal state before:
pp: case refine_1.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
hx : x ∈ closure (⋃ i, ⋃ (_ : p i), ↑(K i))
⊢ ∃ i, p i ∧ 1 ∈ K i

Tactic:
exact ⟨i, hp, (K i).one_mem⟩

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

Goal state before:
pp: case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)

Tactic:
simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]

Goal state after:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ a₁ * a₁ + (a₁ + b) < a₂ * a₂ + (a₂ + b)
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ 1 ≤ n / 2

Tactic:
Nat.le_div_iff_mul_le

Goal state after:
n : ℕ
h : 2 ≤ n
⊢ 1 * 2 ≤ n

n : ℕ
h : 2 ≤ n
⊢ 0 < 2
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ zpowers g ≤ H ↔ g ∈ H

Tactic:
zpowers_eq_closure,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ closure {g} ≤ H ↔ g ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G ≃* G'
H : Subgroup G
⊢ (map (↑f) H).Normal ↔ H.Normal

Tactic:
rw [map_equiv_eq_comap_symm, normal_comap_iff_of_surjective f.symm.surjective]

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G ≃* G'
H : Subgroup G
⊢ (map (↑f) H).Normal ↔ H.Normal

Tactic:
by
  rw [map_equiv_eq_comap_symm, normal_comap_iff_of_surjective f.symm.surjective]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

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

Tactic:
· simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ closure {1} = ⊥

Tactic:
by
  simp [eq_bot_iff_forall, mem_closure_singleton]

Goal state after:
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
m k : ℕ
⊢ x ^ (k * (-↑m.succ % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
← Int.add_mul_emod_self_right (b := (m + 1 : ℕ))

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
m k : ℕ
⊢ x ^ (k * ((-↑m.succ + ↑(m + 1) * ↑n) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (s.disjSum t) = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t

Tactic:
simp_rw [disjSum, map_add, map_map, Function.comp_def]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝ : Infinite ↑s
x : ↑s
h : ¬∃ n, ↑x + n + 1 ∈ s
this : ∀ a ∈ s, a < ↑x + 1
⊢ ∀ a ∈ Multiset.filter (fun x ↦ x ∈ s) (Multiset.range (↑x).succ), a ∈ s

Tactic:
by simp [-Multiset.range_succ]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Set.range (Subtype.val ∘ ofNat s) = s

Tactic:
Set.range_comp Subtype.val,

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Subtype.val '' Set.range (ofNat s) = s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = sublistsAux a r ++ flatMap (fun l ↦ [l, a :: l]) [l]

Tactic:
flatMap_singleton,

Goal state after:
α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = sublistsAux a r ++ [l, a :: l]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++
      (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range tl.length) ++
        flatMap (fun a ↦ sublistsLen (a + 1) tl) [tl.length]) ~
    tl.sublists'

Tactic:
flatMap_singleton,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range tl.length) ++ sublistsLen (tl.length + 1) tl) ~
    tl.sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
have := insert_erase_invOn.2.injOn (notMem_subset hi ha) (notMem_subset hj ha)

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
this : insert a i = insert a j → i = j
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ b ∈ powersetCard n.succ u, id b ⊆ u

Tactic:
mem_powersetCard

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ (b : Finset α), b ⊆ u ∧ #b = n.succ → id b ⊆ u
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: ι : Type u_5
α : Type u_7
inst✝² : LinearOrder α
inst✝¹ : BoundedOrder α
inst✝ : Nontrivial α
s : Finset ι
f : ι → α
⊢ ⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b

Tactic:
exact Finset.le_sup_iff bot_lt_top

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
p : α → Prop
hp : ∀ (a₁ : α), p a₁ → ∀ (a₂ : α), p a₂ → p (a₁ ⊔ a₂)
hs : ∀ b ∈ s, p (f b)
⊢ p (s.sup' H f)

Tactic:
change @WithBot.recBotCoe α (fun _ => Prop) True p ↑(s.sup' H f)
  rw [coe_sup']
  refine sup_induction trivial (fun a₁ h₁ a₂ h₂ ↦ ?_) hs
  match a₁, a₂ with
  | ⊥, _ => rwa [bot_sup_eq]
  | (a₁ : α), ⊥ => rwa [sup_bot_eq]
  | (a₁ : α), (a₂ : α) => exact hp a₁ h₁ a₂ h₂

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 : β → α
inst✝¹ : One α
inst✝ : IsBotOneClass α
hs : s.Nonempty
⊢ s.sup' hs f = 1 ↔ ∀ i ∈ s, f i = 1

Tactic:
by
  simp [sup'_eq_sup]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : LinearOrder α
s : Finset ι
f : ι → α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
g : α → β
mono_g : Monotone g
H : s.Nonempty
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)

Tactic:
exact Finset.apply_sup'_eq_sup'_comp H g (fun x y ↦ Monotone.map_sup mono_g x y)

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
⊢ sSup {a} = a

Tactic:
csSup_singleton

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
⊢ a = a
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

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

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
· have : Nonempty <| Exists p := ⟨h⟩
    refine ciSup_le fun ⟨i, hi⟩ ↦ le_ciSup₂ (f := fun _ _ ↦ _) ⟨f ⟨i, hi⟩, ?_⟩ i hi
    rintro _ ⟨_, ⟨j, rfl⟩, ⟨hj, rfl⟩⟩
    rfl

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_3
β : (i : ι) → α i → Type u_7
s : Set ι
t : (i : ι) → Set (α i)
u : (p : (i : ι) × α i) → Set (β p.fst p.snd)
x : (x : ι) → (y : α x) → β x y
⊢ (∀ (i : (i : ι) × α i), i.fst ∈ s → i.snd ∈ t i.fst → Sigma.uncurry x i ∈ u i) ↔
    ∀ i ∈ s, ∀ i_1 ∈ t i, x i i_1 ∈ u ⟨i, i_1⟩

Tactic:
exact ⟨fun h i hi j hj ↦ h ⟨i, j⟩ hi hj, fun h p hp1 hp2 ↦ h p.1 hp1 p.2 hp2⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (∃ a ∉ s, insert a s = t) → s ⋖ t

Tactic:
rintro ⟨a, ha, rfl⟩; exact covBy_insert ha

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨆ x, ↑(f x) = ⊤ ↔ ¬BddAbove (range f)

Tactic:
rw [iSup_eq_top, not_bddAbove_iff]

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (∀ b < ⊤, ∃ i, b < ↑(f i)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x y : α
inst✝ : PartialOrder α
hy : P y
hP : ∀ ⦃x : α⦄, P x → y ≤ x
⊢ x = y → Minimal P x

Tactic:
by rintro rfl; exact ⟨hy, fun z hz _ ↦ hP hz⟩

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

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
rw [← coe_ssubset, coe_Icc, coe_Icc]

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂

Tactic:
rw [← coe_ssubset, coe_Icc, coe_Icc]

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
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
x : α
hx : x ∈ Ico ↑a ↑b
⊢ p x

Tactic:
rw [mem_Ico] at 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 : ↑a ≤ x ∧ x < ↑b
⊢ p x
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ico a b) = #(Icc a b) - 1

Tactic:
by
  by_cases h : a ≤ b
  · rw [Icc_eq_cons_Ico h, card_cons]
    exact (Nat.add_sub_cancel _ _).symm
  · rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ≠ b ∧ a✝ ∈ Iic b ↔ a✝ ∈ Iio b

Tactic:
mem_Iic,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ≠ b ∧ a✝ ≤ b ↔ a✝ ∈ Iio b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ = b ∨ a✝ ∈ Iio b ↔ a✝ ∈ Iic b

Tactic:
mem_Iic,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ = b ∨ a✝ ∈ Iio b ↔ a✝ ≤ b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Group α
inst✝ : MulDistribMulAction M α
x✝¹ : α
ha : x✝¹ ∈ (submonoid M α).carrier
x✝ : M
⊢ x✝ • x✝¹⁻¹ = x✝¹⁻¹

Tactic:
rw [smul_inv', ha]

Goal state after: