mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Max α
inst✝⁶ : Bot α
inst✝⁵ : Max β
inst✝⁴ : Bot β
inst✝³ : Max γ
inst✝² : Bot γ
inst✝¹ : Max δ
inst✝ : Bot δ
g : SupBotHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun ⊥ = ⊥
h : (fun f ↦ f.toFun) { toFun := toFun✝, map_sup' := map_sup'✝, map_bot' := map_bot'✝ } = (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_bot' := map_bot'✝ } = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Max α
inst✝⁶ : Bot α
inst✝⁵ : Max β
inst✝⁴ : Bot β
inst✝³ : Max γ
inst✝² : Bot γ
inst✝¹ : Max δ
inst✝ : Bot δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_bot'✝¹ : { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun ⊥ = ⊥
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_bot' := map_bot'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_sup' := map_sup'✝, map_bot' := map_bot'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_bot' := map_bot'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_bot' := map_bot'✝ }
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Max α
inst✝⁶ : Bot α
inst✝⁵ : Max β
inst✝⁴ : Bot β
inst✝³ : Max γ
inst✝² : Bot γ
inst✝¹ : Max δ
inst✝ : Bot δ
f g : SupBotHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Max α
inst✝⁴ : Bot α
inst✝³ : Max β
inst✝² : Bot β
inst✝¹ : Max γ
inst✝ : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Bot α
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
P : β → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
this✝ : OrderBot { x // P x } := Subtype.orderBot Pbot
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ (SupHom.subtypeVal Psup).toFun ⊥ = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.max = ↑a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.max = max ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
f g : BoundedLatticeHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
⊢ s = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ ∀ {a : α}, s.max = ↑a → a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : OrderTop α
s : Finset α
⊢ (∃ b ∈ s, ↑b = ⊤) ↔ ⊤ ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min = ↑a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.min = min ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
P : β → Prop
Pbot : P ⊥
Ptop : P ⊤
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this✝ : Lattice { x // P x } := Subtype.lattice Psup Pinf
this : BoundedOrder (Subtype P) := Subtype.boundedOrder Pbot Ptop
⊢ (LatticeHom.subtypeVal Psup Pinf).toFun ⊤ = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ s.min = ⊤ ↔ s = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.min = ↑(s.min' H)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min' ⋯ = a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.max = ↑(s.max' H)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
P : β → Prop
Pbot : P ⊥
Ptop : P ⊤
Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)
Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)
this✝ : Lattice { x // P x } := Subtype.lattice Psup Pinf
this : BoundedOrder (Subtype P) := Subtype.boundedOrder Pbot Ptop
⊢ (LatticeHom.subtypeVal Psup Pinf).toFun ⊥ = ⊥

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.max' ⋯ = a

Tactic:
by

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
ι : Type u_5
κ : Type u_6
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
x : α
h₂ : 1 < #s
⊢ 0 < #s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h₂ : 1 < #s
⊢ s.min' ⋯ < s.max' ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).max

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = (image (⇑ofDual) s).min

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
⊢ RightInverse unzip (uncurry zip)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap (l₁.zip []) = [].zip l₁

Tactic:
rw [zip_nil_right]

Goal state after:
α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap [] = [].zip l₁
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
β : Type u_1
l₁ : List α
⊢ map Prod.swap (l₁.zip []) = [].zip l₁

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
a : α
l₁ : List α
b : β
l₂ : List β
⊢ map Prod.swap ((a :: l₁).zip (b :: l₂)) = (b :: l₂).zip (a :: l₁)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
x✝ : [].length = [].length
⊢ Forall p (zipWith f [] []) ↔ Forall₂ (fun x y ↦ p (f x y)) [] []

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : (a :: l₁).length = (b :: l₂).length
⊢ Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun x y ↦ p (f x y)) (a :: l₁) (b :: l₂)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
l : List (α × β)
⊢ (map Prod.swap l).unzip = l.unzip.swap

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
h : Forall₂ (fun a b ↦ f a b = g a b) la lb
⊢ zipWith f la lb = zipWith g la lb

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.length = l.length

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.fst l.revzip = l

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.snd l.revzip = l.reverse

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.reverse = l.reverse.revzip

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.swap l.revzip = l.reverse.revzip

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithTop.map (⇑toDual) s.min = (image (⇑toDual) s).max

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = (image (⇑toDual) s).min

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ofDual (s.min' hs) = (image (⇑ofDual) s).max' ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
hs : s.Nonempty
⊢ ofDual (s.max' hs) = (image (⇑ofDual) s).min' ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ toDual (s.min' hs) = (image (⇑toDual) s).max' ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ toDual (s.max' hs) = (image (⇑toDual) s).min' ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
r₁ r₂ : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α), x.toList ++ [a :: y] = (x.push (a :: y)).toList

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (↑(insert a s)) (max a (s.max' H))

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (↑(insert a s)) (min a (s.min' H))

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.min' ⋯ = min a b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ {a, b}.max' ⋯ = max a b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).max' h = f (s.max' ⋯)

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
⊢ ∀ (r₁ r₂ : List (List α)),
    sublists'Aux a r₁ r₂ = (Array.foldl (fun r l ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).min' h = f (s.min' ⋯)

Tactic:
by

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

Goal state before:
pp: case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ ∅.max ≠ ↑x

Tactic:
max_empty

Goal state after:
case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ ⊥ ≠ ↑x
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).max ≠ ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).min ≠ ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
y : α
hy : y ∈ s ∧ x < y
⊢ y ∈ s ∧ x < y

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : {x_1 ∈ s | x < x_1}.Nonempty
aux : {x_1 ∈ s | x < x_1}.min' Hne ∈ s ∧ x < {x_1 ∈ s | x < x_1}.min' Hne
⊢ x < {x_1 ∈ s | x < x_1}.min' Hne

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists' = foldr (fun a r ↦ sublists'Aux a r r) [[]] l

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
r₁ x✝ : List (List α)
⊢ sublists'Aux a [] x✝ = x✝ ++ map (cons a) []

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : {x_1 ∈ s | x < x_1}.Nonempty
aux : {x_1 ∈ s | x < x_1}.min' Hne ∈ s ∧ x < {x_1 ∈ s | x < x_1}.min' Hne
z : α
hzs : z ∈ s
hz : x < z
⊢ x < z

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : List α
h : s = []
⊢ s <+ []

Tactic:
by

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

Goal state before:
pp: case mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)
      · simp
      · simp [ih.mp h]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ x < a

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
b : α
hb : b ∈ {y_1 ∈ t | y < y_1}
⊢ y < b

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
⊢ StrictMonoOn f ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ #s ≤ #t + 1

Tactic:
by

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

Goal state before:
pp: α : Type u
l init tail : List α
⊢ (init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
s : Finset α
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
by

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

Goal state before:
pp: α : Type u
s t : List α
⊢ s ∈ t.sublists' ↔ s <+ t

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).sublists'.length = 2 ^ (a :: l).length

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
s : Multiset α
⊢ ∀ (a : List α), ⟦a⟧ ∈ powersetAux l ↔ ⟦a⟧ ≤ ↑l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ powersetAux l ~ powersetAux' l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ cons b ∘ cons a = cons a ∘ cons b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ powersetAux' l₁ ~ powersetAux' l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
r : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α), x.toList ++ [y, a :: y] = ((x.push y).push (a :: y)).toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
l : List α
⊢ (a ::ₘ ⟦l⟧).powerset = powerset ⟦l⟧ + map (cons a) (powerset ⟦l⟧)

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ sublistsAux = fun a r ↦ (Array.foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ ∀ (a b : List α), ⟦a⟧ ∈ powerset ⟦b⟧ ↔ ⟦a⟧ ≤ ⟦b⟧

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
r : List (List α)
⊢ sublistsAux a [] = flatMap (fun l ↦ [l, a :: l]) []

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ map singleton ⟦l⟧ ≤ powerset ⟦l⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ ∀ (a : List α), (powerset ⟦a⟧).card = 2 ^ card ⟦a⟧

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
powerset : s.powerset = {0}
⊢ s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s = 0 → s.powerset = {0}

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l ↦ [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = flatMap (fun l ↦ [l, a :: l]) (r ++ [l])

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux' l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
by

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

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
s : Finset ι
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
⊢ motive s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : LinearOrder α
s : Finset β
f : β → α
h : s.Nonempty
⊢ ∃ x ∈ s, ∀ x' ∈ s, f x' ≤ f x

Tactic:
by

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).sublists = do
    let x ← l₂.sublists
    map (fun x_1 ↦ x_1 ++ x) l₁.sublists

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) i

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
⊢ IsGLB (↑s) i ↔ IsLeast (↑s) i

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.reverse.sublists = map reverse l.sublists'

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists = map reverse l.reverse.sublists'

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.reverse.sublists' = map reverse l.sublists

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists' = map reverse l.reverse.sublists

Tactic:
by

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

Goal state before:
pp: α : Type u
s t : List α
⊢ s ∈ t.sublists ↔ s <+ t

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists.length = 2 ^ l.length

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
a : α
ih : map pure l <+ l.sublists
⊢ [] ++ [a] = pure a

Tactic:
by

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

Goal state before:
pp: α : Type u_7
R : Type u_8
inst✝ : LinearOrder R
f : α → R
s : Multiset α
hs : s ≠ 0
⊢ ∃ y ∈ s, ∀ z ∈ s, f z ≤ f y

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ map pure l <+ l.sublists

Tactic:
by

Goal state after: