mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ ↑s = Set.univ ↔ s = univ

Tactic:
rw [← coe_univ, coe_inj]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ (s.erase a)ᶜ = insert a sᶜ

Tactic:
ext
  simp only [or_iff_not_imp_left, mem_insert, not_and, mem_compl, mem_erase]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ ∅ = image f s ↔ s = ∅

Tactic:
rw [eq_comm, image_eq_empty]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ ↑k = ↑0

Tactic:
by rw [Nat.eq_zero_of_le_zero h]; rfl

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

Goal state before:
pp: n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : Fin n
⊢ motive i

Tactic:
obtain ⟨i, hi⟩ := i

Goal state after:
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : ℕ
hi : i < n
⊢ motive ⟨i, hi⟩
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
⊢ (ofFn f)[↑i] = b

Tactic:
by simpa using! hfb

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:
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.Fin.Tuple.Basic

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

Tactic:
rw [← cons_succ x p]; rfl

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

Goal state before:
pp: n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p (last (n + 1)) = p (last n)

Tactic:
rw [← cons_succ x p]; rfl

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ y ∈ {x}

Tactic:
rw [card_le_one.1 H y hy x hx, mem_singleton]

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

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ 1

Tactic:
rw [← card_singleton x]

Goal state after:
case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ #{x}
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
h : Fintype ↑Set.univ
⊢ card ↑Set.univ = card α

Tactic:
by
  apply Fintype.card_of_finset'
  simp

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

Goal state before:
pp: case cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
a✝ : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : x ∈+ l₁✝
⊢ x ∈+ y :: l₂✝

Tactic:
| cons y _ IH =>

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

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = append (snoc xs y) ys ∘ Fin.cast ⋯

Tactic:
rw [append_left_snoc]; rfl

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
L : List α
a : α
⊢ (orderedInsert r a L).length = L.length + 1

Tactic:
induction L

Goal state after:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ (orderedInsert r a []).length = [].length + 1

case cons
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a head✝ : α
tail✝ : List α
tail_ih✝ : (orderedInsert r a tail✝).length = tail✝.length + 1
⊢ (orderedInsert r a (head✝ :: tail✝)).length = (head✝ :: tail✝).length + 1
Module: Mathlib.Data.List.Range

Goal state before:
pp: case succ
r : ℕ → ℕ → Prop
n : ℕ
hn : IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ
⊢ IsChain r (range (n + 1)) ↔ ∀ (m : ℕ), m < n + 1 - 1 → r m m.succ

Tactic:
| succ n hn =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
head✝ : α
l : List α
⊢ (head✝ :: l) ×ˢ [] = []

Tactic:
by simp [product_cons, product_nil l]

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:
rotate_eq_rotate',

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

Goal state after:
α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate' (n + 1) = (l ++ [a]).rotate' n
Module: Mathlib.Data.List.Rotate

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

Tactic:
rotate_eq_rotate',

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

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
⊢ (l.rotate n).rotate m = l.rotate (n + m)

Tactic:
rotate_eq_rotate',

Goal state after:
α : Type u
l : List α
n m : ℕ
⊢ (l.rotate n).rotate' m = l.rotate (n + m)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
⊢ (l.rotate n).rotate' m = l.rotate (n + m)

Tactic:
rotate_eq_rotate',

Goal state after:
α : Type u
l : List α
n m : ℕ
⊢ (l.rotate' n).rotate' m = l.rotate (n + m)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n m : ℕ
⊢ (l.rotate' n).rotate' m = l.rotate (n + m)

Tactic:
rotate_eq_rotate',

Goal state after:
α : Type u
l : List α
n m : ℕ
⊢ (l.rotate' n).rotate' m = l.rotate' (n + m)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
⊢ l.rotate l.length = l

Tactic:
rotate_eq_rotate',

Goal state after:
α : Type u
l : List α
⊢ l.rotate' l.length = l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate (l.length * n) = l

Tactic:
rotate_eq_rotate',

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' (l.length * n) = l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
l : List α
⊢ l.rotate' (n + 1) ~ l

Tactic:
| succ n hn =>

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
hn : ∀ {l : List α}, l.rotate n = [] ↔ l = []
l : List α
⊢ l.rotate (n + 1) = [] ↔ l = []

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
s t : Multiset α
n : ℕ
h : s.Nodup
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t

Tactic:
by
  classical simp [← h.le_dedup_iff_le, hn]

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

Goal state before:
pp: case cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.IsChain (flip r) (a :: l)), Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
(by rfl : l = l'.1)

Goal state after:
case cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.IsChain (flip r) (a :: ↑l')), Acc (List.lex_chains r) ⟨a :: ↑l', hl⟩
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.IsChain (flip r) (a :: ↑l')), Acc (List.lex_chains r) ⟨a :: ↑l', hl⟩

Tactic:
clear_value l'

Goal state after:
case cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl' : List.IsChain (flip r) l
l' : List.chains r
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.IsChain (flip r) (a :: ↑l')), Acc (List.lex_chains r) ⟨a :: ↑l', hl⟩
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), (l.rotate n).reverse.rotate n = l.reverse
l : List α
⊢ (l.rotate (n + 1)).reverse.rotate (n + 1) = l.reverse

Tactic:
| succ n hn =>

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

Goal state before:
pp: case succ
α : Type u
β : Type u_1
f : α → β
n : ℕ
hn : ∀ (l : List α), map f (l.rotate n) = (map f l).rotate n
l : List α
⊢ map f (l.rotate (n + 1)) = (map f l).rotate (n + 1)

Tactic:
| succ n hn =>

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

Goal state before:
pp: α : Type u_1
l : List α
x : α × α
⊢ x ∈ l.offDiag ↔ ∃ i x_1 j x_2, i ≠ j ∧ l[i] = x.fst ∧ l[j] = x.snd

Tactic:
rcases x with ⟨x, y⟩
  simp only [offDiag, exists_mem_zipIdx, mem_eraseIdx_iff_getElem, mem_flatMap, mem_map,
    Nat.zero_add, Prod.ext_iff, ← exists_and_right, exists_and_left, @exists_comm α, and_assoc,
    exists_eq_left', ne_comm]

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

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (insert a s).pi t = (t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t)

Tactic:
by
  apply eq_of_veq
  rw [← (pi (insert a s) t).2.dedup]
  refine
    (fun s' (h : s' = a ::ₘ s.1) =>
        (?_ :
          dedup (Multiset.pi s' fun a => (t a).1) =
            dedup
              ((t a).1.bind fun b =>
                dedup <|
                  (Multiset.pi s.1 fun a : α => (t a).val).map fun f a' h' =>
                    Multiset.Pi.cons s.1 a b f a' (h ▸ h'))))
      _ (insert_val_of_notMem ha)
  subst s'; rw [pi_cons]
  congr; funext b
  exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

Tactic:
· rw [Pi.cons_ne _ h]
      apply hf'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set β
f : α → β
⊢ MapsTo f s (⋂ i, ⋂ j, t i j) ↔ ∀ (i : ι) (j : κ i), MapsTo f s (t i j)

Tactic:
simp only [mapsTo_iInter]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: α : Type u_5
β : α → Type u_6
γ : (a : α) → β a → Type u_7
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : (a : α) → (b : β a) → One (γ a b)
a : α
b : β a
x : γ a b
⊢ uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle ⟨a, b⟩ x

Tactic:
by
  rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
N N' : Submonoid M
⊢ N ⊔ N' = closure (↑N ∪ ↑N')

Tactic:
simp_rw [closure_union, closure_eq]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s / t) = ⇑m '' (⇑m ⁻¹' s / ⇑m ⁻¹' t)

Tactic:
by
    rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
p q : Subgroup G
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
by
    obtain ⟨⟨⟨hp, _⟩, _⟩, _⟩ := p
    obtain ⟨⟨⟨hq, _⟩, _⟩, _⟩ := q
    congr

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ H ≠ ⊥

Tactic:
nontrivial_iff_exists_ne_one,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ H ≠ ⊥
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H H' : Subgroup G
⊢ H ⊔ H' = closure (↑H ∪ ↑H')

Tactic:
simp_rw [closure_union, closure_eq]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f (x * y) = f x * f y

Tactic:
by rw [map_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → ℕ → α
⊢ ⨆ n, f (unpair n).1 (unpair n).2 = ⨆ i, ⨆ j, f i j

Tactic:
rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ K ≤ normalizer ↑H

Tactic:
rw [← subgroupOf_eq_top, subgroupOf_normalizer_eq h, normalizer_eq_top_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x ↦ a * x) '' s ∪ {b} * s = a • s ∪ b • s

Tactic:
singleton_mul

Goal state after:
α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x ↦ a * x) '' s ∪ (fun x ↦ b * x) '' s = a • s ∪ b • s
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Tactic:
rw [toLex_lt_toLex]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x y : α × β
⊢ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2 ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
h : card ↥S ≤ 1
x : M
hx : x ∈ S
⊢ x = 1

Tactic:
by
      simpa [Subtype.ext_iff] using card_le_one_iff.1 h ⟨x, hx⟩ 1

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 : ℕ
x : ↥(powers x✝)
⊢ x ^ Int.negSucc m = (x ^ ↑m.succ) ^ (n - 1)

Tactic:
change x ^ (Int.natMod _ n) = (x ^ (Int.natMod _ n)) ^ (n - 1)
    ext
    obtain ⟨_, k, rfl⟩ := x
    simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]
    rw [Int.negSucc_eq, ← Int.natCast_succ, ← Int.add_mul_emod_self_right (b := (m + 1 : ℕ))]
    nth_rw 1 [← mul_one ((m + 1 : ℕ) : ℤ)]
    rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]; norm_cast
    simp only [Int.toNat_natCast]
    rw [mul_comm, pow_mul, ← pow_eq_pow_mod _ hx, mul_comm k, mul_assoc, pow_mul _ (_ % _),
      ← pow_eq_pow_mod _ hx, pow_mul, pow_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (s.disjSum t).card = s.card + t.card

Tactic:
disjSum,

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (map inl s + map inr t).card = s.card + t.card
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x

Tactic:
disjSum,

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ map inl s + map inr t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x
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:
disjSum,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (map inl s + map inr t) = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
this : ∃ a ∈ decodeSum n, encodeSum a = bit n.bodd n.div2
⊢ ∃ a ∈ decode n, encode a = n

Tactic:
simpa [bit_bodd_div2]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u.toLeft = s ∧ u.toRight = t
⊢ u = s.disjSum t

Tactic:
simp [← h, toLeft_disjSum_toRight]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f (s.disjSum t).val) =
    op (Multiset.fold op b₁ (Multiset.map (fun x ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun x ↦ f (inr x)) t.val))

Tactic:
disjSum,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f (s.val.disjSum t.val)) =
    op (Multiset.fold op b₁ (Multiset.map (fun x ↦ f (inl x)) s.val))
      (Multiset.fold op b₂ (Multiset.map (fun x ↦ f (inr x)) t.val))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum

Tactic:
· simp [IH h]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ x ⊓ y = x

Tactic:
← hf.eq_iff,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ f (x ⊓ y) = f x
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap (l₁.zip []) = [].zip l₁

Tactic:
zip_nil_right

Goal state after:
α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap [] = [].zip l₁
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip

Tactic:
have := Classical.decEq α
  simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]
  exact (powersetAux_perm p).map _

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : ι → α
inst✝ : Finite ι
⊢ Finite ↑(range f)

Tactic:
classical
  have := Fintype.ofFinite (PLift ι)
  infer_instance

Goal state after:
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:
by
  simp only [← top_le_iff]
  exact Finset.le_sup_iff bot_lt_top

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

Goal state before:
pp: α : Type u
ι : Sort u_1
inst✝ : Subsingleton ι
s : ι → Set α
⊢ (⋃ i, s i).Finite ↔ ∀ (i : ι), (s i).Finite

Tactic:
rw [← iUnion_plift_down, finite_iUnion_iff _root_.Subsingleton.pairwise]
  simp [PLift.forall, Finite.of_subsingleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

Tactic:
rcases isEmpty_or_nonempty β

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : IsEmpty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝ : Nonempty β
⊢ ⨆ p, f p = ⨆ b, ⨆ c, f (b, c)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ {a, b} \ {a} ⊆ {b}

Tactic:
sdiff_singleton_subset_iff

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ⩿ b
⊢ {a, b} ⊆ {a, b}
Module: Mathlib.Order.Cover

Goal state before:
pp: case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t \ {x} ⊆ s

Tactic:
sdiff_singleton_subset_iff

Goal state after:
case neg
α : Type u_1
x : α
s t : Set α
hst : s ⊆ t
h2t : t ⊆ insert x s
h : x ∉ t
⊢ t ⊆ insert x s
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ s.preimage f hf ⊆ t

Tactic:
← coe_subset,

Goal state after:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(s.preimage f hf) ⊆ ↑t
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
⊢ sInf {m | p m} + n = sInf {m | p (m - n)}

Tactic:
suffices h₁ : n ≤ sInf {m | p (m - n)} by
    convert! sInf_add h₁
    simp_rw [Nat.add_sub_cancel_right]
  obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h
  refine
    le_csInf ⟨m + n, ?_⟩ fun b hb ↦
      le_of_not_gt fun hbn ↦
        ne_of_mem_of_not_mem ?_ (notMem_of_lt_sInf h) (Nat.sub_eq_zero_of_le hbn.le)
  · dsimp
    rwa [Nat.add_sub_cancel_right]
  · exact hb

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ico a b = ∅ ↔ ¬a < b

Tactic:
Set.Ico_eq_empty_iff

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ¬a < b ↔ ¬a < b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a₁ a₂ b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : a₁ < a₂
⊢ ↑(Ico a₂ b) ⊆ ↑(Ioo a₁ b)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂

Tactic:
← coe_subset,

Goal state after:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ ↑(Ioc a b₁) ⊆ ↑(Ioo a b₂)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂

Tactic:
rw [← coe_subset, coe_Ioc, coe_Ioo]
  exact Set.Ioc_subset_Ioo_right h

Goal state after: