mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h : Forall₂ (fun x1 x2 ↦ x1 ≤ x2) l₁ l₂
⊢ l₁.prod ≤ l₂.prod

Tactic:
by
  induction h with
  | nil => rfl
  | cons hab ih ih' => simpa only [prod_cons] using mul_le_mul' hab ih'

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
<;>

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ ∀ (i : α), i ∈ l → f i ≤ max (f i) (g i)

pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ ∀ (i : α), i ∈ l → g i ≤ max (f i) (g i)

Tactic:
<;>

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ ∀ (i : α), i ∈ l → f i ≤ max (f i) (g i)

case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ ∀ (i : α), i ∈ l → g i ≤ max (f i) (g i)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod

pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod

Tactic:
<;>

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod

case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ ∀ (i : α), i ∈ l → min (f i) (g i) ≤ f i

pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ ∀ (i : α), i ∈ l → min (f i) (g i) ≤ g i

Tactic:
<;>

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ ∀ (i : α), i ∈ l → min (f i) (g i) ≤ f i

case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ ∀ (i : α), i ∈ l → min (f i) (g i) ≤ g i
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b → Lex r (fun i ↦ Function.swap (s i)) b a

pp: case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r (fun i ↦ Function.swap (s i)) b a → Lex (Function.swap r) s a b

Tactic:
<;>

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex (Function.swap r) s a b → Lex r (fun i ↦ Function.swap (s i)) b a

case mpr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
⊢ Lex r (fun i ↦ Function.swap (s i)) b a → Lex (Function.swap r) s a b
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case pos
M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : p
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

pp: case neg
M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : ¬p
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
<;>

Goal state after:
case pos
M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : p
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

case neg
M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : ¬p
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mpr.inr
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
a : α b.fst
h : s b.fst (⋯ ▸ a) b.snd
⊢ Lex r s ⟨b.fst, a⟩ b

Tactic:
· exact Lex.right _ h

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case none
α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
⊢ ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) none = f none

pp: case some
α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
val✝ : α
⊢ ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) (some val✝) = f (some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
⊢ ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) none = f none

case some
α : Type ?u.8
β : Type ?u.9
f : Option α ↪ β
val✝ : α
⊢ ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) f)) (some val✝) = f (some val✝)
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case a
α : Type ?u.8
β : Type ?u.9
x✝¹ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
x✝ : α
⊢ ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩)).fst x✝ =
    ⟨f, ⟨y, hy⟩⟩.fst x✝

pp: case a
α : Type ?u.8
β : Type ?u.9
x✝ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
⊢ ↑((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩)).snd =
    ↑⟨f, ⟨y, hy⟩⟩.snd

Tactic:
<;>

Goal state after:
case a
α : Type ?u.8
β : Type ?u.9
x✝¹ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
x✝ : α
⊢ ((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩)).fst x✝ =
    ⟨f, ⟨y, hy⟩⟩.fst x✝

case a
α : Type ?u.8
β : Type ?u.9
x✝ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
⊢ ↑((fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩)).snd =
    ↑⟨f, ⟨y, hy⟩⟩.snd
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type ?u.3
s t : Set α
h✝ : s ⊆ t
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : (fun x ↦ ⟨↑x, ⋯⟩) ⟨x, hx⟩ = (fun x ↦ ⟨↑x, ⋯⟩) ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
by
    congr
    injection h

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ map (FreeMonoid.lift f) ⊤ = closure (Set.range f)

Tactic:
← FreeMonoid.closure_range_of,

Goal state after:
M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ map (FreeMonoid.lift f) (closure (Set.range FreeMonoid.of)) = closure (Set.range f)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
h✝ : r hd val✝
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
h✝ : ¬r hd val✝
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
h✝ : r hd val✝
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)

case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
h✝ : ¬r hd val✝
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
h✝ : foldl (argAux r) (some a✝) l✝ = none
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) none → m ∈ a✝ :: (l✝ ++ [a✝²])

pp: case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ val✝ : α
h✝ : foldl (argAux r) (some a✝) l✝ = some val✝
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) (some val✝) → m ∈ a✝ :: (l✝ ++ [a✝²])

Tactic:
<;>

Goal state after:
case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ : α
h✝ : foldl (argAux r) (some a✝) l✝ = none
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) none → m ∈ a✝ :: (l✝ ++ [a✝²])

case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l l✝ : List α
a✝² : α
a✝¹ : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l✝ → m ∈ a :: l✝
a✝ val✝ : α
h✝ : foldl (argAux r) (some a✝) l✝ = some val✝
⊢ ∀ (m : α),
    m ∈ Option.rec (some a✝²) (fun val ↦ if r a✝² val then some a✝² else some val) (some val✝) → m ∈ a✝ :: (l✝ ++ [a✝²])
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case some.head
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
ham : f m ≤ f hd
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

pp: case some.tail
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
a✝ : Mem a tl
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
<;>

Goal state after:
case some.head
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
ham : f m ≤ f hd
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

case some.tail
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
a✝ : Mem a tl
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : f hd < f val✝
hm : some val✝ = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : ¬f hd < f val✝
hm : some hd = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
hm : some val✝ = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
hm : some hd = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : f hd < f val✝
hm : some val✝ = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : ¬f hd < f val✝
hm : some hd = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
hm : some val✝ = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
hm : some hd = some m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : f hd < f val✝
hm : val✝ = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : ¬f hd < f val✝
hm : hd = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
hm : val✝ = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
hm : hd = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : f hd < f val✝
hm : val✝ = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m val✝ : α
h : argmax f tl = some val✝
ham : f m ≤ f hd
h✝ : ¬f hd < f val✝
hm : hd = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
hm : val✝ = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
hm : hd = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match false, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit false n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match false, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit false n.div2

pp: case true
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match true, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit true n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match true, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit true n.div2

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match false, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit false n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match false, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit false n.div2

case true
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match true, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit true n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match true, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit true n.div2
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case bot
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
l : List α
a : α
ha : a ∈ l
h : l.maximum = ⊥
⊢ ¬⊥ < ↑a

pp: case coe
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
l : List α
a : α
ha : a ∈ l
a✝ : α
h : l.maximum = ↑a✝
⊢ ¬↑a✝ < ↑a

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
l : List α
a : α
ha : a ∈ l
h : l.maximum = ⊥
⊢ ¬⊥ < ↑a

case coe
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
l : List α
a : α
ha : a ∈ l
a✝ : α
h : l.maximum = ↑a✝
⊢ ¬↑a✝ < ↑a
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ inl x ∈ u.toLeft.disjSum u.toRight ↔ inl x ∈ u

pp: case inr
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ inr x ∈ u.toLeft.disjSum u.toRight ↔ inr x ∈ u

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ inl x ∈ u.toLeft.disjSum u.toRight ↔ inl x ∈ u

case inr
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ inr x ∈ u.toLeft.disjSum u.toRight ↔ inr x ∈ u
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∀ a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x), a ∈ s

Tactic:
intro a ha; simpa using! (List.mem_filter.mp ha).2

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ [].maximum ↔ ∃ b, b ∈ [] ∧ a ≤ b

pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : ↑a ≤ tail✝.maximum ↔ ∃ b, b ∈ tail✝ ∧ a ≤ b
⊢ ↑a ≤ (head✝ :: tail✝).maximum ↔ ∃ b, b ∈ head✝ :: tail✝ ∧ a ≤ b

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ [].maximum ↔ ∃ b, b ∈ [] ∧ a ≤ b

case cons
α : Type u_1
inst✝ : LinearOrder α
l : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : ↑a ≤ tail✝.maximum ↔ ∃ b, b ∈ tail✝ ∧ a ≤ b
⊢ ↑a ≤ (head✝ :: tail✝).maximum ↔ ∃ b, b ∈ head✝ :: tail✝ ∧ a ≤ b
Module: Mathlib.Data.Finset.Lattice.Union

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ (∃ i ∈ s, a✝ ∈ t i) ↔ a✝ ∈ s.biUnion t

Tactic:
mem_biUnion

Goal state after:
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
a✝ : β
⊢ (∃ i ∈ s, a✝ ∈ t i) ↔ ∃ a ∈ s, a✝ ∈ t a
Module: Mathlib.Data.List.Zip

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

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ (head✝ :: tail✝).inits.zip (head✝ :: tail✝).tails ↔ init ++ tail = head✝ :: tail✝

Tactic:
<;>

Goal state after:
case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ [].inits.zip [].tails ↔ init ++ tail = []

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ (head✝ :: tail✝).inits.zip (head✝ :: tail✝).tails ↔ init ++ tail = head✝ :: tail✝
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) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails → 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) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails

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) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails → init ++ tail = hd :: tl

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) :: (map (fun t ↦ hd :: t) tl.inits).zip tl.tails
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 α
⊢ (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 α
⊢ s <+ a :: t → s <+ t ∨ ∃ a_2, a_2 <+ t ∧ a :: a_2 = s

Tactic:
<;>

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

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