awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
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₁)
⊢ a :: l₁ = a :: l₂
have rw : a :: l₂ = a :: l₂
Tactic: rw [aux l₁ l₂ (mt cons hab) (mt cons hba)]
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))
have haveI : (this : Decidable (Lex r l₁ l₂)) → Decidable (Lex r (a :: l₁) (b :: l₂))
Tactic: haveI := decidableRel r l₁ l₂
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))
have refine_1 : ∀ (h : r a b ∨ a = b ∧ Lex r l₁ l₂), Lex r (a :: l₁) (b :: l₂)
Tactic: refine decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
refine_1 : ∀ (h : r a b ∨ a = b ∧ Lex r l₁ l₂), Lex r (a :: l₁) (b :: l₂)
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))
have refine_2 : ∀ (h : Lex r (a :: l₁) (b :: l₂)), r a b ∨ a = b ∧ Lex r l₁ l₂
Tactic: refine decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b ∨ a = b ∧ Lex r l₁ l₂
⊢ Lex r (a :: l₁) (b :: l₂)
have refine_1 : ∀ (h : r a b), Lex r (a :: l₁) (b :: l₂)
Tactic: rcases h with (h | ⟨rfl, h⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : r a b ∨ a = b ∧ Lex r l₁ l₂
refine_1 : ∀ (h : r a b), Lex r (a :: l₁) (b :: l₂)
⊢ Lex r (a :: l₁) (b :: l₂)
have refine_1₁ : ∀ (h : Lex r l₁ l₂), Lex r (a :: l₁) (a :: l₂)
Tactic: rcases h with (h | ⟨rfl, h⟩)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂
have refine_2 : ∀ (h : r a b), r a b ∨ a = b ∧ Lex r l₁ l₂
Tactic: rcases h with (_ | h | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
r : α → α → Prop
inst_1 : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
this : Decidable (Lex r l₁ l₂)
h : Lex r (a :: l₁) (b :: l₂)
refine_2 : ∀ (h : r a b), r a b ∨ a = b ∧ Lex r l₁ l₂
⊢ r a b ∨ a = b ∧ Lex r l₁ l₂
have refine_2₁ : ∀ (h : Lex r l₁ l₂), r a a ∨ a = a ∧ Lex r l₁ l₂
Tactic: rcases h with (_ | h | h)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
h : l₁ ≠ l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
have nil : ∀ {l₂ : List α} (H : length.{u} (α := α) [] ≤ l₂.length) (h : [] ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] l₂
Tactic: induction l₁ generalizing l₂
Cleared hypotheses: l₁, l₂, H, h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
h : l₁ ≠ l₂
nil : ∀ {l₂ : List α} (H : length.{u} (α := α) [] ≤ l₂.length) (h : [] ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
have cons : ∀ (head : α) (tail : List α),
  (∀ {l₂ : List α} (H : tail.length ≤ l₂.length) (h : tail ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) tail l₂) →
    ∀ {l₂ : List α} (H : (head :: tail).length ≤ l₂.length) (h : head :: tail ≠ l₂),
      Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) l₂
Tactic: induction l₁ generalizing l₂
Cleared hypotheses: l₁, l₂, H, h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
l₂ : List α
H : length.{u} (α := α) [] ≤ l₂.length
h : [] ≠ l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] l₂
have nil : ∀ (H : length.{u} (α := α) [] ≤ length.{u} (α := α) []) (h : Ne.{u + 1} (α := List α) [] []),
  Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] []
Tactic: rcases l₂ with - | ⟨b, l₂⟩
Cleared hypotheses: l₂, H, h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
l₂ : List α
H : length.{u} (α := α) [] ≤ l₂.length
h : [] ≠ l₂
nil :
  ∀ (H : length.{u} (α := α) [] ≤ length.{u} (α := α) []) (h : Ne.{u + 1} (α := List α) [] []),
    Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] []
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] l₂
have nil₁ : ∀ (b : α) (l₂ : List α) (H : length.{u} (α := α) [] ≤ (b :: l₂).length) (h : [] ≠ b :: l₂),
  Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) [] (b :: l₂)
Tactic: rcases l₂ with - | ⟨b, l₂⟩
Cleared hypotheses: l₂, H, h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
head : α
tail : List α
tail_ih : ∀ {l₂ : List α} (H : tail.length ≤ l₂.length) (h : tail ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) tail l₂
l₂ : List α
H : (head :: tail).length ≤ l₂.length
h : head :: tail ≠ l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) l₂
have cons : ∀ (H : (head :: tail).length ≤ length.{u} (α := α) []) (h : head :: tail ≠ []),
  Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) []
Tactic: rcases l₂ with - | ⟨b, l₂⟩
Cleared hypotheses: l₂, H, h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
head : α
tail : List α
tail_ih : ∀ {l₂ : List α} (H : tail.length ≤ l₂.length) (h : tail ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) tail l₂
l₂ : List α
H : (head :: tail).length ≤ l₂.length
h : head :: tail ≠ l₂
cons :
  ∀ (H : (head :: tail).length ≤ length.{u} (α := α) []) (h : head :: tail ≠ []),
    Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) []
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) l₂
have cons₁ : ∀ (b : α) (l₂ : List α) (H : (head :: tail).length ≤ (b :: l₂).length) (h : head :: tail ≠ b :: l₂),
  Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (head :: tail) (b :: l₂)
Tactic: rcases l₂ with - | ⟨b, l₂⟩
Cleared hypotheses: l₂, H, h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
have pos : ∀ (ab : a = b), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
Tactic: by_cases ab : a = b
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
pos : ∀ (ab : a = b), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
have neg : ∀ (ab : ¬a = b), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
Tactic: by_cases ab : a = b
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
l₁ : List α
IH : ∀ {l₂ : List α} (H : l₁.length ≤ l₂.length) (h : l₁ ≠ l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) l₁ l₂
b : α
l₂ : List α
H : (a :: l₁).length ≤ (b :: l₂).length
h : a :: l₁ ≠ b :: l₂
ab : a = b
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (b :: l₂)
have pos : ∀ (H : (a :: l₁).length ≤ (a :: l₂).length) (h : a :: l₁ ≠ a :: l₂), Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) (a :: l₁) (a :: l₂)
Tactic: subst b
Cleared hypotheses: b, H, h, ab
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : LT α
l l' : List α
⊢ l.lt l' ↔ Lex (fun (x1 x2 : α) ↦ x1 < x2) l l'
have rw : Lex (fun (x1 x2 : α) ↦ x1 < x2) l l' ↔ Lex (fun (x1 x2 : α) ↦ x1 < x2) l l'
Tactic: rw [List.lt]
-- Lean 4 proof step from Mathlib.Data.List.Lex (hypothesis)
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
h : l' < l
hl' : l' ≠ []
⊢ l'.head! ≤ l.head!
have h₁ : Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l
Tactic: replace h : List.Lex (· < ·) l' l := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l
⊢ l'.head! ≤ l.head!
have pos : ∀ (hl : l = []), l'.head! ≤ l.head!
Tactic: by_cases hl : l = []
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l
pos : ∀ (hl : l = []), l'.head! ≤ l.head!
⊢ l'.head! ≤ l.head!
have neg : ∀ (hl : ¬l = []), l'.head! ≤ l.head!
Tactic: by_cases hl : l = []
-- Lean 4 proof step from Mathlib.Data.List.Lex (hypothesis)
Goal:
α : Type u
inst : Preorder α
inst_1 : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun (x1 x2 : α) ↦ x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!
have h₁ : Lex (fun (x1 x2 : α) ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
Tactic: rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h
Cleared hypotheses: h, hl
-- Lean 4 proof step from Mathlib.Data.List.Lex (goal)
Goal:
α : Type u
inst : LinearOrder α
a : α
l l' : List α
h : l' ≤ l
⊢ a :: l' ≤ a :: l
have rw : ∀ (h : l' < l ∨ l' = l), a :: l' < a :: l ∨ a :: l' = a :: l
Tactic: rw [le_iff_lt_or_eq] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ go f (hd :: tl) acc = acc.toListAppend (lookmap f (hd :: tl))
have cons : (match (motive := Option α → List α) f hd with
  | some b => acc.toListAppend (b :: tl)
  | none => go f tl (acc.push hd)) =
  acc.toListAppend
    (match (motive := Option α → List α) f hd with
    | some b => Array.toListAppend #[] (b :: tl)
    | none => go f tl (Array.push #[] hd))
Tactic: rw [lookmap, go, go]
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match (motive := Option α → List α) none with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match (motive := Option α → List α) none with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))
have cons : acc.toList ++ ([hd] ++ lookmap f tl) = acc.toList ++ ([] ++ ([hd] ++ lookmap f tl))
Tactic: simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match (motive := Option α → List α) f hd with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match (motive := Option α → List α) f hd with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))
have cons : ∀ (x : Option α),
  (match (motive := Option α → List α) x with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match (motive := Option α → List α) x with
      | some b => Array.toListAppend #[] (b :: tl)
      | none => go f tl (Array.push #[] hd))
Tactic: cases f hd with
    | none =>
      simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl
    | some a => rfl
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l : List α
acc : Array α
⊢ go f l acc = acc.toListAppend (lookmap f l)
have nil : go f [] acc = acc.toListAppend (lookmap f [])
Tactic: cases l with
  | nil => simp [go, lookmap]
  | cons hd tl =>
    rw [lookmap, go, go]
    cases f hd with
    | none =>
      simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl
    | some a => rfl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l : List α
acc : Array α
nil : go f [] acc = acc.toListAppend (lookmap f [])
⊢ go f l acc = acc.toListAppend (lookmap f l)
have cons : ∀ (hd : α) (tl : List α), go f (hd :: tl) acc = acc.toListAppend (lookmap f (hd :: tl))
Tactic: cases l with
  | nil => simp [go, lookmap]
  | cons hd tl =>
    rw [lookmap, go, go]
    cases f hd with
    | none =>
      simp only [go_append tl _, Array.toListAppend_eq, append_assoc, Array.toList_push]
      rfl
    | some a => rfl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) = a :: lookmap f l
have simp : (match (motive := Option α → List α) f a with
  | some b => b :: l
  | none => lookmap.go f l (Array.push #[] a)) =
  a :: lookmap.go f l #[]
Tactic: simp only [lookmap, lookmap.go, Array.toListAppend_eq, nil_append]
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match (motive := Option α → List α) f a with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    a :: lookmap.go f l #[]
have rw : (match (motive := Option α → List α) none with
  | some b => b :: l
  | none => (Array.push #[] a).toListAppend (lookmap f l)) =
  a :: lookmap.go f l #[]
Tactic: rw [lookmap.go_append, h]
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
⊢ lookmap f (a :: l) = b :: l
have simp : (match (motive := Option α → List α) f a with
  | some b => b :: l
  | none => lookmap.go f l (Array.push #[] a)) =
  b :: l
Tactic: simp only [lookmap, lookmap.go, Array.toListAppend_eq, nil_append]
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
⊢ (match (motive := Option α → List α) f a with
    | some b => b :: l
    | none => lookmap.go f l (Array.push #[] a)) =
    b :: l
have rw : (match (motive := Option α → List α) some b with
  | some b => b :: l
  | none => lookmap.go f l (Array.push #[] a)) =
  b :: l
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
⊢ lookmap f (a :: l) =
    match (motive := Option α → List α) f a with
    | none => a :: lookmap f l
    | some b => b :: l
have none : ∀ (h : f a = none),
  lookmap f (a :: l) =
    match (motive := Option α → List α) none with
    | none => a :: lookmap f l
    | some b => b :: l
Tactic: cases h : f a
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
a : α
l : List α
none :
  ∀ (h : f a = Option.none),
    lookmap f (a :: l) =
      match (motive := Option α → List α) Option.none with
      | Option.none => a :: lookmap f l
      | some b => b :: l
⊢ lookmap f (a :: l) =
    match (motive := Option α → List α) f a with
    | Option.none => a :: lookmap f l
    | some b => b :: l
have some : ∀ (val : α) (h : f a = some val),
  lookmap f (a :: l) =
    match (motive := Option α → List α) some val with
    | Option.none => a :: lookmap f l
    | some b => b :: l
Tactic: cases h : f a
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (hypothesis)
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
⊢ lookmap f (a :: l) = lookmap g (a :: l)
have H₁ : f a = g a
Tactic: obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (hypothesis)
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
⊢ lookmap f (a :: l) = lookmap g (a :: l)
have H₂ : ∀ (x : α), x ∈ l → f x = g x
Tactic: obtain ⟨H₁, H₂⟩ := forall_mem_cons.1 H
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
⊢ lookmap f (a :: l) = lookmap g (a :: l)
have none : ∀ (h : g a = none), lookmap f (a :: l) = lookmap g (a :: l)
Tactic: rcases h : g a with - | b
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
H₁ : f a = g a
H₂ : ∀ (x : α), x ∈ l → f x = g x
none : ∀ (h : g a = Option.none), lookmap f (a :: l) = lookmap g (a :: l)
⊢ lookmap f (a :: l) = lookmap g (a :: l)
have some : ∀ (b : α) (h : g a = some b), lookmap f (a :: l) = lookmap g (a :: l)
Tactic: rcases h : g a with - | b
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
⊢ map g (lookmap f (a :: l)) = map g (a :: l)
have none : ∀ (h' : f a = none), map g (lookmap f (a :: l)) = map g (a :: l)
Tactic: rcases h' : f a with - | b
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
none : ∀ (h' : f a = Option.none), map g (lookmap f (a :: l)) = map g (a :: l)
⊢ map g (lookmap f (a :: l)) = map g (a :: l)
have some : ∀ (b : α) (h' : f a = some b), map g (lookmap f (a :: l)) = map g (a :: l)
Tactic: rcases h' : f a with - | b
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ lookmap f l = l
have h₁ : ∀ (a b : α), b ∈ f a → id a = id b
Tactic: rw [← map_id (l.lookmap f), lookmap_map_eq, map_id]
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l : List α
⊢ (lookmap f l).length = l.length
have h : ∀ (a b : α), b ∈ f a → () = ()
Tactic: rw [← length_map, lookmap_map_eq _ fun _ => (), length_map]
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a : α
l₁_1 l₂_1 : List α
p : l₁_1 ~ l₂_1
IH :
  ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁_1),
    lookmap f l₁_1 ~ lookmap f l₂_1
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁_1)
⊢ lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)
have cons : ∀ (h : f a = none), lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)
Tactic: cases h : f a
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a : α
l₁_1 l₂_1 : List α
p : l₁_1 ~ l₂_1
IH :
  ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁_1),
    lookmap f l₁_1 ~ lookmap f l₂_1
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁_1)
cons : ∀ (h : f a = none), lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)
⊢ lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)
have cons₁ : ∀ (val : α) (h : f a = some val), lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)
Tactic: cases h : f a
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
have swap : ∀ (h₁ : f a = none), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Tactic: rcases h₁ : f a with - | c
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
swap : ∀ (h₁ : f a = none), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
have swap₁ : ∀ (c : α) (h₁ : f a = some c), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Tactic: rcases h₁ : f a with - | c
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
have swap : ∀ (h₂ : f b = none), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Tactic: rcases h₂ : f b with - | d
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
swap : ∀ (h₂ : f b = none), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
have swap₁ : ∀ (d : α) (h₂ : f b = some d), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Tactic: rcases h₂ : f b with - | d
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
have swap : ∀ (h₂ : f b = none), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Tactic: rcases h₂ : f b with - | d
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
swap : ∀ (h₂ : f b = none), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
have swap₁ : ∀ (d : α) (h₂ : f b = some d), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Tactic: rcases h₂ : f b with - | d
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
have swap : ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: b :: l))
  (h₁ : f b = some d), lookmap f (b :: b :: l) ~ lookmap f (b :: b :: l)
Tactic: rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩
Cleared hypotheses: a, H, c, h₁
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ l₁_1 l₂_1 l₃ : List α
p₁ : l₁_1 ~ l₂_1
h : l₂_1 ~ l₃
IH₁ :
  ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁_1),
    lookmap f l₁_1 ~ lookmap f l₂_1
IH₂ :
  ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₂_1),
    lookmap f l₂_1 ~ lookmap f l₃
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁_1
⊢ lookmap f l₁_1 ~ lookmap f l₃
have trans : ∀ {x y : α},
  (∀ (c : α), c ∈ f x → ∀ (d : α), d ∈ f y → x = y ∧ c = d) → ∀ (c : α), c ∈ f y → ∀ (d : α), d ∈ f x → y = x ∧ c = d
Tactic: refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))