mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)

Tactic:
induction l₁ with
  | nil => simp
  | cons a l₁ ih =>
    rw [foldr_cons, ih]
    simp [List.flatMap, flatten_flatten, Function.comp_def]

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

Goal state before:
pp: case nil
α : Type u
⊢ map pure [] <+ [].sublists

pp: case append_singleton
α : Type u
l✝ : List α
a✝¹ : α
a✝ : map pure l✝ <+ l✝.sublists
⊢ map pure (l✝ ++ [a✝¹]) <+ (l✝ ++ [a✝¹]).sublists

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ map pure [] <+ [].sublists

case append_singleton
α : Type u
l✝ : List α
a✝¹ : α
a✝ : map pure l✝ <+ l✝.sublists
⊢ map pure (l✝ ++ [a✝¹]) <+ (l✝ ++ [a✝¹]).sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
β : Type v
f : List α → β
r : List β
⊢ sublistsLenAux 0 [] f r = f [] :: r

pp: case cons
α : Type u
β : Type v
f : List α → β
r : List β
head✝ : α
tail✝ : List α
⊢ sublistsLenAux 0 (head✝ :: tail✝) f r = f [] :: r

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
f : List α → β
r : List β
⊢ sublistsLenAux 0 [] f r = f [] :: r

case cons
α : Type u
β : Type v
f : List α → β
r : List β
head✝ : α
tail✝ : List α
⊢ sublistsLenAux 0 (head✝ :: tail✝) f r = f [] :: r
Module: Mathlib.Data.List.Sublists

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

Tactic:
rw [sublistsLen_succ_cons, sublists'_cons]
    exact (sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)

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

Goal state before:
pp: case inr
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ (a :: l').length = n + 1

Tactic:
exact congr_arg (· + 1) (length_of_sublistsLen h)

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

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

pp: case cons
α : Type u
β : Type v
f : α → β
a : α
l head✝ : List α
tail✝ : List (List α)
tail_ih✝ :
  flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) tail✝) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) tail✝)
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) (head✝ :: tail✝)) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) (head✝ :: tail✝))

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) []) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) [])

case cons
α : Type u
β : Type v
f : α → β
a : α
l head✝ : List α
tail✝ : List (List α)
tail_ih✝ :
  flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) tail✝) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) tail✝)
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) (head✝ :: tail✝)) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) (head✝ :: tail✝))
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case empty.zero
α : Type u_1
β : Type u_2
f : α → β
⊢ powersetCard 0 (map f 0) = map (map f) (powersetCard 0 0)

pp: case empty.succ
α : Type u_1
β : Type u_2
f : α → β
n✝ : ℕ
⊢ powersetCard (n✝ + 1) (map f 0) = map (map f) (powersetCard (n✝ + 1) 0)

Tactic:
<;>

Goal state after:
case empty.zero
α : Type u_1
β : Type u_2
f : α → β
⊢ powersetCard 0 (map f 0) = map (map f) (powersetCard 0 0)

case empty.succ
α : Type u_1
β : Type u_2
f : α → β
n✝ : ℕ
⊢ powersetCard (n✝ + 1) (map f 0) = map (map f) (powersetCard (n✝ + 1) 0)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case cons.zero
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
⊢ powersetCard 0 (map f (t ::ₘ s)) = map (map f) (powersetCard 0 (t ::ₘ s))

pp: case cons.succ
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n✝ : ℕ
⊢ powersetCard (n✝ + 1) (map f (t ::ₘ s)) = map (map f) (powersetCard (n✝ + 1) (t ::ₘ s))

Tactic:
<;>

Goal state after:
case cons.zero
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
⊢ powersetCard 0 (map f (t ::ₘ s)) = map (map f) (powersetCard 0 (t ::ₘ s))

case cons.succ
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n✝ : ℕ
⊢ powersetCard (n✝ + 1) (map f (t ::ₘ s)) = map (map f) (powersetCard (n✝ + 1) (t ::ₘ s))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ∀ (x y : { x // P x }), ↑(x ⊔ y) = ↑x ⊔ ↑y

pp: case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥

Tactic:
<;>

Goal state after:
case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ∀ (x y : { x // P x }), ↑(x ⊔ y) = ↑x ⊔ ↑y

case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
x✝ y✝ : { x // P x }
⊢ ↑(x✝ ⊔ y✝) = ↑x✝ ⊔ ↑y✝

pp: case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥

Tactic:
<;>

Goal state after:
case g_sup
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
x✝ y✝ : { x // P x }
⊢ ↑(x✝ ⊔ y✝) = ↑x✝ ⊔ ↑y✝

case bot
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := ⋯
this : OrderBot { x // P x } := ⋯
⊢ ↑⊥ = ⊥
Module: Mathlib.Data.Set.Finite.Powerset

Goal state before:
pp: α : Type u
a : Set α
h : a.Finite
⊢ {b | b ⊆ a}.Finite

Tactic:
convert! ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet
  ext s
  simpa [← @exists_finite_iff_finset α fun t => t ⊆ a ∧ t = s, Finite.subset_toFinset,
    ← and_assoc, Finset.coeEmb] using h.subset

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ i = insert a j → i = j

pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ insert a i = j → i = j

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ i = insert a j → i = j

case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ insert a i = j → i = j
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
j : Finset α
hj : j ⊆ s
hi : insert a j ⊆ s
⊢ insert a j = j

pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
hj : insert a i ⊆ s
⊢ i = insert a i

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
j : Finset α
hj : j ⊆ s
hi : insert a j ⊆ s
⊢ insert a j = j

case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
hj : insert a i ⊆ s
⊢ i = insert a i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
⊢ ∅.sup f = ⊥ ↔ ∀ s ∈ ∅, f s = ⊥

pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
a✝² : β
s✝ : Finset β
a✝¹ : a✝² ∉ s✝
a✝ : s✝.sup f = ⊥ ↔ ∀ s ∈ s✝, f s = ⊥
⊢ (insert a✝² s✝).sup f = ⊥ ↔ ∀ s ∈ insert a✝² s✝, f s = ⊥

Tactic:
<;>

Goal state after:
case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
⊢ ∅.sup f = ⊥ ↔ ∀ s ∈ ∅, f s = ⊥

case insert
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
a✝² : β
s✝ : Finset β
a✝¹ : a✝² ∉ s✝
a✝ : s✝.sup f = ⊥ ↔ ∀ s ∈ s✝, f s = ⊥
⊢ (insert a✝² s✝).sup f = ⊥ ↔ ∀ s ∈ insert a✝² s✝, f s = ⊥
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ (Disjoint on fun i ↦ ⨆ i' ∈ t, f (i, i')) i j

pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ (Disjoint on fun i' ↦ ⨆ i ∈ s, f (i, i')) i j

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ (Disjoint on fun i ↦ ⨆ i' ∈ t, f (i, i')) i j

case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ (Disjoint on fun i' ↦ ⨆ i ∈ s, f (i, i')) i j
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ i_1 ∈ t, ∀ i_3 ∈ t, Disjoint (f (i, i_1)) (f (j, i_3))

pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ i_1 ∈ s, ∀ i_3 ∈ s, Disjoint (f (i_1, i)) (f (i_3, j))

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ i_1 ∈ t, ∀ i_3 ∈ t, Disjoint (f (i, i_1)) (f (j, i_3))

case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ i_1 ∈ s, ∀ i_3 ∈ s, Disjoint (f (i_1, i)) (f (i_3, j))
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: case none
α : Type u_1
a : α
⊢ a ∈ none.toFinset ↔ a ∈ none

pp: case some
α : Type u_1
a val✝ : α
⊢ a ∈ (some val✝).toFinset ↔ a ∈ some val✝

Tactic:
<;>

Goal state after:
case none
α : Type u_1
a : α
⊢ a ∈ none.toFinset ↔ a ∈ none

case some
α : Type u_1
a val✝ : α
⊢ a ∈ (some val✝).toFinset ↔ a ∈ some val✝
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: case none
α : Type u_1
⊢ none.toFinset.card = none.elim 0 1

pp: case some
α : Type u_1
val✝ : α
⊢ (some val✝).toFinset.card = (some val✝).elim 0 1

Tactic:
<;>

Goal state after:
case none
α : Type u_1
⊢ none.toFinset.card = none.elim 0 1

case some
α : Type u_1
val✝ : α
⊢ (some val✝).toFinset.card = (some val✝).elim 0 1
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: case none
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ image some (eraseNone s) ↔ none ∈ s.erase none

pp: case some
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ image some (eraseNone s) ↔ some x ∈ s.erase none

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ image some (eraseNone s) ↔ none ∈ s.erase none

case some
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ image some (eraseNone s) ↔ some x ∈ s.erase none
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: case none
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ insertNone (eraseNone s) ↔ none ∈ insert none s

pp: case some
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ insertNone (eraseNone s) ↔ some x ∈ insert none s

Tactic:
<;>

Goal state after:
case none
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ insertNone (eraseNone s) ↔ none ∈ insert none s

case some
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ insertNone (eraseNone s) ↔ some x ∈ insert none s
Module: Mathlib.Data.Finset.Option

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

Tactic:
map_some_eraseNone

Goal state after:
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ #(s.erase none) = #(s.erase none)
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.powerset = (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯

Tactic:
by
  refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
  · rw [mem_disjiUnion]
    exact
      ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp ha))),
        mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
  · rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
    exact mem_powerset.mpr (mem_powersetCard.mp ha).1

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

Goal state before:
pp: P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
f_empty : ∀ (i : Fintype PEmpty.{u + 1}), P PEmpty.{u + 1} := fun i ↦ ?m.44
⊢ ∀ {α : Type u} [Fintype α] [DecidableEq α], (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)

Tactic:
rintro α hα - Pα hα'
      convert! h_option α (Pα _)

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ∀ (a : β), g ({a}.sup' ⋯ f) = {a}.sup' ⋯ (g ∘ f)

pp: case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ∀ (a : β) (s : Finset β) (h : a ∉ s) (hs : s.Nonempty),
    g (s.sup' hs f) = s.sup' hs (g ∘ f) → g ((cons a s h).sup' ⋯ f) = (cons a s h).sup' ⋯ (g ∘ f)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ∀ (a : β), g ({a}.sup' ⋯ f) = {a}.sup' ⋯ (g ∘ f)

case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ ∀ (a : β) (s : Finset β) (h : a ∉ s) (hs : s.Nonempty),
    g (s.sup' hs f) = s.sup' hs (g ∘ f) → g ((cons a s h).sup' ⋯ f) = (cons a s h).sup' ⋯ (g ∘ f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝ : β
⊢ g ({a✝}.sup' ⋯ f) = {a✝}.sup' ⋯ (g ∘ f)

pp: case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝¹ : β
s✝ : Finset β
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : g (s✝.sup' hs✝ f) = s✝.sup' hs✝ (g ∘ f)
⊢ g ((cons a✝¹ s✝ h✝).sup' ⋯ f) = (cons a✝¹ s✝ h✝).sup' ⋯ (g ∘ f)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝ : β
⊢ g ({a✝}.sup' ⋯ f) = {a✝}.sup' ⋯ (g ∘ f)

case refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝¹ : β
s✝ : Finset β
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : g (s✝.sup' hs✝ f) = s✝.sup' hs✝ (g ∘ f)
⊢ g ((cons a✝¹ s✝ h✝).sup' ⋯ f) = (cons a✝¹ s✝ h✝).sup' ⋯ (g ∘ f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ ∀ (a : ι), f ({a}.sup' ⋯ g) = {a}.sup' ⋯ (⇑f ∘ g)

pp: case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s) (hs : s.Nonempty),
    f (s.sup' hs g) = s.sup' hs (⇑f ∘ g) → f ((cons a s h).sup' ⋯ g) = (cons a s h).sup' ⋯ (⇑f ∘ g)

Tactic:
<;>

Goal state after:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ ∀ (a : ι), f ({a}.sup' ⋯ g) = {a}.sup' ⋯ (⇑f ∘ g)

case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s) (hs : s.Nonempty),
    f (s.sup' hs g) = s.sup' hs (⇑f ∘ g) → f ((cons a s h).sup' ⋯ g) = (cons a s h).sup' ⋯ (⇑f ∘ g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝ : ι
⊢ f ({a✝}.sup' ⋯ g) = {a✝}.sup' ⋯ (⇑f ∘ g)

pp: case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : f (s✝.sup' hs✝ g) = s✝.sup' hs✝ (⇑f ∘ g)
⊢ f ((cons a✝¹ s✝ h✝).sup' ⋯ g) = (cons a✝¹ s✝ h✝).sup' ⋯ (⇑f ∘ g)

Tactic:
<;>

Goal state after:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝ : ι
⊢ f ({a✝}.sup' ⋯ g) = {a✝}.sup' ⋯ (⇑f ∘ g)

case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : f (s✝.sup' hs✝ g) = s✝.sup' hs✝ (⇑f ∘ g)
⊢ f ((cons a✝¹ s✝ h✝).sup' ⋯ g) = (cons a✝¹ s✝ h✝).sup' ⋯ (⇑f ∘ g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
⊢ x ∈ ∅.sup f ↔ ∃ v ∈ ∅, x ∈ f v

pp: case cons
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : x ∈ s✝.sup f ↔ ∃ v ∈ s✝, x ∈ f v
⊢ x ∈ (Finset.cons a✝¹ s✝ h✝).sup f ↔ ∃ v ∈ Finset.cons a✝¹ s✝ h✝, x ∈ f v

Tactic:
<;>

Goal state after:
case empty
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
⊢ x ∈ ∅.sup f ↔ ∃ v ∈ ∅, x ∈ f v

case cons
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a✝¹ : α
s✝ : Finset α
h✝ : a✝¹ ∉ s✝
a✝ : x ∈ s✝.sup f ↔ ∃ v ∈ s✝, x ∈ f v
⊢ x ∈ (Finset.cons a✝¹ s✝ h✝).sup f ↔ ∃ v ∈ Finset.cons a✝¹ s✝ h✝, x ∈ f v
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝ : ι
⊢ a ∈ {a✝}.sup' ⋯ f ↔ ∃ i ∈ {a✝}, a ∈ f i

pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : a ∈ s✝.sup' hs✝ f ↔ ∃ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).sup' ⋯ f ↔ ∃ i ∈ cons a✝¹ s✝ h✝, a ∈ f i

Tactic:
<;>

Goal state after:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝ : ι
⊢ a ∈ {a✝}.sup' ⋯ f ↔ ∃ i ∈ {a✝}, a ∈ f i

case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : a ∈ s✝.sup' hs✝ f ↔ ∃ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).sup' ⋯ f ↔ ∃ i ∈ cons a✝¹ s✝ h✝, a ∈ f i
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case singleton
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝ : ι
⊢ a ∈ {a✝}.inf' ⋯ f ↔ ∀ i ∈ {a✝}, a ∈ f i

pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : a ∈ s✝.inf' hs✝ f ↔ ∀ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).inf' ⋯ f ↔ ∀ i ∈ cons a✝¹ s✝ h✝, a ∈ f i

Tactic:
<;>

Goal state after:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝ : ι
⊢ a ∈ {a✝}.inf' ⋯ f ↔ ∀ i ∈ {a✝}, a ∈ f i

case cons
α : Type u_2
ι : Type u_5
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
a : α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : a ∈ s✝.inf' hs✝ f ↔ ∀ i ∈ s✝, a ∈ f i
⊢ a ∈ (cons a✝¹ s✝ h✝).inf' ⋯ f ↔ ∀ i ∈ cons a✝¹ s✝ h✝, a ∈ f i