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

Goal state before:
pp: case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)

Tactic:
·

Goal state after:
case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ StrictMono fun i ↦ if ↑i = 0 then n else m

pp: case mpr.refine_2
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ?mpr.refine_1) ix)

Tactic:
·

Goal state after:
case mpr.refine_1
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ StrictMono fun i ↦ if ↑i = 0 then n else m
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc ≍ (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j

Tactic:
·

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc ≍ (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1.zero.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi hj : 0 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

pp: case mpr.refine_1.zero.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

pp: case mpr.refine_1.succ.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
·

Goal state after:
case mpr.refine_1.zero.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi hj : 0 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1.zero.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

pp: case mpr.refine_1.succ.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
·

Goal state after:
case mpr.refine_1.zero.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨0, hi⟩ < ⟨n✝ + 1, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨0, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case i
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ Fin (n + 1)

pp: case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ i.insertNth a f (rev ?i) = i.rev.insertNth a (f ∘ rev) ?i

pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (succAbove ?i j✝).rev = i.rev.insertNth a (f ∘ rev) (succAbove ?i j✝)

Tactic:
·

Goal state after:
case i
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ Fin (n + 1)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1.succ.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩

pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
·

Goal state after:
case mpr.refine_1.succ.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
hj : 0 < (replicate 2 x).length
⊢ ⟨n✝ + 1, hi⟩ < ⟨0, hj⟩ → (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨0, hj⟩
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ i.insertNth a f i.rev.rev = i.rev.insertNth a (f ∘ rev) i.rev

pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (i.rev.succAbove j✝).rev = i.rev.insertNth a (f ∘ rev) (i.rev.succAbove j✝)

Tactic:
·

Goal state after:
case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ i.insertNth a f i.rev.rev = i.rev.insertNth a (f ∘ rev) i.rev
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩

Tactic:
·

Goal state after:
case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj : n✝ + 1 < (replicate 2 x).length
⊢ ⟨n✝¹ + 1, hi⟩ < ⟨n✝ + 1, hj⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj⟩
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (i.rev.succAbove j✝).rev = i.rev.insertNth a (f ∘ rev) (i.rev.succAbove j✝)

Tactic:
·

Goal state after:
case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (i.rev.succAbove j✝).rev = i.rev.insertNth a (f ∘ rev) (i.rev.succAbove j✝)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ Finite α

Tactic:
by
  rw [← finite_univ_iff, ← union_compl_self s]
  exact hs.union hsc

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

Goal state before:
pp: case mpr.refine_2
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ix)

Tactic:
·

Goal state after:
case mpr.refine_2
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
⊢ ∀ (ix : Fin (replicate 2 x).length),
    (replicate 2 x).get ix = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ix)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_2.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨0, hi⟩ = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨0, hi⟩)

pp: case mpr.refine_2.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)

Tactic:
·

Goal state after:
case mpr.refine_2.zero
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
hi : 0 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨0, hi⟩ = l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨0, hi⟩)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_2.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)

Tactic:
·

Goal state after:
case mpr.refine_2.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝ : ℕ
hi : n✝ + 1 < (replicate 2 x).length
⊢ (replicate 2 x).get ⟨n✝ + 1, hi⟩ =
    l.get ((OrderEmbedding.ofStrictMono (fun i ↦ if ↑i = 0 then n else m) ⋯) ⟨n✝ + 1, hi⟩)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : r x b
⊢ x :: a :: as <+ x :: b :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
⊢ x :: a :: as <+ b :: orderedInsert r x bs

pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
·

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : r x b
⊢ x :: a :: as <+ x :: b :: bs
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
⊢ fold op (op b₁ b₂) (s₁ + 0) = op (fold op b₁ s₁) (fold op b₂ 0)

Tactic:
by rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op]

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

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
⊢ x :: a :: as <+ b :: orderedInsert r x bs

pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
·

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : r x a
h✝ : ¬r x b
⊢ x :: a :: as <+ b :: orderedInsert r x bs
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (f a) (op (g a) (op (fold op u₁ (map f b)) (fold op u₂ (map g b)))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))

Tactic:
← ha.assoc (g a),

Goal state after:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (f a) (op (op (g a) (fold op u₁ (map f b))) (fold op u₂ (map g b))) =
    op (op (f a) (fold op u₁ (map f b))) (op (fold op u₂ (map g b)) (g a))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
·

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs

pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
·

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : ¬r x b
⊢ a :: orderedInsert r x as <+ b :: orderedInsert r x bs
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
·

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : r x a
⊢ x :: a :: as <+ x :: a :: bs
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs

Tactic:
·

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as bs : List α
hb : Pairwise r (a :: bs)
a✝ : as <+ bs
hr : ¬r x a
⊢ a :: orderedInsert r x as <+ a :: orderedInsert r x bs
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
·

Goal state after:
case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
·

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
·

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg.inl
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
b : α
l : List α
h : Pairwise r (b :: l)
b' : α
h' : ¬r b' b
bm : b' ∈ List.orderedInsert r b' l
⊢ r b b'

pp: case neg.inr
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'

Tactic:
·

Goal state after:
case neg.inl
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
b : α
l : List α
h : Pairwise r (b :: l)
b' : α
h' : ¬r b' b
bm : b' ∈ List.orderedInsert r b' l
⊢ r b b'
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg.inr
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'

Tactic:
·

Goal state after:
case neg.inr
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op c b = op b c

pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : s = ∅
⊢ op c b = op b c
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∉ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
h : a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)