awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a <+ g a
nil : ∀ (h : ∀ (a : α), Membership.mem (γ := List α) [] a → f a <+ g a), flatMap f [] <+ flatMap g []
⊢ flatMap f l <+ flatMap g l
have cons : ∀ (head : α) (tail : List α),
  (∀ (h : ∀ (a : α), a ∈ tail → f a <+ g a), flatMap f tail <+ flatMap g tail) →
    ∀ (h : ∀ (a : α), a ∈ head :: tail → f a <+ g a), flatMap f (head :: tail) <+ flatMap g (head :: tail)
Tactic: induction l with grind
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
L : List α
i : Nat
h : i < L.length
⊢ drop i (take (i + 1) L) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) L i h]
have nil : ∀ (i : Nat) (h : i < length.{u_1} (α := α) []),
  drop i (take (i + 1) []) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] i h]
Tactic: induction L generalizing i with grind
Cleared hypotheses: L, i, h
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
L : List α
i : Nat
h : i < L.length
nil :
  ∀ (i : Nat) (h : i < length.{u_1} (α := α) []),
    drop i (take (i + 1) []) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] i h]
⊢ drop i (take (i + 1) L) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) L i h]
have cons : ∀ (head : α) (tail : List α),
  (∀ (i : Nat) (h : i < tail.length),
      drop i (take (i + 1) tail) = [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i h]) →
    ∀ (i : Nat) (h : i < (head :: tail).length),
      drop i (take (i + 1) (head :: tail)) =
        [getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) i h]
Tactic: induction L generalizing i with grind
Cleared hypotheses: L, i, h
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
L : List (List α)
x : List α
⊢ x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) L) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) L) ++ x
have nil : x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) []) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) []) ++ x
Tactic: induction L with grind
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
L : List (List α)
x : List α
nil : x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) []) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) []) ++ x
⊢ x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) L) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) L) ++ x
have cons : ∀ (head : List α) (tail : List (List α)),
  x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) tail) = flatten (map (fun (x_1 : List α) ↦ x ++ x_1) tail) ++ x →
    x ++ flatten (map (fun (x_1 : List α) ↦ x_1 ++ x) (head :: tail)) =
      flatten (map (fun (x_1 : List α) ↦ x ++ x_1) (head :: tail)) ++ x
Tactic: induction L with grind
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.head hl ≠ []
⊢ (l.head hl).head hl' = l.flatten.head ⋯
have nil : ∀ (hl : Ne.{u_1 + 1} (α := List (List α)) [] []) (hl' : head [] hl ≠ []), (head [] hl).head hl' = head (flatten []) sorry
Tactic: cases l with grind
Cleared hypotheses: l, hl, hl'
-- Lean 4 proof step from Mathlib.Data.List.Flatten (goal)
Goal:
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.head hl ≠ []
nil :
  ∀ (hl : Ne.{u_1 + 1} (α := List (List α)) [] []) (hl' : head [] hl ≠ []), (head [] hl).head hl' = head (flatten []) ⋯
⊢ (l.head hl).head hl' = l.flatten.head ⋯
have cons : ∀ (head : List α) (tail : List (List α)) (hl : head :: tail ≠ []) (hl' : (head :: tail).head hl ≠ []),
  ((head :: tail).head hl).head hl' = (head :: tail).flatten.head sorry
Tactic: cases l with grind
Cleared hypotheses: l, hl, hl'
-- Lean 4 proof step from Mathlib.Data.List.Flatten (hypothesis)
Goal:
α : Type u_1
l : List (List α)
hl : l ≠ []
hl' : l.getLast hl ≠ []
⊢ (l.getLast hl).getLast hl' = l.flatten.getLast ⋯
have x : l = [] ∨ ∃ (l' : List (List α)), ∃ (b : List α), l = l'.concat b
Tactic: cases eq_nil_or_concat l with grind
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂
have nil : Forall₂ S [] []
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
nil : Forall₂ S [] []
⊢ Forall₂ S l₁ l₂
have cons : ∀ {a : α} {b : β} {l₁ : List α} {l₂ : List β}, R a b → Forall₂ R l₁ l₂ → Forall₂ S l₁ l₂ → Forall₂ S (a :: l₁) (b :: l₂)
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a : α
b : β
l₁_1 : List α
l₂_1 : List β
h : R a b
h_1 : Forall₂ R l₁_1 l₂_1
a_ih : Forall₂ S l₁_1 l₂_1
⊢ Forall₂ S (a :: l₁_1) (b :: l₂_1)
have cons : S a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α → List α → Prop) (Forall₂ fun (x1 x2 : α) ↦ x1 = x2) Eq
have h : ∀ (a b : List α), Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b = (a = b)
Tactic: funext a b
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
a b : List α
⊢ Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b = (a = b)
have h : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b ↔ a = b
Tactic: apply propext
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
a b : List α
⊢ Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b ↔ a = b
have h : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b → a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
a b : List α
h : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b → a = b
⊢ Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b ↔ a = b
have h₁ : a = b → Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
a b : List α
h : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b
⊢ a = b
have h₁ : Eq.{u_1 + 1} (α := List α) [] []
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
a b : List α
h : Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) a b
h₁ : Eq.{u_1 + 1} (α := List α) [] []
⊢ a = b
have h₂ : ∀ {a b : α} {l₁ l₂ : List α}, a = b → Forall₂ (fun (x1 x2 : α) ↦ x1 = x2) l₁ l₂ → l₁ = l₂ → a :: l₁ = b :: l₂
Tactic: induction h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List β
H : Forall₂ R [] l
⊢ l = []
have nil : Eq.{u_2 + 1} (α := List β) [] []
Tactic: cases H
Cleared hypotheses: l, H
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
H : Forall₂ R l []
⊢ l = []
have nil : Eq.{u_1 + 1} (α := List α) [] []
Tactic: cases H
Cleared hypotheses: l, H
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Prop
a : α
l : List α
u : List β
⊢ Forall₂ (fun (a : α) (b : β) ↦ p a ∧ R a b) (a :: l) u ↔ (∀ (a_1 : α), a_1 ∈ a :: l → p a_1) ∧ Forall₂ R (a :: l) u
have simp : (p a ∧ ∃ (x : β), R a x ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ (x_1 : List β), Forall₂ R l x_1 ∧ u = x :: x_1) ↔
  p a ∧ (∀ (a : α), a ∈ l → p a) ∧ ∃ (b : β), R a b ∧ ∃ (x : List β), Forall₂ R l x ∧ u = b :: x
Tactic: simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc,
      exists_and_left]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
b : β
l₁ : List α
l₂ : List β
h₁ : R a b
h₂ : Forall₂ R l₁ l₂
x : α
y : β
hx : (x, y) ∈ (a :: l₁).zip (b :: l₂)
⊢ R x y
have hx₁ : (x, y) = (a, b) ∨ (x, y) ∈ zipWith Prod.mk l₁ l₂
Tactic: rw [zip, zipWith, mem_cons] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length ∧ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
⊢ Forall₂ R l₁ l₂
have h₁ : l₁.length = l₂.length
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : l₁.length = l₂.length ∧ ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
h₁ : l₁.length = l₂.length
⊢ Forall₂ R l₁ l₂
have h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
Tactic: obtain ⟨h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ : List β
h₁ : length.{u_1} (α := α) [] = l₂.length
h₂ : ∀ {a : α} {b : β}, Membership.mem (γ := List (α × β)) (zip [] l₂) (a, b) → R a b
⊢ Forall₂ R [] l₂
have nil : ∀ (h₁ : length.{u_1} (α := α) [] = length.{u_2} (α := β) [])
  (h₂ : ∀ {a : α} {b : β}, Membership.mem (γ := List (α × β)) (zip [] []) (a, b) → R a b), Forall₂ R [] []
Tactic: cases length_eq_zero_iff.1 h₁.symm
Cleared hypotheses: l₂, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
l₂ : List β
h₁ : (a :: l₁).length = l₂.length
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ (a :: l₁).zip l₂ → R a_1 b
⊢ Forall₂ R (a :: l₁) l₂
have cons : ∀ (h₁ : (a :: l₁).length = length.{u_2} (α := β) [])
  (h₂ : ∀ {a_1 : α} {b : β}, Membership.mem (γ := List (α × β)) ((a :: l₁).zip []) (a_1, b) → R a_1 b),
  Forall₂ R (a :: l₁) []
Tactic: rcases l₂ with - | ⟨b, l₂⟩
Cleared hypotheses: l₂, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
l₂ : List β
h₁ : (a :: l₁).length = l₂.length
h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ (a :: l₁).zip l₂ → R a_1 b
cons :
  ∀ (h₁ : (a :: l₁).length = length.{u_2} (α := β) [])
    (h₂ : ∀ {a_1 : α} {b : β}, Membership.mem (γ := List (α × β)) ((a :: l₁).zip []) (a_1, b) → R a_1 b),
    Forall₂ R (a :: l₁) []
⊢ Forall₂ R (a :: l₁) l₂
have cons₁ : ∀ (b : β) (l₂ : List β) (h₁ : (a :: l₁).length = (b :: l₂).length)
  (h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1), Forall₂ R (a :: l₁) (b :: l₂)
Tactic: rcases l₂ with - | ⟨b, l₂⟩
Cleared hypotheses: l₂, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₁ : (a :: l₁).length = (b :: l₂).length
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
⊢ Forall₂ R (a :: l₁) (b :: l₂)
have h₃ : l₁.length = l₂.length
Tactic: simp only [length_cons, succ.injEq] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_2 : α} {b_2 : β}, (a_2, b_2) ∈ (a :: l₁).zip (b :: l₂) → R a_2 b_2
h₁ : l₁.length = l₂.length
a_1 : α
b_1 : β
h : (a_1, b_1) ∈ l₁.zip l₂
⊢ (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂)
have simp : a_1 = a ∧ b_1 = b ∨ (a_1, b_1) ∈ zipWith Prod.mk l₁ l₂
Tactic: simp only [zip, zipWith, mem_cons, Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_2 : α} {b_2 : β}, (a_2, b_2) ∈ (a :: l₁).zip (b :: l₂) → R a_2 b_2
h₁ : l₁.length = l₂.length
a_1 : α
b_1 : β
h : (a_1, b_1) ∈ l₁.zip l₂
⊢ a_1 = a ∧ b_1 = b ∨ (a_1, b_1) ∈ zipWith Prod.mk l₁ l₂
have h₃ : (a_1, b_1) ∈ zipWith Prod.mk l₁ l₂
Tactic: right
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h₁ : l₁.length = l₂.length
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
⊢ Forall₂ R l₁ l₂
have nil : ∀ {l₂ : List β} (h₁ : length.{u_1} (α := α) [] = l₂.length)
  (h₂ : ∀ {a : α} {b : β}, Membership.mem (γ := List (α × β)) (zip [] l₂) (a, b) → R a b), Forall₂ R [] l₂
Tactic: induction l₁ generalizing l₂ with
    | nil =>
      cases length_eq_zero_iff.1 h₁.symm
      constructor
    | cons a l₁ IH =>
      rcases l₂ with - | ⟨b, l₂⟩
      · simp at h₁
      · simp only [length_cons, succ.injEq] at h₁
        exact Forall₂.cons (h₂ <| by simp [zip])
          (IH h₁ fun h => h₂ <| by
            simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)
Cleared hypotheses: l₁, l₂, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h₁ : l₁.length = l₂.length
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b
nil :
  ∀ {l₂ : List β} (h₁ : length.{u_1} (α := α) [] = l₂.length)
    (h₂ : ∀ {a : α} {b : β}, Membership.mem (γ := List (α × β)) (zip [] l₂) (a, b) → R a b), Forall₂ R [] l₂
⊢ Forall₂ R l₁ l₂
have cons : ∀ (a : α) (l₁ : List α)
  (IH :
    ∀ {l₂ : List β} (h₁ : l₁.length = l₂.length) (h₂ : ∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b), Forall₂ R l₁ l₂)
  {l₂ : List β} (h₁ : (a :: l₁).length = l₂.length) (h₂ : ∀ {a_1 : α} {b : β}, (a_1, b) ∈ (a :: l₁).zip l₂ → R a_1 b),
  Forall₂ R (a :: l₁) l₂
Tactic: induction l₁ generalizing l₂ with
    | nil =>
      cases length_eq_zero_iff.1 h₁.symm
      constructor
    | cons a l₁ IH =>
      rcases l₂ with - | ⟨b, l₂⟩
      · simp at h₁
      · simp only [length_cons, succ.injEq] at h₁
        exact Forall₂.cons (h₂ <| by simp [zip])
          (IH h₁ fun h => h₂ <| by
            simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h)
Cleared hypotheses: l₁, l₂, h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (take l₁.length l) l₁
have h' : Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))
Tactic: have h' : Forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)) :=
    forall₂_take (length l₁) h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (take l₁.length l) l₁
have rwa : ∀ (h' : Forall₂ R (take l₁.length l) l₁), Forall₂ R (take l₁.length l) l₁
Tactic: rwa [take_left] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (drop l₁.length l) l₂
have h' : Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))
Tactic: have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) :=
    forall₂_drop (length l₁) h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (drop l₁.length l) l₂
have rwa : ∀ (h' : Forall₂ R (drop l₁.length l) l₂), Forall₂ R (drop l₁.length l) l₂
Tactic: rwa [drop_left] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ (fun (x1 : α) (x2 : List α) ↦ x1 ∈ x2) a (a' :: as) ↔ (fun (x1 : β) (x2 : List β) ↦ x1 ∈ x2) b (b' :: bs)
have simp : a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs
Tactic: simp only [mem_cons]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
b : β
l₁ : List α
l₂ : List β
h₁ : R a b
h₂ : Forall₂ R l₁ l₂
⊢ Forall₂ R (a :: l₁).reverse (b :: l₂).reverse
have simp : Forall₂ R (l₁.reverse ++ [a]) (l₂.reverse ++ [b])
Tactic: simp only [reverse_cons]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁ l₂
have rw : Forall₂ R l₁.reverse.reverse l₂.reverse.reverse
Tactic: rw [← reverse_reverse l₁, ← reverse_reverse l₂]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
have pos : ∀ (h : p a = true), Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
pos : ∀ (h : p a = true), Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
have neg : ∀ (h : ¬p a = true), Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
Tactic: by_cases h : p a
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
have this : q b = true
Tactic: have : q b := by rwa [← hpq h₁]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))
have this : ¬q b = true
Tactic: have : ¬q b := by rwa [← hpq h₁]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))
have rw : Forall₂ P
  (match (motive := Option γ → List γ) f a with
  | none => filterMap f as
  | some b => b :: filterMap f as)
  (match (motive := Option δ → List δ) g b with
  | none => filterMap g bs
  | some b => b :: filterMap g bs)
Tactic: rw [filterMap_cons, filterMap_cons]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
have mp : SublistForall₂ R l₁ l₂ → ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
mp : SublistForall₂ R l₁ l₂ → ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
have mpr : (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂) → SublistForall₂ R l₁ l₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : α
b : β
l1 : List α
l2 : List β
rab : R a b
h : SublistForall₂ R l1 l2
ih : ∃ (l : List β), Forall₂ R l1 l ∧ l <+ l2
⊢ ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2
have mp : ∀ (l : List β) (hl1 : Forall₂ R l1 l) (hl2 : l <+ l2), ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2
Tactic: obtain ⟨l, hl1, hl2⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
a : β
l₁_1 : List α
l₂_1 : List β
h : SublistForall₂ R l₁_1 l₂_1
ih : ∃ (l : List β), Forall₂ R l₁_1 l ∧ l <+ l₂_1
⊢ ∃ (l : List β), Forall₂ R l₁_1 l ∧ l <+ a :: l₂_1
have mp : ∀ (l : List β) (hl1 : Forall₂ R l₁_1 l) (hl2 : l <+ l₂_1), ∃ (l : List β), Forall₂ R l₁_1 l ∧ l <+ a :: l₂_1
Tactic: obtain ⟨l, hl1, hl2⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
⊢ ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
have mp : ∀ {l : List β}, ∃ (l_1 : List β), Forall₂ R [] l_1 ∧ l_1 <+ l
Tactic: induction h with
    | nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
    | @cons a b l1 l2 rab _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
    | cons_right _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
mp : ∀ {l : List β}, ∃ (l_1 : List β), Forall₂ R [] l_1 ∧ l_1 <+ l
⊢ ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
have mp₁ : ∀ {a : α} {b : β} {l1 : List α} {l2 : List β} (rab : R a b),
  SublistForall₂ R l1 l2 →
    ∀ (ih : ∃ (l : List β), Forall₂ R l1 l ∧ l <+ l2), ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2
Tactic: induction h with
    | nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
    | @cons a b l1 l2 rab _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
    | cons_right _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : SublistForall₂ R l₁ l₂
mp : ∀ {l : List β}, ∃ (l_1 : List β), Forall₂ R [] l_1 ∧ l_1 <+ l
mp₁ :
  ∀ {a : α} {b : β} {l1 : List α} {l2 : List β} (rab : R a b),
    SublistForall₂ R l1 l2 →
      ∀ (ih : ∃ (l : List β), Forall₂ R l1 l ∧ l <+ l2), ∃ (l : List β), Forall₂ R (a :: l1) l ∧ l <+ b :: l2
⊢ ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
have mp₂ : ∀ {a : β} {l₁ : List α} {l₂ : List β},
  SublistForall₂ R l₁ l₂ →
    ∀ (ih : ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂), ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ a :: l₂
Tactic: induction h with
    | nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
    | @cons a b l1 l2 rab _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
    | cons_right _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ l₂
⊢ SublistForall₂ R l₁ l₂
have mpr : ∀ (l : List β) (hl1 : Forall₂ R l₁ l) (hl2 : l <+ l₂), SublistForall₂ R l₁ l₂
Tactic: obtain ⟨l, hl1, hl2⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ l : List β
hl1 : Forall₂ R l₁ l
hl2 : l <+ l₂
⊢ SublistForall₂ R l₁ l₂
have mpr : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l), SublistForall₂ R l₁ l₂
Tactic: revert l₁
Cleared hypotheses: l₁, hl1
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R l₁ []
have mpr : SublistForall₂ R [] []
Tactic: rw [forall₂_nil_right_iff.1 hl1]