mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ ↑a✝

pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝ ≤ x ∧ x ≤ ⊤

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝¹ ≤ x ∧ x ≤ ↑a✝

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ⊤ ≤ x ∧ x ≤ ↑a✝

case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝ ≤ x ∧ x ≤ ⊤

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, none => {⊤}
      | none, Option.some b => ∅
      | Option.some a, none => insertTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Icc a b)) ↔
    ↑a✝¹ ≤ x ∧ x ≤ ↑a✝
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
⊢ (x ∈
      match ⊤, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < b

pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝ ≤ x ∧ x < b

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
⊢ (x ∈
      match ⊤, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < b

case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝ ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < ↑a✝

pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝ ≤ x ∧ x < ⊤

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝¹ ≤ x ∧ x < ↑a✝

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ⊤ ≤ x ∧ x < ↑a✝

case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝ ≤ x ∧ x < ⊤

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ici a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ico a b)) ↔
    ↑a✝¹ ≤ x ∧ x < ↑a✝
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
⊢ (x ∈
      match ⊤, b with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ b

pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, b with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝ < x ∧ x ≤ b

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
⊢ (x ∈
      match ⊤, b with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ b

case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, b with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝ < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n a : ℕ
⊢ Multiset.map (fun x ↦ x % a) (Multiset.Ico n (n + a)) = Multiset.range a

Tactic:
convert! congr_arg Finset.val (image_Ico_mod n a)

Goal state after:
case e'_2
n a : ℕ
⊢ Multiset.map (fun x ↦ x % a) (Multiset.Ico n (n + a)) = (image (fun x ↦ x % a) (Finset.Ico n (n + a))).val
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ ↑a✝

pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝ < x ∧ x ≤ ⊤

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝¹ < x ∧ x ≤ ↑a✝

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ⊤ < x ∧ x ≤ ↑a✝

case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝ < x ∧ x ≤ ⊤

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => insertTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioc a b)) ↔
    ↑a✝¹ < x ∧ x ≤ ↑a✝
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r → ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

pp: case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) → WellQuasiOrdered r

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r → ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ (∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))) → WellQuasiOrdered r
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
⊢ (x ∈
      match ⊤, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < b

pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝ < x ∧ x < b

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
⊢ (x ∈
      match ⊤, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < b

case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
b x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, b with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝ < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < ↑a✝

pp: case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝ < x ∧ x < ⊤

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝¹ < x ∧ x < ↑a✝

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
⊢ (x ∈
      match ⊤, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ⊤, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ⊤ < x ∧ x < ↑a✝

case coe.top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝ : α
⊢ (x ∈
      match ↑a✝, ⊤ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝ < x ∧ x < ⊤

case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : WithTop α
a✝¹ a✝ : α
⊢ (x ∈
      match ↑a✝¹, ↑a✝ with
      | none, x => ∅
      | Option.some a, none => Finset.map Embedding.coeWithTop (Ioi a)
      | Option.some a, Option.some b => Finset.map Embedding.coeWithTop (Ioo a b)) ↔
    ↑a✝¹ < x ∧ x < ↑a✝
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    (∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)) →
      ∀ (f : ℕ → (i : ι) → α i),
        ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ i ∈ Finset.cons a s h, r i ((f ∘ ⇑g) a_2 i) ((f ∘ ⇑g) b i)

Tactic:
intro i s hi ih f
    obtain ⟨g, hg⟩ := (hr i).exists_monotone_subseq (f · i)
    obtain ⟨g', hg'⟩ := ih (f ∘ g)
    refine ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩
    exact ⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_2.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : m < n
⊢ m = n

pp: case inr.refine_2.inr.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m : ℕ
hf : f (g m) = f (g m)
⊢ m = m

pp: case inr.refine_2.inr.inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : n < m
⊢ m = n

Tactic:
<;>

Goal state after:
case inr.refine_2.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : m < n
⊢ m = n

case inr.refine_2.inr.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m : ℕ
hf : f (g m) = f (g m)
⊢ m = m

case inr.refine_2.inr.inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
hf : f (g m) = f (g n)
h : n < m
⊢ m = n
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case zero
M : Type u_3
inst✝ : Monoid M
s : Set M
S : Submonoid M
hs : s ⊆ ↑S
⊢ s ^ 0 ⊆ ↑S

pp: case succ
M : Type u_3
inst✝ : Monoid M
s : Set M
S : Submonoid M
hs : s ⊆ ↑S
n✝ : ℕ
a✝ : s ^ n✝ ⊆ ↑S
⊢ s ^ (n✝ + 1) ⊆ ↑S

Tactic:
<;>

Goal state after:
case zero
M : Type u_3
inst✝ : Monoid M
s : Set M
S : Submonoid M
hs : s ⊆ ↑S
⊢ s ^ 0 ⊆ ↑S

case succ
M : Type u_3
inst✝ : Monoid M
s : Set M
S : Submonoid M
hs : s ⊆ ↑S
n✝ : ℕ
a✝ : s ^ n✝ ⊆ ↑S
⊢ s ^ (n✝ + 1) ⊆ ↑S
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y

Tactic:
have h₁ := transGen_wcovBy_of_le hz.1.1

Goal state after:
case neg
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun x1 x2 ↦ x1 ⩿ x2) x z
⊢ TransGen (fun x1 x2 ↦ x1 ⩿ x2) x y
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a : N), Commute (e x) a

pp: case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (b c : N), e x * (b * c) = e x * b * c

pp: case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a b : N), a * b * e x = a * (b * e x)

Tactic:
<;>

Goal state after:
case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a : N), Commute (e x) a

case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (b c : N), e x * (b * c) = e x * b * c

case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a b : N), a * b * e x = a * (b * e x)