awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ : List α
inst : DecidableEq α
a : α
nil : List.bagInter [] [a] = if Membership.mem (γ := List α) [] a then [a] else []
⊢ l₁.bagInter [a] = if a ∈ l₁ then [a] else []
have cons : ∀ (head : α) (tail : List α),
  (tail.bagInter [a] = if a ∈ tail then [a] else []) →
    (head :: tail).bagInter [a] = if a ∈ head :: tail then [a] else []
Tactic: induction l₁
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : ¬a ∈ l₁
⊢ l₁.bagInter (l₂.erase a) = l₁.bagInter l₂
have nil : ∀ {l₂ : List α} (h : ¬Membership.mem (γ := List α) [] a), List.bagInter [] (l₂.erase a) = List.bagInter [] l₂
Tactic: induction l₁ generalizing l₂
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : ¬a ∈ l₁
nil : ∀ {l₂ : List α} (h : ¬Membership.mem (γ := List α) [] a), List.bagInter [] (l₂.erase a) = List.bagInter [] l₂
⊢ l₁.bagInter (l₂.erase a) = l₁.bagInter l₂
have cons : ∀ (head : α) (tail : List α),
  (∀ {l₂ : List α} (h : ¬a ∈ tail), tail.bagInter (l₂.erase a) = tail.bagInter l₂) →
    ∀ {l₂ : List α} (h : ¬a ∈ head :: tail), (head :: tail).bagInter (l₂.erase a) = (head :: tail).bagInter l₂
Tactic: induction l₁ generalizing l₂
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : ¬a ∈ l₂
⊢ (l₁.erase a).bagInter l₂ = l₁.bagInter l₂
have nil : ∀ {l₂ : List α} (h : ¬a ∈ l₂), (List.erase [] a).bagInter l₂ = List.bagInter [] l₂
Tactic: induction l₁ generalizing l₂
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
a : α
inst : DecidableEq α
h : ¬a ∈ l₂
nil : ∀ {l₂ : List α} (h : ¬a ∈ l₂), (List.erase [] a).bagInter l₂ = List.bagInter [] l₂
⊢ (l₁.erase a).bagInter l₂ = l₁.bagInter l₂
have cons : ∀ (head : α) (tail : List α),
  (∀ {l₂ : List α} (h : ¬a ∈ l₂), (tail.erase a).bagInter l₂ = tail.bagInter l₂) →
    ∀ {l₂ : List α} (h : ¬a ∈ l₂), ((head :: tail).erase a).bagInter l₂ = (head :: tail).bagInter l₂
Tactic: induction l₁ generalizing l₂
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
b : α
l₁ l₂ : List α
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
have pos : ∀ (h : b ∈ l₂), (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
Tactic: by_cases h : b ∈ l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
b : α
l₁ l₂ : List α
pos : ∀ (h : b ∈ l₂), (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
have neg : ∀ (h : ¬b ∈ l₂), (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []
Tactic: by_cases h : b ∈ l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
⊢ (head :: tail).bagInter l₂ <+ (head :: tail) ∩ l₂
have cons : (if head ∈ l₂ then head :: tail.bagInter (l₂.erase head) else tail.bagInter l₂) <+ (head :: tail) ∩ l₂
Tactic: rw [cons_bagInter]
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
⊢ (if head ∈ l₂ then head :: tail.bagInter (l₂.erase head) else tail.bagInter l₂) <+ (head :: tail) ∩ l₂
have cons : head ∈ l₂ → head :: tail.bagInter (l₂.erase head) <+ (head :: tail) ∩ l₂
Tactic: split
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
cons : head ∈ l₂ → head :: tail.bagInter (l₂.erase head) <+ (head :: tail) ∩ l₂
⊢ (if head ∈ l₂ then head :: tail.bagInter (l₂.erase head) else tail.bagInter l₂) <+ (head :: tail) ∩ l₂
have cons₁ : ¬head ∈ l₂ → tail.bagInter l₂ <+ (head :: tail) ∩ l₂
Tactic: split
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
head : α
tail : List α
ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂
l₂ : List α
h : head ∈ l₂
⊢ head :: tail.bagInter (l₂.erase head) <+ (head :: tail) ∩ l₂
have cons : tail.bagInter (l₂.erase head) <+ tail ∩ l₂
Tactic: rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
⊢ l₁.bagInter l₂ <+ l₁ ∩ l₂
have nil : ∀ {l₂ : List α}, List.bagInter [] l₂ <+ [] ∩ l₂
Tactic: induction l₁ generalizing l₂ with
  | nil => simp
  | cons _ _ ih =>
    rw [cons_bagInter]
    split
    · rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]
      exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])
    · simp_all
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lattice (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
nil : ∀ {l₂ : List α}, List.bagInter [] l₂ <+ [] ∩ l₂
⊢ l₁.bagInter l₂ <+ l₁ ∩ l₂
have cons : ∀ (head : α) (tail : List α) (ih : ∀ {l₂ : List α}, tail.bagInter l₂ <+ tail ∩ l₂) {l₂ : List α},
  (head :: tail).bagInter l₂ <+ (head :: tail) ∩ l₂
Tactic: induction l₁ generalizing l₂ with
  | nil => simp
  | cons _ _ ih =>
    rw [cons_bagInter]
    split
    · rw [inter_cons_of_mem _ (by assumption), cons_sublist_cons]
      exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])
    · simp_all
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (hypothesis)
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 :: tl
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)
⊢ n = m
have hx₁ : ¬x = hd ∧ ¬x ∈ tl
Tactic: simp only [mem_cons, not_or] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
⊢ n = m
have 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
Tactic: cases n
Cleared hypotheses: n, hn, h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
⊢ n = m
have 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
Tactic: cases n
Cleared hypotheses: n, hn, h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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)
⊢ 0 = m
have 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
Tactic: cases m
Cleared hypotheses: m, hm, h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
⊢ 0 = m
have 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
Tactic: cases m
Cleared hypotheses: m, hm, h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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)
⊢ n + 1 = m
have 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
Tactic: cases m
Cleared hypotheses: m, hm, h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
⊢ n + 1 = m
have 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
Tactic: cases m
Cleared hypotheses: m, hm, h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (hypothesis)
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))
⊢ n + 1 = n_1 + 1
have h₁ : tl.insertIdx n x = tl.insertIdx n_1 x
Tactic: simp only [insertIdx_succ_cons, cons.injEq, true_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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 + 1 = n_1 + 1
have cons : n = n_1
Tactic: rw [Nat.succ_inj]
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
have cons : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n
Tactic: refine IH hx.right ?_ ?_ h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
⊢ n = n_1
have cons₁ : Membership.mem (γ := Set ℕ) {n : ℕ | n ≤ tl.length} n_1
Tactic: refine IH hx.right ?_ ?_ h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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)
⊢ n = m
have 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
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
Cleared hypotheses: l, hx, n, hn, m, hm, h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
⊢ n = m
have 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
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
Cleared hypotheses: l, hx, n, hn, m, hm, h
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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)
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
have cons : ∀ (c : γ) (hgf : g c = f b), foldr f a (b :: l) ∈ Set.range (foldr g a)
Tactic: obtain ⟨c, hgf⟩ := hfg (Set.mem_range_self b)
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
have cons : ∀ (m : List γ) (hgf' : foldr g a m = foldr f a l), foldr f a (b :: l) ∈ Set.range (foldr g a)
Tactic: obtain ⟨m, hgf'⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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
⊢ foldr f a (b :: l) ∈ Set.range (foldr g a)
have cons : g c (foldr g a m) ∈ Set.range (foldr g a)
Tactic: rw [foldr_cons, ← hgf, ← hgf']
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
l : List β
⊢ foldr f a l ∈ Set.range (foldr g a)
have nil : foldr f a [] ∈ 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⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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)
⊢ foldr f a l ∈ Set.range (foldr g a)
have cons : ∀ (b : β) (l : List β) (H : foldr f a l ∈ Set.range (foldr g a)), foldr f a (b :: 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⟩
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
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 : α
⊢ Subset.{u_1} (α := Set α) (Set.range fun (l : List β) ↦ foldl f a l) (Set.range fun (l : List γ) ↦ foldl g a l)
have 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)
Tactic: simp_rw [← (foldr_reverse), Set.range_comp' _ reverse,
    reverse_involutive.bijective.surjective.range_eq, Set.image_univ]
-- Lean 4 proof step from Mathlib.Data.List.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
φ : Type u_5
f : α → β → σ → σ × φ
a : α
as : List α
b : β
bs : List β
s : σ
⊢ 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))
have 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))
Tactic: simp only [mapAccumr₂, mapAccumr₂_eq_foldr f as]
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
r : α → α → Prop
inst : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂
have rel : ∀ (h : r a a), Lex r l₁ l₂
Tactic: obtain - | h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
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₂
⊢ Lex r l₁ l₂
have cons : ∀ (h : Lex r l₁ l₂), Lex r l₁ l₂
Tactic: obtain - | h | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
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₃
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
have inl : ∀ (ab : r a b), Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
Tactic: rcases trichotomous_of r a b with (ab | rfl | ab)
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
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₃)
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
have inr : Lex r (a :: l₁) (a :: l₂) ∨ Lex r (a :: l₂) (a :: l₃)
Tactic: rcases trichotomous_of r a b with (ab | rfl | ab)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
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₃)
⊢ Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
have inr₁ : ∀ (ab : r b a), Lex r (a :: l₁) (b :: l₂) ∨ Lex r (b :: l₂) (a :: l₃)
Tactic: rcases trichotomous_of r a b with (ab | rfl | ab)
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
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₁)
⊢ a :: l₁ = b :: l₂
have obtain : ∀ (hab : ¬Lex r (a :: l₁) (a :: l₂)) (hba : ¬Lex r (a :: l₂) (a :: l₁)), a :: l₁ = a :: l₂
Tactic: obtain rfl := Std.Trichotomous.trichotomous a b (mt rel hab) (mt rel hba)
Cleared hypotheses: b, hab, hba