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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x ↦ (x, ↑l - x)) (powersetAux l) ~ List.map (fun x ↦ (x, ↑l - x)) (powersetAux' l)

Tactic:
]

Goal state after:
α : Type u_1
l : List α
this : DecidableEq α
⊢ List.map (fun x ↦ (x, ↑l - x)) (powersetAux l) ~ List.map (fun x ↦ (x, ↑l - x)) (powersetAux' l)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
]

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ [] = []

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ List.map ofList l₁✝.sublists' <+~ List.map ofList l₂✝.sublists'

Tactic:
]

Goal state after:
α : Type u_1
s t : Multiset α
le : s ≤ t
l₁✝ l₂✝ : List α
hsub : l₁✝ <+ l₂✝
⊢ List.map ofList l₁✝.sublists' <+~ List.map ofList l₂✝.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) (sublistsLen 0 s) = map (fun x ↦ [x]) (a :: s).reverse

Tactic:
reverse_cons,

Goal state after:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) (sublistsLen 0 s) = map (fun x ↦ [x]) (s.reverse ++ [a])
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) [[]] = map (fun x ↦ [x]) s.reverse ++ map (fun x ↦ [x]) [a]

Tactic:
]

Goal state after:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) [[]] = map (fun x ↦ [x]) s.reverse ++ map (fun x ↦ [x]) [a]
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
⊢ List.map ofList (sublistsLen n l) = List.map ofList (sublistsLen n l)

Tactic:
]

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ l.length.choose n + l.length.choose (n + 1) = l.length.choose n + l.length.choose n.succ

Tactic:
]

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'

Tactic:
]

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) l₂✝ <+ sublistsLen (n + 1) l₂✝ ++ map (cons a) (sublistsLen n l₂✝)

Tactic:
]

Goal state after:
case succ.cons
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
IH : sublistsLen (n + 1) l₁✝ <+ sublistsLen (n + 1) l₂✝
⊢ sublistsLen (n + 1) l₂✝ <+ sublistsLen (n + 1) l₂✝ ++ map (cons a) (sublistsLen n l₂✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1, a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'
⊢ l'.length = n + 1

Tactic:
]

Goal state after:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1, a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'
⊢ l'.length = n + 1
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Tactic:
]

Goal state after:
case cons.cons
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons_cons
α : Type u
l l' l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝ ∈ sublistsLen l₁✝.length l₂✝
⊢ a :: l₁✝ ∈ sublistsLen (l₁✝.length + 1) l₂✝ ++ map (cons a) (sublistsLen l₁✝.length l₂✝)

Tactic:
]

Goal state after:
case cons_cons
α : Type u
l l' l₁✝ l₂✝ : List α
a : α
s : l₁✝ <+ l₂✝
IH : l₁✝ ∈ sublistsLen l₁✝.length l₂✝
⊢ a :: l₁✝ ∈ sublistsLen (l₁✝.length + 1) l₂✝ ++ map (cons a) (sublistsLen l₁✝.length l₂✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
this : Pairwise (fun a b ↦ Lex (Function.swap fun b a ↦ R a b) a.reverse b.reverse) l.sublists
⊢ Pairwise (Lex R on reverse) l.sublists

Tactic:
]

Goal state after:
α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
this : Pairwise (fun a b ↦ Lex (Function.swap fun b a ↦ R a b) a.reverse b.reverse) l.sublists
⊢ Pairwise (Lex R on reverse) l.sublists
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝)

Tactic:
]

Goal state after:
case succ.swap.succ
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
n✝ : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux (n✝ + 1) l₁ ~ powersetCardAux (n✝ + 1) l₂
⊢ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝) ~
    List.map (cons b) (powersetCardAux (n✝ + 1) l✝) ++ List.map (cons a) (powersetCardAux (n✝ + 1) l✝) ++
      List.map (cons a ∘ cons b) (powersetCardAux n✝ l✝)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.Nodup ↔ l.Nodup

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) l.sublists) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) l.sublists)

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) l.sublists) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) l.sublists)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ map (map l.get) (finRange l.length).sublists ~ map (map l.get) (finRange l.length).sublists'

Tactic:
]

Goal state after:
α : Type u
l : List α
⊢ map (map l.get) (finRange l.length).sublists ~ map (map l.get) (finRange l.length).sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'

Tactic:
]

Goal state after:
case cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' ++ map (List.cons a) l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'

Tactic:
]

Goal state after:
case cons_cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' ++ map (List.cons a) l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l₁ l₂ : List α
sublist : l₁ <+ l₂
⊢ l₁.sublists' <+ l₂.sublists'

Tactic:
by
  induction sublist with
  | slnil => exact .refl _
  | cons a _ ih =>
    rw [sublists'_cons]
    exact ih.trans (List.sublist_append_left ..)
  | cons_cons a _ ih =>
    rw [sublists'_cons, sublists'_cons]
    exact ih.append (ih.map _)

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
]

Goal state after:
α : Type u
a : α
l : List α
⊢ l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse
⊢ l₁ ++ l₂ ~ l

Tactic:
]

Goal state after:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse
⊢ l₁ ++ l₂ ~ l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x ↦ x ++ [a]) (l'.sublists.zip l'.sublists.reverse) ++
      map (Prod.map (fun x ↦ x ++ [a]) id) (l'.sublists.zip l'.sublists.reverse)
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
]

Goal state after:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x ↦ x ++ [a]) (l'.sublists.zip l'.sublists.reverse) ++
      map (Prod.map (fun x ↦ x ++ [a]) id) (l'.sublists.zip l'.sublists.reverse)
⊢ l₁ ++ l₂ ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inl
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]

Tactic:
]

Goal state after:
case append_singleton.inl
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]

Tactic:
]

Goal state after:
case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]

Tactic:
]

Goal state after:
case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ l₂ ~ l

Tactic:
]

Goal state after:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ l₂ ~ l
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ (s✝.sup f ⊔ s✝.sup g) = f a✝ ⊔ s✝.sup f ⊔ (g a✝ ⊔ s✝.sup g)

Tactic:
]

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f g : β → α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
ih : s✝.sup (f ⊔ g) = s✝.sup f ⊔ s✝.sup g
⊢ (f ⊔ g) a✝ ⊔ (s✝.sup f ⊔ s✝.sup g) = f a✝ ⊔ s✝.sup f ⊔ (g a✝ ⊔ s✝.sup g)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id (cons a)) (l.sublists'.zip l.sublists'.reverse) ++
      map (Prod.map (cons a) id) (l.sublists'.zip l.sublists'.reverse)
⊢ l₁ ++ l₂ ~ a :: l

pp: case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l.sublists'.length = (map (cons a) l.sublists').reverse.length

Tactic:
]

Goal state after:
case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id (cons a)) (l.sublists'.zip l.sublists'.reverse) ++
      map (Prod.map (cons a) id) (l.sublists'.zip l.sublists'.reverse)
⊢ l₁ ++ l₂ ~ a :: l

case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l.sublists'.length = (map (cons a) l.sublists').reverse.length
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f (g i) ⊔ s.sup (⇑f ∘ g) = f (g i) ⊔ s.sup (⇑f ∘ g)

Tactic:
]

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

Goal state before:
pp: case empty
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: case cons
α : Type u_7
β : Type u_8
inst✝ : GeneralizedBooleanAlgebra α
f : β → α
a : α
a✝ : β
s✝ : Finset β
h✝ : a✝ ∉ s✝
h : (s✝.sup fun b ↦ f b \ a) = s✝.sup f \ a
⊢ f a✝ \ a ⊔ s✝.sup f \ a = f a✝ \ a ⊔ s✝.sup f \ a

Tactic:
]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c) ⊔ t.sup (g ∘ f) = g (f c) ⊔ t.sup (g ∘ f)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∀ (x : Set α) (h : x ∈ s), (↑⟨x, h⟩).Pairwise r) ↔ ∀ a ∈ s, a.Pairwise r

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (↑l).dedup.sup

Tactic:
]

Goal state after:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
l : List α
⊢ Multiset.fold (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (↑l).dedup = (↑l).dedup.sup
Module: Mathlib.Data.List.Sublists

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s = ∅ ↔ s = ∅

Tactic:
]

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

Goal state before:
pp: α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
⊢ r ⊆ insert a r

Tactic:
]

Goal state after:
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
⊢ r ⊆ insert a r
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case right
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ r.sup id ≤ z

Tactic:
]

Goal state after:
case right
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ a ≤ z ∧ r.sup id ≤ z
Module: Mathlib.Data.Finset.Powerset

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥

Tactic:
]

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
hxt : x ⊆ t
hxn : #x = n
hsx : s ⊆ x
⊢ n - #s = n - #s

Tactic:
]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset α
f : α → β
⊢ s.sup f = s.sup f

Tactic:
]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ n - #s + #s = n

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ n - #s + #s = n
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
⊢ s ⊆ t ↔ s ⊆ t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h : #s < n
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
this : f a ≤ (fun x ↦ x.sup f) t
⊢ f a ≤ t.sup f

Tactic:
]

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
this : f a ≤ (fun x ↦ x.sup f) t
⊢ f a ≤ t.sup f
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ s ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ s ∪ {x ∈ image (insert x) s.powerset | #x = n.succ} =
    powersetCard n.succ s ∪ image (insert x) (powersetCard n s)
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i, ∃ (_ : i ∈ t), a ∈ f i

Tactic:
]

Goal state after:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i, ∃ (_ : i ∈ t), a ∈ f i
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s ↔ a✝ = s

Tactic:
]

Goal state after:
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s ↔ a✝ = s
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ s.erase none = s.erase none

Tactic:
]

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

Goal state before:
pp: case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
s a : Finset α
ha : a ∈ s.powerset
⊢ ∃ a_1 ∈ range (#s + 1), a ∈ powersetCard a_1 s