mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
u : Multiset α
v : Multiset β
huv : Rel r u v
a✝ : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
hab : r a✝ b✝
hst : Rel r as✝ bs✝
ih : Rel r (as✝ + u) (bs✝ + v)
⊢ Rel r (a✝ ::ₘ as✝ + u) (b✝ ::ₘ bs✝ + v)

Tactic:
| cons hab hst ih =>

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
t : α
⊢ map f ∘ cons t = cons (f t) ∘ map f

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList = [] ↔ s = 0

Tactic:
← coe_eq_zero,

Goal state after:
α : Type u_1
s : Multiset α
⊢ ↑s.toList = 0 ↔ s = 0
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ ⟦b⟧ ∧ p a
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
⊢ ⟨x, px⟩ = ⟨y, py⟩

Tactic:
rcases hp with ⟨z, ⟨_z_mem_l, _pz⟩, z_unique⟩

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
z : α
z_unique : ∀ (y : α), (fun a ↦ a ∈ ⟦b⟧ ∧ p a) y → y = z
_z_mem_l : z ∈ ⟦b⟧
_pz : p z
⊢ ⟨x, px⟩ = ⟨y, py⟩
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∪ t) = max (count a s) (count a t)

Tactic:
by
  simp [(· ∪ ·), union, Nat.sub_add_eq_max]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
n : l.Nodup
⊢ (↑l).Nodup

Tactic:
rwa [Multiset.coe_nodup]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.toList.toFinset = s

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ ↑(cons a s h) = insert a ↑s

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ⊆ insert a t ↔ s ⊆ t

Tactic:
by
  rw [subset_insert_iff, erase_eq_of_notMem h]

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x ↦ x ∉ t₁) s) → x ∈ t₂ \ t₁

Tactic:
simp only [coe_filter, Set.mem_ofPred_eq, and_imp]

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ s → x ∉ t₁ → x ∈ t₂ \ t₁
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
f : α → β
inst✝² : Fintype β
inst✝¹ : DecidablePred fun y ↦ ∃ x, f x = y
inst✝ : DecidableEq β
⊢ {y | ∃ x, f x = y} = image f univ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map { toFun := ⇑f ∘ ⇑g, inj' := ⋯ } s = map { toFun := ⇑g' ∘ ⇑f', inj' := ⋯ } s

Tactic:
Function.comp_def,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map { toFun := fun x ↦ f (g x), inj' := ⋯ } s = map { toFun := fun x ↦ g' (f' x), inj' := ⋯ } s
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∩ t)
⊢ (s ∩ t).toFinset = s.toFinset ∩ t.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ∪ t)
⊢ (s ∪ t).toFinset = s.toFinset ∪ t.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s \ t)
⊢ (s \ t).toFinset = s.toFinset \ t.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝³ : DecidableEq α
inst✝² : Fintype ↑s
inst✝¹ : Fintype α
inst✝ : Fintype ↑sᶜ
⊢ sᶜ.toFinset = s.toFinsetᶜ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype ↑∅
⊢ ∅.toFinset = ∅

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
⊢ univ.toFinset = Finset.univ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
⊢ {x | p x}.toFinset = filter p Finset.univ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype β
f : β → α
inst✝ : Fintype ↑(range f)
⊢ (range f).toFinset = Finset.image f Finset.univ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Fintype ↑{a}
⊢ {a}.toFinset = {a}

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
a : α
s : Set α
inst✝¹ : Fintype ↑(insert a s)
inst✝ : Fintype ↑s
⊢ (insert a s).toFinset = insert a s.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
⊢ (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.predAbove i.rev = (p.rev.predAbove i).rev

Tactic:
rw [predAbove_rev_left, rev_rev]

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ (p.predAbove i).rev = p.rev.predAbove i.rev

Tactic:
rw [predAbove_rev_left, rev_rev]

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
y : Fin m
x✝ : y ∈ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding)
x : Fin n
hx : ((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) x = y
⊢ y ∈ {i | m ≤ ↑i + n}

Tactic:
by simp [← hx]; lia

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ Set.InjOn f ↑s

Tactic:
have : (s.1.map f).dedup = s.1.map f := by
    refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
    simp only [H, Multiset.card_map, le_rfl]

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).dedup = Multiset.map f s.val
⊢ Set.InjOn f ↑s
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin n
⊢ ↑↑↑a = ↑a.castSucc

Tactic:
exact val_cast_of_lt (Nat.lt_succ_of_lt a.is_lt)

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

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hp : p ≠ 0
⊢ (p.pred hp).predAbove i = i.pred ⋯

Tactic:
by
  rw [predAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
⊢ map (⇑e) univ.val = univ.val

Tactic:
← congr_arg Finset.val (Finset.map_univ_equiv e),

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
⊢ map (⇑e) univ.val = (Finset.map e.toEmbedding univ).val
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
⊢ Injective (cons x₀ x)

Tactic:
intro i j

Goal state after:
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
hx₀ : ¬x₀ ∈ Set.range x
hx : Injective x
i j : Fin (n + 1)
⊢ cons x₀ x i = cons x₀ x j → i = j
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x

Tactic:
intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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

Goal state before:
pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x

Tactic:
intro
      simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_ofPred]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
nd : l.Nodup
h : ∀ (x : α), x ∈ l
i : Fin l.length
⊢ (fun a ↦ ⟨idxOf a l, ⋯⟩) ((fun i ↦ l.get i) i) = i

Tactic:
simp [nd]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ #s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Tactic:
by
  rw [← Fintype.card_coe] at h
  rcases nonempty_of_card_le h with ⟨f⟩
  exact ⟨f.trans (Embedding.subtype _), by simp [Set.range_subset_iff]⟩

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∩ t).Finite
⊢ h.toFinset = hs.toFinset ∩ ht.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
⊢ h.toFinset = hs.toFinset ∪ ht.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s \ t).Finite
⊢ h.toFinset = hs.toFinset \ ht.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hs : s.Finite
h : sᶜ.Finite
⊢ h.toFinset = hs.toFinsetᶜ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝ : DecidableEq β
f : α → β
hs : s.Finite
h : (f '' s).Finite
⊢ h.toFinset = Finset.image f hs.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype β
f : β → α
h : (range f).Finite
⊢ h.toFinset = Finset.image f Finset.univ

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl : ∀ (a : α), a ∈ x :: xs → ∀ (b : α), b ∈ x :: xs → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
simp_rw [List.forall_mem_cons, forall_and] at hl
    simp_rw [List.map, insertionSort_cons]
    rw [List.map_orderedInsert _ s, ih hl.2.2]
    · simpa only [mem_insertionSort] using hl.2.1
    · simpa only [mem_insertionSort] using hl.1.2

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op a b) s

Tactic:
by
  rw [fold_cons'_right, hc.comm]

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
⊢ b' ∈ List.orderedInsert r a l → r b b'

Tactic:
bm

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm : b' ∈ List.orderedInsert r a l
⊢ r b b'
Module: Mathlib.Data.List.Rotate

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

Tactic:
by simp [rotate]

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ [].rotate n = []

Tactic:
by simp [rotate]

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

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

Tactic:
by simp [rotate]

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

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

Tactic:
rw [rotate_eq_rotate', rotate'_length_mul]

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

Goal state before:
pp: case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m + n % l.length < l.length
⊢ l[n % l.length + m]? = l[(m + n % l.length) % l.length]?

Tactic:
rw [mod_eq_of_lt hm, Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
wf : WellFounded r
h : List.IsChain r l
⊢ List.Pairwise rᶜ l.reverse

Tactic:
refine List.pairwise_iff_forall_infix.mpr fun l' hne hsub ↦ ?_
  have := wf.asymmetricₙ (by grind) <| h.infix <| l.reverse_reverse ▸ hsub.reverse
  simpa

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ op (unop l.prod) = op (map unop l).reverse.prod

Tactic:
op_unop,

Goal state after:
M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ l.prod = op (map unop l).reverse.prod
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝ : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
hab : Rel r a✝ b✝
hst : Rel (Rel r) as✝ bs✝
ih : Rel r as✝.join bs✝.join
⊢ Rel r (a✝ ::ₘ as✝).join (b✝ ::ₘ bs✝).join

Tactic:
| cons hab hst ih =>

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
this : ∀ (a : α), ∃ l, f a = ↑l
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
choose f' h' using this

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}

Tactic:
by
  simp only [SProd.sprod, product, bind_singleton, map_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
⊢ (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' f ⁻¹' sᶜ = sᶜ ↔ (range f)ᶜ ⊆ s

Tactic:
image_preimage_eq_iff,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ sᶜ ⊆ range f ↔ (range f)ᶜ ⊆ s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
⊢ s ×ˢ ⋃ i, t i = ⋃ i, s ×ˢ t i

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
⊢ (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
⊢ ⋃ x, s x.1 ×ˢ t x.2 = (⋃ i, s i) ×ˢ ⋃ i, t i

Tactic:
by
  ext
  simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ comap f f.range = ⊤

Tactic:
by
  ext
  simp

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ Subgroup.map (powMonoidHom n) (↑e).range = (powMonoidHom n).range

Tactic:
e.range_eq_top,

Goal state after:
M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ Subgroup.map (powMonoidHom n) ⊤ = (powMonoidHom n).range
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

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

Tactic:
op_unop,

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ closure s = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

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

Tactic:
op_unop,

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ closure s = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.Algebra.Group.Subgroup.MulOpposite

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

Tactic:
op_unop,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ normalizer ↑H = (normalizer ↑H.unop).op
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
simp [coe_prod]

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

Goal state before:
pp: m n : ℕ
a b : Bool
h : m < n
⊢ bit a m < 2 * n

Tactic:
by cases a <;> dsimp [bit] <;> lia

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ (closure s).unop.op = (closure (MulOpposite.op ⁻¹' s)).op

Tactic:
op_unop,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = (closure (MulOpposite.op ⁻¹' s)).op
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
simp [coe_prod]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝¹ : Monoid M
N : Type u_5
inst✝ : Monoid N
g : M →* N
f : α → M
⊢ g.comp (lift f) = lift (⇑g ∘ f)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : 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.Total (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b ∨ Lex r s b a

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩
    obtain hij | rfl | hji := trichotomous_of r i j
    · exact Or.inl (Lex.left _ _ hij)
    · obtain hab | hba := total_of (s i) a b
      · exact Or.inl (Lex.right _ _ hab)
      · exact Or.inr (Lex.right _ _ hba)
    · exact Or.inr (Lex.left _ _ hji)

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

Goal state before:
pp: case inr.inl.inr.inl
ι : 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 : α i
⊢ Lex r s ⟨i, a⟩ ⟨i, a⟩ ∨ ⟨i, a⟩ = ⟨i, a⟩ ∨ Lex r s ⟨i, a⟩ ⟨i, a⟩

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.inl rfl)

Goal state after:
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⟩
Module: Mathlib.Logic.Embedding.Set

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

Tactic:
| inl x =>

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
a b : Lex (α × β)
this : DecidableLT (Lex (α × β))
⊢ compare a b = compareOfLessAndEq a b

Tactic:
have : Std.LawfulBEqOrd (α ×ₗ β) := ⟨by
      simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq]⟩

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
a b : Lex (α × β)
this✝ : DecidableLT (Lex (α × β))
this : Std.LawfulBEqOrd (Lex (α × β))
⊢ compare a b = compareOfLessAndEq a b
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case refine_3
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
⊢ (∃ (hm : x ∈ ⨆ i, S i), motive x hm) →
    (∃ (hm : y ∈ ⨆ i, S i), motive y hm) → ∃ (hm : x * y ∈ ⨆ i, S i), motive (x * y) hm

Tactic:
rintro ⟨_, Cx⟩ ⟨_, Cy⟩

Goal state after:
case refine_3
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, S i
x y : M
w✝¹ : x ∈ ⨆ i, S i
Cx : motive x w✝¹
w✝ : y ∈ ⨆ i, S i
Cy : motive y w✝
⊢ ∃ (hm : x * y ∈ ⨆ i, S i), motive (x * y) hm
Module: Mathlib.Data.Nat.Order.Lemmas

Goal state before:
pp: p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
this : 0 < k
⊢ p (k - 1 + 1)

Tactic:
Nat.sub_add_cancel this

Goal state after:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
this : 0 < k
⊢ p k
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ a ≤ maximum_of_length_pos w

Tactic:
simp only [le_maximum_of_length_pos_iff]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ ↑a ≤ l.maximum
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

Tactic:
obtain - | ⟨-, h⟩ | ⟨-, h⟩ := h
    · exact Or.inl h
    · exact Or.inr ⟨_, h, rfl⟩

Goal state after: