awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) n) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) m)
hx : ¬x = hd ∧ ¬x ∈ tl
cons :
  ∀ (hn : 0 ≤ tl.length + 1)
    (h :
      Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0)
        ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) m)),
    0 = m
cons₁ :
  ∀ (n : ℕ) (hn : n + 1 ≤ tl.length + 1)
    (h :
      Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n + 1))
        ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) m)),
    n + 1 = m
⊢ n = m

Tactic:
cases n
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
m : ℕ
hm : m ≤ tl.length + 1
hx : ¬x = hd ∧ ¬x ∈ tl
hn : 0 ≤ tl.length + 1
h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) m)
cons :
  ∀ (hm : 0 ≤ tl.length + 1)
    (h :
      Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0)
        ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0)),
    Eq (α := ℕ) 0 0
cons₁ :
  ∀ (n : ℕ) (hm : n + 1 ≤ tl.length + 1)
    (h :
      Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0)
        ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n + 1))),
    0 = n + 1
⊢ 0 = m

Tactic:
cases m
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
m : ℕ
hm : m ≤ tl.length + 1
hx : ¬x = hd ∧ ¬x ∈ tl
n : ℕ
hn : n + 1 ≤ tl.length + 1
h :
  Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n + 1))
    ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) m)
cons :
  ∀ (hm : 0 ≤ tl.length + 1)
    (h :
      Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n + 1))
        ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0)),
    n + 1 = 0
cons₁ :
  ∀ (n_1 : ℕ) (hm : n_1 + 1 ≤ tl.length + 1)
    (h :
      Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n + 1))
        ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n_1 + 1))),
    n + 1 = n_1 + 1
⊢ n + 1 = m

Tactic:
cases m
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
hn hm : 0 ≤ tl.length + 1
h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0)
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
hn : 0 ≤ tl.length + 1
n : ℕ
hm : n + 1 ≤ tl.length + 1
h :
  Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0)
    ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n + 1))
⊢ 0 = n + 1

Tactic:
simp [hx.left] at h

Premises used: And.left
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n : ℕ
hn : n + 1 ≤ tl.length + 1
hm : 0 ≤ tl.length + 1
h :
  Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n + 1))
    ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) 0)
⊢ n + 1 = 0

Tactic:
simp [Ne.symm hx.left] at h

Premises used: Ne.symm, And.left
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n : ℕ
hn : n + 1 ≤ tl.length + 1
n_1 : ℕ
hm : n_1 + 1 ≤ tl.length + 1
h :
  Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n + 1))
    ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) (n_1 + 1))
⊢ tl.insertIdx n x = tl.insertIdx n_1 x

Tactic:
simp only [insertIdx_succ_cons, cons.injEq, true_and] at h

Premises used: List.insertIdx_succ_cons, List.cons.injEq, true_and
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n : ℕ
hn : n + 1 ≤ tl.length + 1
n_1 : ℕ
hm : n_1 + 1 ≤ tl.length + 1
h : tl.insertIdx n x = tl.insertIdx n_1 x
cons : n = n_1
⊢ n + 1 = n_1 + 1

Tactic:
rw [Nat.succ_inj]

Premises used: Nat.succ_inj
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n : ℕ
hn : n + 1 ≤ tl.length + 1
n_1 : ℕ
hm : n_1 + 1 ≤ tl.length + 1
h : tl.insertIdx n x = tl.insertIdx n_1 x
⊢ n = n_1

Tactic:
IH hx.right ?_ ?_ h

Premises used: And.right
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n : ℕ
hn : n + 1 ≤ tl.length + 1
n_1 : ℕ
hm : n_1 + 1 ≤ tl.length + 1
h : tl.insertIdx n x = tl.insertIdx n_1 x
cons : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n
cons₁ : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n_1
⊢ n = n_1

Tactic:
refine IH hx.right ?_ ?_ h

Premises used: And.right
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n : ℕ
hn : n + 1 ≤ tl.length + 1
n_1 : ℕ
hm : n_1 + 1 ≤ tl.length + 1
h : tl.insertIdx n x = tl.insertIdx n_1 x
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n

Tactic:
simpa [Nat.succ_le_succ_iff] using hn

Premises used: Nat.succ_le_succ_iff
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
x hd : α
tl : List α
IH :
  ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)), n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n : ℕ
hn : n + 1 ≤ tl.length + 1
n_1 : ℕ
hm : n_1 + 1 ≤ tl.length + 1
h : tl.insertIdx n x = tl.insertIdx n_1 x
⊢ Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n_1

Tactic:
simpa [Nat.succ_le_succ_iff] using hm

Premises used: Nat.succ_le_succ_iff
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
n : ℕ
hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ l.length} n
m : ℕ
hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ l.length} m
h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ l.insertIdx k x) n) ((fun (k : ℕ) ↦ l.insertIdx k x) m)
nil :
  ∀ (hx : ¬Membership.mem (γ := List α) [] x) ⦃n : ℕ⦄
    (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ length.{u_1} (α := α) []} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ length.{u_1} (α := α) []} m)
    (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ insertIdx [] k x) n) ((fun (k : ℕ) ↦ insertIdx [] k x) m)), n = m
cons :
  ∀ (hd : α) (tl : List α)
    (IH :
      ∀ (hx : ¬x ∈ tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n) ⦃m : ℕ⦄
        (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} m)
        (h : Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ tl.insertIdx k x) n) ((fun (k : ℕ) ↦ tl.insertIdx k x) m)),
        n = m)
    (hx : ¬x ∈ hd :: tl) ⦃n : ℕ⦄ (hn : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ (hd :: tl).length} n) ⦃m : ℕ⦄
    (hm : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ (hd :: tl).length} m)
    (h :
      Eq.{u_1 + 1} (α := List α) ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) n)
        ((fun (k : ℕ) ↦ (hd :: tl).insertIdx k x) m)),
    n = m
⊢ n = m

Tactic:
induction l generalizing n m with
  | nil =>
    simp_all [Set.mem_singleton_iff, Set.setOf_eq_eq_singleton, length]
  | cons hd tl IH =>
    simp only [length, Set.mem_setOf_eq] at hn hm
    simp only [mem_cons, not_or] at hx
    cases n <;> cases m
    · rfl
    · simp [hx.left] at h
    · simp [Ne.symm hx.left] at h
    · simp only [insertIdx_succ_cons, cons.injEq, true_and] at h
      rw [Nat.succ_inj]
      refine IH hx.right ?_ ?_ h
      · simpa [Nat.succ_le_succ_iff] using hn
      · simpa [Nat.succ_le_succ_iff] using hm

Premises used: Nat.succ_inj, Set.setOf_eq_eq_singleton, List.insertIdx_succ_cons, Set.mem_setOf_eq, not_or, List.cons, List.cons.injEq, Set.mem_singleton_iff, Nat.succ_le_succ_iff, List.mem_cons, List.length, true_and, List.nil
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ foldr f a [] ∈ Set.range (foldr g a)

Tactic:
⟨[], rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl, List.nil
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ foldr f a [] ∈ Set.range (foldr g a)

Tactic:
exact ⟨[], rfl⟩
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
cons : ∀ (c : γ) (hgf : g c = f b), foldr f a (b :: l) ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)

Tactic:
obtain ⟨c, hgf⟩ := hfg (Set.mem_range_self b)

Premises used: Set.mem_range_self
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
H : foldr f a l ∈ Set.range (foldr g a)
c : γ
hgf : g c = f b
cons : ∀ (m : List γ) (hgf' : foldr g a m = foldr f a l), foldr f a (b :: l) ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)

Tactic:
obtain ⟨m, hgf'⟩ := H
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
cons : g c (foldr g a m) ∈ Set.range (foldr g a)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)

Tactic:
rw [foldr_cons, ← hgf, ← hgf']

Premises used: List.foldr_cons
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)

Tactic:
⟨c :: m, rfl⟩

Premises used: Set.Mem, setOf, List.cons, Exists.intro, Set.range, rfl
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
b : β
l : List β
c : γ
hgf : g c = f b
m : List γ
hgf' : foldr g a m = foldr f a l
⊢ g c (foldr g a m) ∈ Set.range (foldr g a)

Tactic:
exact ⟨c :: m, rfl⟩
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
l : List β
nil : foldr f a [] ∈ Set.range (foldr g a)
cons : ∀ (b : β) (l : List β) (H : foldr f a l ∈ Set.range (foldr g a)), foldr f a (b :: l) ∈ Set.range (foldr g a)
⊢ foldr f a l ∈ Set.range (foldr g a)

Tactic:
induction l with
  | nil => exact ⟨[], rfl⟩
  | cons b l H =>
    obtain ⟨c, hgf⟩ := hfg (Set.mem_range_self b)
    obtain ⟨m, hgf'⟩ := H
    rw [foldr_cons, ← hgf, ← hgf']
    exact ⟨c :: m, rfl⟩

Premises used: List.foldr_cons, List.cons, List.nil
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg :
  Subset.{u_1} (α := Set ((c : α) → α)) (Set.range fun (a : β) (c : α) ↦ f c a) (Set.range fun (b : γ) (c : α) ↦ g c b)
a : α
simp_rw :
  Set.range.{u_1, u_2 + 1} (ι := List β) (foldr (fun (y : β) (x : α) ↦ f x y) a) ⊆
    Set.range.{u_1, u_3 + 1} (ι := List γ) (foldr (fun (y : γ) (x : α) ↦ g x y) a)
⊢ Subset.{u_1} (α := Set α) (Set.range fun (l : List β) ↦ foldl f a l) (Set.range fun (l : List γ) ↦ foldl g a l)

Tactic:
simp_rw [← (foldr_reverse), Set.range_comp' _ reverse,
    reverse_involutive.bijective.surjective.range_eq, Set.image_univ]

Premises used: Set.image_univ, List.foldr_reverse, Function.Surjective.range_eq, Function.Bijective.surjective, List.reverse, Function.Involutive.bijective, List.reverse_involutive, Set.range_comp'
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg :
  Subset.{u_1} (α := Set ((c : α) → α)) (Set.range fun (a : β) (c : α) ↦ f c a) (Set.range fun (b : γ) (c : α) ↦ g c b)
a : α
⊢ Set.range.{u_1, u_2 + 1} (ι := List β) (foldr (fun (y : β) (x : α) ↦ f x y) a) ⊆
    Set.range.{u_1, u_3 + 1} (ι := List γ) (foldr (fun (y : γ) (x : α) ↦ g x y) a)

Tactic:
foldr_range_subset_of_range_subset hfg a

Premises used: List.foldr_range_subset_of_range_subset
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg :
  Subset.{u_1} (α := Set ((c : α) → α)) (Set.range fun (a : β) (c : α) ↦ f c a) (Set.range fun (b : γ) (c : α) ↦ g c b)
a : α
⊢ Set.range.{u_1, u_2 + 1} (ι := List β) (foldr (fun (y : β) (x : α) ↦ f x y) a) ⊆
    Set.range.{u_1, u_3 + 1} (ι := List γ) (foldr (fun (y : γ) (x : α) ↦ g x y) a)

Tactic:
exact foldr_range_subset_of_range_subset hfg a

Premises used: List.foldr_range_subset_of_range_subset
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f = Set.range g
a : α
⊢ Set.range (foldr f a) = Set.range (foldr g a)

Tactic:
(foldr_range_subset_of_range_subset hfg.le a).antisymm
    (foldr_range_subset_of_range_subset hfg.ge a)

Premises used: Eq.ge, Eq.le, HasSubset.Subset.antisymm, List.foldr_range_subset_of_range_subset
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → α
g : α → γ → α
hfg :
  Eq.{u_1 + 1} (α := Set ((c : α) → α)) (Set.range fun (a : β) (c : α) ↦ f c a) (Set.range fun (b : γ) (c : α) ↦ g c b)
a : α
⊢ Set.range (foldl f a) = Set.range (foldl g a)

Tactic:
(foldl_range_subset_of_range_subset hfg.le a).antisymm
    (foldl_range_subset_of_range_subset hfg.ge a)

Premises used: Eq.ge, List.foldl_range_subset_of_range_subset, Eq.le, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
f : α → σ → σ × β
a : α
as : List α
s : σ
⊢ mapAccumr f (a :: as) s =
    foldr
      (fun (a : α) (s : Prod.{u_4, u_2} σ (List β)) ↦
        let r := f a s.1;
        (r.1, r.2 :: s.2))
      (s, []) (a :: as)

Tactic:
simp only [mapAccumr, foldr, mapAccumr_eq_foldr f as]

Premises used: List.mapAccumr, List.foldr
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
simp :
  ((f a b
          (foldr (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2))
              (s, []) (as.zip bs)).1).1,
      (f a b
            (foldr
                (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2))
                (s, []) (as.zip bs)).1).2 ::
        (foldr (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2))
            (s, []) (as.zip bs)).2) =
    foldr (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2))
      (s, []) ((a :: as).zip (b :: bs))
⊢ mapAccumr₂ f (a :: as) (b :: bs) s =
    foldr
      (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦
        let r := f ab.1 ab.2 s.1;
        (r.1, r.2 :: s.2))
      (s, []) ((a :: as).zip (b :: bs))

Tactic:
simp only [mapAccumr₂, mapAccumr₂_eq_foldr f as]

Premises used: List.mapAccumr₂
-- Module: Mathlib.Data.List.Lemmas
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ ((f a b
          (foldr (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2))
              (s, []) (as.zip bs)).1).1,
      (f a b
            (foldr
                (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2))
                (s, []) (as.zip bs)).1).2 ::
        (foldr (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2))
            (s, []) (as.zip bs)).2) =
    foldr (fun (ab : α × β) (s : Prod.{u_4, u_5} σ (List φ)) ↦ ((f ab.1 ab.2 s.1).1, (f ab.1 ab.2 s.1).2 :: s.2))
      (s, []) ((a :: as).zip (b :: bs))

Tactic:
rfl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
rel : ∀ (h : r a a), Lex r l₁ l₂
cons : ∀ (h : Lex r l₁ l₂), Lex r l₁ l₂
⊢ Lex r l₁ l₂

Tactic:
obtain - | h | h := h
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : Std.Irrefl r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂

Tactic:
(irrefl_of r a h).elim

Premises used: False.elim, irrefl_of
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂

Tactic:
h
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : Std.Irrefl r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂

Tactic:
exacts [(irrefl_of r a h).elim, h]

Premises used: False.elim, irrefl_of
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
l : List α
⊢ Lex r [] l ∨ l = []

Tactic:
match l with
  | [] => Or.inr rfl
  | _ :: _ => .inl .nil

Premises used: _private.0.List.lex_nil_or_eq_nil.match_1, List.Lex.nil, Or.inl, Or, Eq, List.Lex, Or.inr, rfl, List.nil
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
a b : α
⊢ Lex r [a] [b] ↔ r a b

Tactic:
⟨fun | .rel h => h, .rel⟩

Premises used: _private.0.List.lex_singleton_iff.match_1, List.Lex.rel, Iff.intro
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : IsOrderConnected α r
inst_1 : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
inl : ∀ (ab : r a b), Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
inr : Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)
inr₁ : ∀ (ab : r b a), Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
rcases trichotomous_of r a b with (ab | rfl | ab)

Premises used: trichotomous_of, rfl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : IsOrderConnected α r
inst_1 : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
Or.inl (rel ab)

Premises used: List.Lex.rel, Or.inl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : IsOrderConnected α r
inst_1 : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r a b
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
exact Or.inl (rel ab)

Premises used: List.Lex.rel, Or.inl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : IsOrderConnected α r
inst_1 : Std.Trichotomous r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)

Tactic:
(aux _ l₂ _ h).imp cons cons

Premises used: Or.imp, List.Lex.cons
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : IsOrderConnected α r
inst_1 : Std.Trichotomous r
a : α
l₁ l₂ l₃ : List α
h : Lex r l₁ l₃
⊢ Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)

Tactic:
exact (aux _ l₂ _ h).imp cons cons

Premises used: Or.imp, List.Lex.cons
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : IsOrderConnected α r
inst_1 : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
Or.inr (rel ab)

Premises used: List.Lex.rel, Or.inr
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : IsOrderConnected α r
inst_1 : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ l₃ : List α
h : Lex r l₁ l₃
ab : r b a
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)

Tactic:
exact Or.inr (rel ab)

Premises used: List.Lex.rel, Or.inr
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ : List α
hab : ¬Lex r (a :: l₁) (b :: l₂)
hba : ¬Lex r (b :: l₂) (a :: l₁)
obtain : ∀ (hab : ¬Lex r (a :: l₁) (a :: l₂)) (hba : ¬Lex r (a :: l₂) (a :: l₁)), a :: l₁ = a :: l₂
⊢ a :: l₁ = b :: l₂

Tactic:
obtain rfl := Std.Trichotomous.trichotomous a b (mt rel hab) (mt rel hba)

Premises used: mt, List.Lex.rel, Std.Trichotomous.trichotomous, rfl
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
r : α → α → Prop
inst : Std.Trichotomous r
a : α
l₁ l₂ : List α
hab : ¬Lex r (a :: l₁) (a :: l₂)
hba : ¬Lex r (a :: l₂) (a :: l₁)
rw rw₁ : a :: l₂ = a :: l₂
⊢ a :: l₁ = a :: l₂

Tactic:
rw [aux l₁ l₂ (mt cons hab) (mt cons hba)]

Premises used: mt, List.Lex.cons
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
l₁ : List α
h : Lex r l₁ []
⊢ False

Tactic:
cases h
-- Module: Mathlib.Data.List.Lex
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
haveI : (this : Decidable (Lex r l₁ l₂)) → Decidable (Lex r (a :: l₁) (b :: l₂))
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))

Tactic:
haveI := decidableRel r l₁ l₂