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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)

Tactic:
]

Goal state after:
α : Type u_1
s✝¹ : List α
a : α
t : List α
o : s✝¹ = [] ∨ ∃ l, l ∈ t.inits ∧ a :: l = s✝¹
s✝ r : List α
hr : r ∈ t.inits
hs : a :: r = s✝
s : List α
ht : r ++ s = t
⊢ a :: r <+: a :: (r ++ s)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
h : a ∈ s
ht : ndinsert a s = s
⊢ s.attach = s.attach

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = a :: s

Tactic:
]

Goal state after:
α : Type u_1
s✝ : List α
a : α
t : List α
mi : s✝ <+: a :: t
b : α
s r : List α
hr : b :: s ++ r = a :: t
ba : b ≍ a
st : s ++ r ≍ t
⊢ ∃ l, l ∈ t.inits ∧ a :: l = a :: s
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : a ::ₘ s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : a ::ₘ s = t
h : ¬a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ ¬a ∈ s ∧ _root_.Disjoint t s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse

Tactic:
]

Goal state after:
α : Type u_1
l : List α
⊢ l.reverse.inits = (map reverse (map reverse l.reverse.inits).reverse).reverse
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse

Tactic:
]

Goal state after:
α : Type u_1
l : List α
⊢ l.reverse.tails = (map reverse (map reverse l.reverse.tails).reverse).reverse
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s.ndinter t).Nodup

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s.ndinter t).Nodup
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse

Tactic:
]

Goal state after:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.tails).reverse = l.reverse.tails.reverse
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.ndinter t ⊆ 0 ↔ _root_.Disjoint s t
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse

Tactic:
]

Goal state after:
α : Type u_1
l : List α
⊢ map reverse (map reverse l.reverse.inits).reverse = l.reverse.inits.reverse
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ↑a✝ = ↑a✝

Tactic:
]

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s.val = {a}.val

Tactic:
]

Goal state after:
α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s.val = {a}.val
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s t : Finset α
⊢ (∀ ⦃a : α⦄, a ∈ t → a ∉ s) ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s

Tactic:
]

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

Goal state before:
pp: α : Type u_2
s t : Finset α
x✝ : α
⊢ x✝ ∈ s ∧ x✝ ∈ t ↔ x✝ ∈ s ∧ x✝ ∈ t

Tactic:
]

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

Goal state before:
pp: α : Type u_2
a b : α
⊢ ¬a = b ↔ a ≠ b

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ n ::ₘ ↑(List.range n) = n ::ₘ ↑(List.range n)

Tactic:
]

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

Goal state before:
pp: a : ℕ
m : Multiset ℕ
⊢ ∀ {a_1 : ℕ}, a_1 ∈ range a → ¬a_1 ∈ map (fun x ↦ a + x) m

Tactic:
]

Goal state after:
a : ℕ
m : Multiset ℕ
⊢ ∀ {a_1 : ℕ}, a_1 ∈ range a → ¬a_1 ∈ map (fun x ↦ a + x) m
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False

Tactic:
]

Goal state after:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x ↦ a + x) m
⊢ False
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a b : ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) (range b))

Tactic:
]

Goal state after:
a b : ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) (range b))
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ ↑s = {a} ∨ s.Nontrivial

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ ↑s = {a} ∨ s.Nontrivial
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: α : Type u_2
s : Finset α
a : α
h : Disjoint s {a}
⊢ cons a s ⋯ = cons a s ⋯

Tactic:
]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∉ s ∧ Disjoint s t ↔ a ∉ s ∧ Disjoint s t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ s ⊆ t ↔ s ⊆ t

pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ a ∉ ↑s

Tactic:
]

Goal state after:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ a ∉ ↑s
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ a ::ₘ s.val = a ::ₘ s.val

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ s = {a, b} ↔ s = {a, b}

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ motive (Finset.cons a { val := s, nodup := ⋯ } ⋯)

Tactic:
]

Goal state after:
case cons
α : Type u_3
motive : Finset α → Prop
empty : motive ∅
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : s.Nodup), motive { val := s, nodup := nd }
nd : (a ::ₘ s).Nodup
⊢ motive (Finset.cons a { val := s, nodup := ⋯ } ⋯)
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ {a} = {a}

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn : 1 < n
⊢ (Set.Iio n).Nontrivial

Tactic:
]

Goal state after:
n : ℕ
hn : 1 < n
⊢ (Set.Iio n).Nontrivial
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ¬a ∈ s ∧ ¬a ∈ t ↔ ¬a ∈ s ∧ ¬a ∈ t

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
⊢ insert x s = insert x s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P ({x} ∪ s) a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
⊢ P ({x} ∪ s) a
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a✝ b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi✝ : P a✝ s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
⊢ P ({a} ∪ t) {x}

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a✝ b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi✝ : P a✝ s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
⊢ P ({a} ∪ t) {x}
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ insert a (s₁ ∩ s₂) = insert a (s₁ ∩ s₂)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : x ∉ s₂
⊢ False

Tactic:
exact h H

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
⊢ s₁ ∩ s₂ = s₁ ∩ s₂

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∈ s
⊢ insert a ∅ = insert a ∅

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ {a} = {a}

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ ∅ = ∅

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ insert a (s ∪ t) = insert a (s ∪ t)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ ¬Disjoint s t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ Disjoint s t ∨ ¬Disjoint s t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⊆ s.erase a

Tactic:
]

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 ⊆ t ↔ s ⊆ t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).Nodup ↔ Set.InjOn f ↑s

Tactic:
by
  simp [Multiset.nodup_map_iff_inj_on s.nodup, Set.InjOn]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ insert a ((fun s ↦ s.erase a) t) = insert a (t.erase a)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ Injective f ↔ Injective f

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
⊢ Disjoint s t ↔ Disjoint s t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ Disjoint s t ↔ Disjoint s t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ a ∉ s.erase a ∧ Disjoint (s.erase a) t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ a ∉ s.erase a ∧ Disjoint (s.erase a) t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ a ∉ t.erase a ∧ Disjoint s (t.erase a)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
hst : Disjoint s (t.erase a)
⊢ a ∉ t.erase a ∧ Disjoint s (t.erase a)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s = ∅ ∨ s = {a} ↔ s = ∅ ∨ s = {a}

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ x ∈ s

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ x ∈ s
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Set.univ.Nonempty ↔ Set.univ.Nonempty

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ Nontrivial α ↔ Nontrivial α

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ s ↔ a ∈ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∉ s ↔ a ∉ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ univ = univ

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ univ.erase a = univ.erase a

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a ↦ insert a s) (↑s)ᶜ

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a ↦ insert a s) (↑s)ᶜ
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ s = s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = map (Embedding.subtype p) univ

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
f : α → β
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map (f ∘ fun a ↦ ↑a) univ.val = Multiset.map (f ∘ Subtype.val) univ.val

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Multiset α
H : ∀ (x : α), x ∈ s
⊢ ∀ (x : α), x ∈ s.toFinset

Tactic:
simpa using H

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l : List α
H : ∀ (x : α), x ∈ l
⊢ ∀ (x : α), x ∈ l.toFinset

Tactic:
simpa using H

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s

Tactic:
]

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ s = ∅ ↔ s = ∅

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Multiset.map (⇑(Embedding.subtype fun x ↦ x ∈ s)) s.val.attach = s.val

Tactic:
]

Goal state after:
α : Type u_1
s : Finset α
⊢ Multiset.map (⇑(Embedding.subtype fun x ↦ x ∈ s)) s.val.attach = s.val
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ p ↔ x ∈ p

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ t = t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ s ⊂ ↑t ↔ s ⊂ ↑t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ ↑s ⊆ t ↔ ↑s ⊆ t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ ↑s ⊂ t ↔ ↑s ⊂ t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ s ⊆ ↑t ↔ s ⊆ ↑t

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
A : Fintype ↑∅ := Fintype.ofIsEmpty
⊢ s = ∅ ↔ s = ∅

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
x : α
hx : x ∈ s
⊢ g x = a✝ ↔ g x = a✝

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i, f (i % ↑n) = a
i : ℤ
hi : f (i % ↑n) = a
this : 0 ≤ i % ↑n
⊢ i % ↑n < ↑n ∧ f (i % ↑n) = a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i, f (i % ↑n) = a
i : ℤ
hi : f (i % ↑n) = a
this : 0 ≤ i % ↑n
⊢ i % ↑n < ↑n ∧ f (i % ↑n) = a
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % ↑n) = f i
hn' : 0 < ↑n
x✝ : ∃ i < n, f ↑i = a
i : ℕ
hi : i < n
ha : f ↑i = a
⊢ a = a

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c * c) ≤ a * b

Tactic:
]

Goal state after:
case inr
a : Int
ha : 0 ≤ a
b c : Int
hc : 0 ≤ c
hlt : 0 < c
⊢ a * (b / c * c) ≤ a * b
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ m / (n * k) = m / (n * k)

Tactic:
]

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

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ image (f ∘ f^[n]) s = image (f ∘ f^[n]) s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x ↦ x ∈ t) s
⊢ a ∈ t

Tactic:
]

Goal state after:
α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x ↦ x ∈ t) s
⊢ a ∈ t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ insert (k + 1) (range (k + 1) \ {0}) = insert k.succ (range (k + 1) \ {0})

pp: case succ.h
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ k + 1 ∉ {0}

Tactic:
]

Goal state after:
case succ.h
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ k + 1 ∉ {0}
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i = j.rev ↔ i = j.rev

Tactic:
]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ j.rev < i ↔ j.rev < i

Tactic:
]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ j.rev ≤ i ↔ j.rev ≤ i

Tactic:
]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ j < i.rev ↔ j < i.rev

Tactic:
]

Goal state after: