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

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.pmap (fun a_1 h ↦ ⟨↑⟨a_1, h⟩, ⋯⟩) l ⋯

Tactic:
;

Goal state after:
α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.pmap (fun a_1 h ↦ ⟨↑⟨a_1, h⟩, ⋯⟩) l ⋯
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b ↦ flip r (f a) b) s t ↔ Rel (fun a b ↦ r a (f b)) s t

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip fun a b ↦ flip r (f a) b) s t ↔ Rel (fun a b ↦ r a (f b)) s t
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map (g ∘ fun x ↦ i ↑x ⋯) s.attach

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map (g ∘ fun x ↦ i ↑x ⋯) s.attach
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (s ++ t).dedup ~ s.dedup

Tactic:
← coe_eq_coe,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ ↑(s ++ t).dedup = ↑s.dedup
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
⊢ m.toList ~ [a] ↔ m = {a}

Tactic:
← coe_eq_coe,

Goal state after:
α : Type u_1
a : α
m : Multiset α
⊢ ↑m.toList = ↑[a] ↔ m = {a}
Module: Mathlib.Data.Multiset.Basic

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

Tactic:
;

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ xs ~ ys

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ xs ~ ys
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ s.erase a ∩ t.erase a

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ a ::ₘ s.erase a ∩ t.erase a
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ List.map f (List.filter ((fun b ↦ decide (p b)) ∘ f) l) ~ List.map f (List.filter (fun b ↦ decide (p (f b))) l)

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ List.map f (List.filter ((fun b ↦ decide (p b)) ∘ f) l) ~ List.map f (List.filter (fun b ↦ decide (p (f b))) l)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
⊢ ∀ (s : Multiset α), s - t + t ∩ s = s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
ih : map f (filter p s) = filterMap (fun a ↦ if p a then some (f a) else none) s
⊢ map (fun x ↦ f x) (if p a then {a} else 0) + filterMap (fun a ↦ if p a then some (f a) else none) s =
    (if p a then some {f a} else none).getD 0 + filterMap (fun a ↦ if p a then some (f a) else none) s

Tactic:
;

Goal state after:
case cons
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
ih : map f (filter p s) = filterMap (fun a ↦ if p a then some (f a) else none) s
⊢ map (fun x ↦ f x) (if p a then {a} else 0) + filterMap (fun a ↦ if p a then some (f a) else none) s =
    (if p a then some {f a} else none).getD 0 + filterMap (fun a ↦ if p a then some (f a) else none) s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case cons
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ map (fun x ↦ f x) (if p a then {a} else 0) + filterMap (fun a ↦ if p a then some (f a) else none) s =
    (if p a then some {f a} else none).getD 0 + filterMap (fun a ↦ if p a then some (f a) else none) s

Tactic:
;

Goal state after:
case cons
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ map (fun x ↦ f x) (if p a then {a} else 0) + filterMap (fun a ↦ if p a then some (f a) else none) s =
    (if p a then some {f a} else none).getD 0 + filterMap (fun a ↦ if p a then some (f a) else none) s
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(s.bagInter t)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : List α
a✝ : α
⊢ count a✝ (↑s ∩ ↑t) = count a✝ ↑(s.bagInter t)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
;

Goal state after:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
Module: Mathlib.Data.Multiset.UnionInter

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t : Multiset α
⊢ ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
a : α
⊢ count a (s - filter p s) = count a (filter (fun a ↦ ¬p a) s)
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂

Tactic:
;

Goal state after:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₁ = take l₁.length l₂

Tactic:
;

Goal state after:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₁ = take l₁.length l₂
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length

Tactic:
;

Goal state after:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l : List α
m n : ℕ
⊢ min m l.length ≤ n ↔ m ≤ n ∨ l.length ≤ n

Tactic:
;

Goal state after:
α : Type u_1
l : List α
m n : ℕ
⊢ min m l.length ≤ n ↔ m ≤ n ∨ l.length ≤ n
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take x.length y ++ [y[x.length]]

pp: α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x.length < y.length

Tactic:
;

Goal state after:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take x.length y ++ [y[x.length]]

α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x.length < y.length
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case mpr
α : Type u_1
x : α
⊢ [x] <:+: [x]

Tactic:
;

Goal state after:
case mpr
α : Type u_1
x : α
⊢ [x] <:+: [x]
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.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: α : 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.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.Finset.Erase

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: case mk
α : Type u_5
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } t
⊢ a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } ∨ a ∈ t

Tactic:
;

Goal state after:
case mk
α : Type u_5
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } t
⊢ a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } ∨ a ∈ t
Module: Mathlib.Data.Finset.Disjoint

Goal state before:
pp: case mk.mk
α : Type u_5
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) t)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }
    { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }
⊢ a ∈
      { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }.disjUnion
        { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ } ∨
      a ∈ { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_5
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) t)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }
    { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }
⊢ a ∈
      { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }.disjUnion
        { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ } ∨
      a ∈ { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
a : α
hs : {a}.Nontrivial
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
a : α
hs : {a}.Nontrivial
⊢ False
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.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 α
s t : Finset α
a : α
ha : a ∉ s
⊢ ↑(insert a s) ⊆ ↑(insert a t) ↔ ↑s ⊆ ↑t

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ ↑(insert a s) ⊆ ↑(insert a t) ↔ ↑s ⊆ ↑t
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
h : DecidablePred fun x ↦ True
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x ↦ True) s ↔ a✝ ∈ s

Tactic:
;

Goal state after:
α : Type u_1
h : DecidablePred fun x ↦ True
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x ↦ True) s ↔ a✝ ∈ s
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
h : DecidablePred fun x ↦ False
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x ↦ False) s ↔ a✝ ∈ ∅

Tactic:
;

Goal state after:
α : Type u_1
h : DecidablePred fun x ↦ False
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x ↦ False) s ↔ a✝ ∈ ∅
Module: Mathlib.Data.Finset.SDiff

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
a✝ : α
⊢ a✝ ∈ insert a s \ insert b s ↔ a✝ ∈ {a}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
a✝ : α
⊢ a✝ ∈ insert a s \ insert b s ↔ a✝ ∈ {a}
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
singleton_union

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
⊢ insert x s = insert x s
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₂
⊢ x ∈ s₂
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:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : x ∉ s₂
⊢ False
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), ¬(x = a ∧ x ∈ s)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
H : a ∉ s
⊢ ∀ (x : α), ¬(x = a ∧ x ∈ s)
Module: Mathlib.Data.Finset.Lattice.Lemmas

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
h : x ∈ s
H : x ∉ s
⊢ False
Module: Mathlib.Data.Fintype.Defs

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Fintype α
x✝ : α
⊢ x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
x✝¹ x✝ : Fintype α
s₁ : Finset α
h₁ : ∀ (x : α), x ∈ s₁
s₂ : Finset α
h₂ : ∀ (x : α), x ∈ s₂
⊢ s₁ = s₂

Tactic:
;

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
x✝¹ x✝ : Fintype α
s₁ : Finset α
h₁ : ∀ (x : α), x ∈ s₁
s₂ : Finset α
h₂ : ∀ (x : α), x ∈ s₂
⊢ s₁ = s₂
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
a✝ : α
⊢ a✝ ∈ s.erase a \ s.erase b ↔ a✝ ∈ {b}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
a✝ : α
⊢ a✝ ∈ s.erase a \ s.erase b ↔ a✝ ∈ {b}
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: m n a✝ : ℕ
⊢ a✝ ∈ range m ∩ range n ↔ a✝ ∈ range (min m n)

Tactic:
;

Goal state after:
m n a✝ : ℕ
⊢ a✝ ∈ range m ∩ range n ↔ a✝ ∈ range (min m n)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: m n a✝ : ℕ
⊢ a✝ ∈ range m ∪ range n ↔ a✝ ∈ range (max m n)

Tactic:
;

Goal state after:
m n a✝ : ℕ
⊢ a✝ ∈ range m ∪ range n ↔ a✝ ∈ range (max m n)
Module: Mathlib.Data.Finset.BooleanAlgebra

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ univ.Nonempty ↔ Nonempty α
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ a✝ ∈ (s ∪ t).toFinset ↔ a✝ ∈ s.toFinset ∪ t.toFinset
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter p s.toFinset

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter p s.toFinset
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter (fun x ↦ p x = true) s.toFinset

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter (fun x ↦ p x = true) s.toFinset
Module: Mathlib.Data.Finset.BooleanAlgebra

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ univ ∩ s ↔ a ∈ s
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a b : α
⊢ b ∈ {a} ↔ b ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a b : α
⊢ b ∈ {a} ↔ b ∈ univ
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ Multiset.map (⇑g ∘ ⇑f) s.val = Multiset.map (⇑(f.trans g)) s.val

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ Multiset.map (⇑g ∘ ⇑f) s.val = Multiset.map (⇑(f.trans g)) s.val
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 (g.trans f) s = map (f'.trans g') s

Tactic:
Embedding.trans,

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 := ⇑f ∘ ⇑g, inj' := ⋯ } s = map { toFun := ⇑g' ∘ ⇑f', inj' := ⋯ } s
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_4
a : α
H : {a} = ∅
⊢ False

Tactic:
;

Goal state after:
α : Type u_4
a : α
H : {a} = ∅
⊢ False
Module: Mathlib.Data.Fintype.Sets

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

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
inst✝¹ inst✝ : Fintype ↑s
⊢ s.toFinset = s.toFinset
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: ⊢ univ.val = True ::ₘ {False}

Tactic:
;

Goal state after:
⊢ univ.val = True ::ₘ {False}
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
hs : s.Nontrivial
hf : Set.InjOn f ↑s
⊢ (image f s).Nontrivial

Tactic:
by
  obtain ⟨x, hx, y, hy, hxy⟩ := hs
  exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f : α → β
inst✝ : DecidableEq γ
g : β → γ
s : Finset α
a✝ : γ
⊢ a✝ ∈ (image g ∘ image f) s ↔ a✝ ∈ image (g ∘ f) s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f : α → β
inst✝ : DecidableEq γ
g : β → γ
s : Finset α
a✝ : γ
⊢ a✝ ∈ (image g ∘ image f) s ↔ a✝ ∈ image (g ∘ f) s
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
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) ⋯

Tactic:
;

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) ⋯