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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum

pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : ¬tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)

pp: case cons.tail
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
·

Goal state after:
case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons.tail
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
·

Goal state after:
case cons.tail
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ x :: l
⊢ a ≤ max x (foldr max b l)

pp: case cons.inr
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)

Tactic:
·

Goal state after:
case cons.inl
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ x :: l
⊢ a ≤ max x (foldr max b l)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)

Tactic:
·

Goal state after:
case cons.inr
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
hl : x ∈ l
⊢ a ≤ max y (foldr max b l)
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (max a b) = f a ⊔ f b

pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (max a b) = f a ⊔ f b

Tactic:
·

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (max a b) = f a ⊔ f b
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (max a b) = f a ⊔ f b

Tactic:
·

Goal state after:
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (max a b) = f a ⊔ f b
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (min a b) = f a ⊓ f b

pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (min a b) = f a ⊓ f b

Tactic:
·

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f (min a b) = f a ⊓ f b
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (min a b) = f a ⊓ f b

Tactic:
·

Goal state after:
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (min a b) = f a ⊓ f b
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 lia

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

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

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

Tactic:
·

Goal state after:
case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).max ≠ ↑x
Module: Mathlib.Data.Finset.Max

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

Tactic:
·

Goal state after:
case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ (s.erase x).max ≠ ↑x
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l ↦ r.push (x :: l)) y.toList.toArray y.toList.toArray).toList =
      (Array.foldl (fun r l ↦ r.push (x :: l)) y y).toList

Tactic:
·

Goal state after:
α : Type u
l : List α
⊢ ∀ (x : α) (y : Array (List α)),
    (Array.foldl (fun r l ↦ r.push (x :: l)) y.toList.toArray y.toList.toArray).toList =
      (Array.foldl (fun r l ↦ r.push (x :: l)) y y).toList
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

pp: case mpr
α : 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 →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)

Tactic:
·

Goal state after:
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
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mp.inl
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl

pp: case mp.inr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ tl.inits.zip tl.tails
⊢ (fun t ↦ hd :: t) w✝¹ ++ id w✝ = hd :: tl

Tactic:
·

Goal state after:
case mp.inl
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mp.inr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ tl.inits.zip tl.tails
⊢ (fun t ↦ hd :: t) w✝¹ ++ id w✝ = hd :: tl

Tactic:
·

Goal state after:
case mp.inr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ tl.inits.zip tl.tails
⊢ (fun t ↦ hd :: t) w✝¹ ++ id w✝ = hd :: tl
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mpr
α : 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 →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)

Tactic:
·

Goal state after:
case mpr
α : 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 →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)
Module: Mathlib.Data.List.Zip

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

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

Tactic:
·

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

Goal state before:
pp: case cons.mp
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t

pp: case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

Tactic:
·

Goal state after:
case cons.mp
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mp.inl
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t

pp: case cons.mp.inr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t

Tactic:
·

Goal state after:
case cons.mp.inl
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t
Module: Mathlib.Data.List.Zip

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

Tactic:
·

Goal state after:
case mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
⊢ hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (hd' :: tl', tail)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mp.inr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t

Tactic:
·

Goal state after:
case cons.mp.inr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t
Module: Mathlib.Data.Finset.Max

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

pp: case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
⊢ motive s

Tactic:
·

Goal state after:
case H.inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
ih : ∀ s ∈ ∅, motive (∅.erase s)
⊢ motive ∅
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

Tactic:
·

Goal state after:
case cons.mpr
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
Module: Mathlib.Data.Finset.Max

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

Tactic:
·

Goal state after:
case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
⊢ motive s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mpr.cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

pp: case cons.mpr.cons_cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝

Tactic:
·

Goal state after:
case cons.mpr.cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons.mpr.cons_cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝

Tactic:
·

Goal state after:
case cons.mpr.cons_cons
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁✝ : List α
h : l₁✝ <+ t
⊢ a :: l₁✝ <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: l₁✝
Module: Mathlib.Data.Finset.Max

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

pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
⊢ motive s

Tactic:
·

Goal state after:
case H.inl
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : image f s = ∅
⊢ motive s
Module: Mathlib.Data.Finset.Max

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

Tactic:
·

Goal state after:
case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
⊢ motive s
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:
induction s using Finset.eraseInduction with | _ s ihs
  rcases (s.image f).eq_empty_or_nonempty with (hne | hne)
  · simp only [image_eq_empty] at hne
    simp only [hne, empty]
  · have H : (s.image f).max' hne ∈ s.image f := max'_mem (s.image f) hne
    simp only [mem_image] at H
    rcases H with ⟨a, has, hfa⟩
    rw [← insert_erase has]
    refine insert _ _ (notMem_erase a s) (fun x hx => ?_) (ihs a has)
    rw [hfa]
    exact le_max' _ _ (mem_image_of_mem _ <| mem_of_mem_erase hx)

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
  simp only [sublists, foldr_append]
  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
⊢ [] <+ [].sublists

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

Tactic:
·

Goal state after:
case nil
α : Type u
⊢ [] <+ [].sublists
Module: Mathlib.Data.List.Sublists

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

Tactic:
length_sublistsLen n l,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ l.length.choose (n + 1) + l.length.choose n = (a :: l).length.choose (n + 1)
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) (a :: l₂✝)

Tactic:
sublistsLen_succ_cons

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: case inl
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ l'.length = n + 1

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

Tactic:
·

Goal state after:
case inl
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ l'.length = n + 1
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:
·

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

Goal state before:
pp: case cons.nil
α : Type u
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen [].length l₂
⊢ [] ∈ sublistsLen [].length (a :: l₂)

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 (b :: l₁).length (a :: l₂)

Tactic:
·

Goal state after:
case cons.nil
α : Type u
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen [].length l₂
⊢ [] ∈ sublistsLen [].length (a :: l₂)
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 (b :: l₁).length (a :: 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 (b :: l₁).length (a :: l₂)
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) (a :: l₂)

Tactic:
sublistsLen_succ_cons

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) (a :: l₂✝)

Tactic:
sublistsLen_succ_cons

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₂✝)