awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Lookmap
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)
cons₁ : ∀ (val : α) (h : f a = some val), lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)
⊢ lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)

Tactic:
cases h : f a
-- Module: Mathlib.Data.List.Lookmap
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)
h : f a = none
⊢ lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)

Tactic:
simpa [h] using IH (pairwise_cons.1 H).2

Premises used: List.pairwise_cons, And.right, Iff.mp
-- Module: Mathlib.Data.List.Lookmap
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)
val : α
h : f a = some val
⊢ lookmap f (a :: l₁_1) ~ lookmap f (a :: l₂_1)

Tactic:
simp [lookmap_cons_some _ _ h, p]

Premises used: List.lookmap_cons_some
-- Module: Mathlib.Data.List.Lookmap
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)
swap₁ : ∀ (c : α) (h₁ : f a = some c), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases h₁ : f a with - | c
-- Module: Mathlib.Data.List.Lookmap
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)
swap₁ : ∀ (d : α) (h₂ : f b = some d), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases h₂ : f b with - | d
-- Module: Mathlib.Data.List.Lookmap
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)
swap₁ : ∀ (d : α) (h₂ : f b = some d), lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases h₂ : f b with - | d
-- Module: Mathlib.Data.List.Lookmap
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
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
simpa [h₁, h₂] using swap _ _ _

Premises used: List.Perm.swap
-- Module: Mathlib.Data.List.Lookmap
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
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
simpa [h₁, lookmap_cons_some _ _ h₂] using swap _ _ _

Premises used: List.Perm.swap, List.lookmap_cons_some
-- Module: Mathlib.Data.List.Lookmap
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
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
simpa [lookmap_cons_some _ _ h₁, h₂] using swap _ _ _

Premises used: List.Perm.swap, List.lookmap_cons_some
-- Module: Mathlib.Data.List.Lookmap
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
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)
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩

Premises used: Iff.mpr, List.pairwise_cons, And.left, Iff.mp, Or.inl, List.mem_cons, rfl
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
b : α
l : List α
d : α
h₂ : f b = some d
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:
Perm.refl _

Premises used: List.Perm.refl
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
b : α
l : List α
d : α
h₂ : f b = some d
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:
exact Perm.refl _

Premises used: List.Perm.refl
-- Module: Mathlib.Data.List.Lookmap
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₃

Tactic:
(IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))

Premises used: List.Perm.pairwise_iff, List.Perm.trans, Iff.mp
-- Module: Mathlib.Data.List.Lookmap
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
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
⊢ lookmap f l₁_1 ~ lookmap f l₃

Tactic:
refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))

Premises used: List.Perm.pairwise_iff, List.Perm.trans, Iff.mp
-- Module: Mathlib.Data.List.Lookmap
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
⊢ ∀ {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:
grind
-- Module: Mathlib.Data.List.Lookmap
Goal:
α : Type u_1
f : α → Option α
l₁ l₂ : List α
H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁
p : l₁ ~ l₂
nil :
  ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) []),
    lookmap f [] ~ lookmap f []
cons :
  ∀ (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂)
    (IH :
      ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁),
        lookmap f l₁ ~ lookmap f l₂)
    (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁)),
    lookmap f (a :: l₁) ~ lookmap f (a :: l₂)
swap :
  ∀ (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)
trans :
  ∀ {l₁ l₂ l₃ : List α} (p₁ : l₁ ~ l₂),
    l₂ ~ l₃ →
      ∀
        (IH₁ :
          ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁),
            lookmap f l₁ ~ lookmap f l₂)
        (IH₂ :
          ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₂),
            lookmap f l₂ ~ lookmap f l₃)
        (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁),
        lookmap f l₁ ~ lookmap f l₃
⊢ lookmap f l₁ ~ lookmap f l₂

Tactic:
induction p with
  | nil => simp
  | cons a p IH =>
    cases h : f a
    · simpa [h] using IH (pairwise_cons.1 H).2
    · simp [lookmap_cons_some _ _ h, p]
  | swap a b l =>
    rcases h₁ : f a with - | c <;> rcases h₂ : f b with - | d
    · simpa [h₁, h₂] using swap _ _ _
    · simpa [h₁, lookmap_cons_some _ _ h₂] using swap _ _ _
    · simpa [lookmap_cons_some _ _ h₁, h₂] using swap _ _ _
    · rcases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) _ h₂ _ h₁ with ⟨rfl, rfl⟩
      exact Perm.refl _
  | trans p₁ _ IH₁ IH₂ =>
    refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
    grind

Premises used: List.Perm.refl, List.Perm.swap, List.Perm.trans, List.cons, rfl, List.nil
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
nil : map₂Left' f [] [] = (map (fun (a : α) ↦ f a none) [], [])
cons : ∀ (head : α) (tail : List α), map₂Left' f (head :: tail) [] = (map (fun (a : α) ↦ f a none) (head :: tail), [])
⊢ map₂Left' f as [] = (map (fun (a : α) ↦ f a none) as, [])

Tactic:
cases as
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
⊢ map₂Left' f [] [] = (map (fun (a : α) ↦ f a none) [], [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head : α
tail : List α
⊢ map₂Left' f (head :: tail) [] = (map (fun (a : α) ↦ f a none) (head :: tail), [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
nil : map₂Right' f [] [] = (map (f none) [], [])
cons : ∀ (head : β) (tail : List β), map₂Right' f [] (head :: tail) = (map (f none) (head :: tail), [])
⊢ map₂Right' f [] bs = (map (f none) bs, [])

Tactic:
cases bs
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
⊢ map₂Right' f [] [] = (map (f none) [], [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head : β
tail : List β
⊢ map₂Right' f [] (head :: tail) = (map (f none) (head :: tail), [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
⊢ map₂Right' f as [] = ([], as)

Tactic:
rfl

Premises used: List.map₂Left', List.map₂Right', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
b : β
bs : List β
⊢ map₂Right' f [] (b :: bs) = (f none b :: map (f none) bs, [])

Tactic:
rfl

Premises used: List.map₂Left', List.map, List.map₂Right', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ map₂Right' f (a :: as) (b :: bs) =
    let r := map₂Right' f as bs;
    (f (some a) b :: r.fst, r.snd)

Tactic:
rfl

Premises used: List.map₂Left', List.map₂Right', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List β
nil : zipWith f [] [] = []
cons : ∀ (head : β) (tail : List β), zipWith f [] (head :: tail) = []
⊢ zipWith f [] l = []

Tactic:
cases l
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
⊢ zipWith f [] [] = []

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head : β
tail : List β
⊢ zipWith f [] (head :: tail) = []

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List α
nil : zipWith f [] [] = []
cons : ∀ (head : α) (tail : List α), zipWith f (head :: tail) [] = []
⊢ zipWith f l [] = []

Tactic:
cases l
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
head : α
tail : List α
⊢ zipWith f (head :: tail) [] = []

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
simp! : flip f b a = f a b
⊢ zipWith (flip f) (b :: bs) (a :: as) = zipWith f (a :: as) (b :: bs)

Tactic:
simp! [zipWith_flip]
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ flip f b a = f a b

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
as : List α
nil : Eq (α := List (Prod.{u, v} α (Option β)) × List β) (zipLeft' [] []) (map (fun (a : α) ↦ (a, none)) [], [])
cons :
  ∀ (head : α) (tail : List α),
    Eq (α := List (Prod.{u, v} α (Option β)) × List β) ((head :: tail).zipLeft' [])
      (map (fun (a : α) ↦ (a, none)) (head :: tail), [])
⊢ Eq (α := List (Prod.{u, v} α (Option β)) × List β) (as.zipLeft' []) (map (fun (a : α) ↦ (a, none)) as, [])

Tactic:
cases as
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
⊢ Eq (α := List (Prod.{u, v} α (Option β)) × List β) (zipLeft' [] []) (map (fun (a : α) ↦ (a, none)) [], [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
tail : List α
⊢ Eq (α := List (Prod.{u, v} α (Option β)) × List β) ((head :: tail).zipLeft' [])
    (map (fun (a : α) ↦ (a, none)) (head :: tail), [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
bs : List β
⊢ Eq (α := List (Prod.{u, v} α (Option β)) × List β) (zipLeft' [] bs) ([], bs)

Tactic:
rfl

Premises used: List.zipWithLeft', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
a : α
as : List α
⊢ Eq (α := List (Prod.{u, v} α (Option β)) × List β) ((a :: as).zipLeft' [])
    ((a, none) :: map (fun (a : α) ↦ (a, none)) as, [])

Tactic:
rfl

Premises used: List.map, List.zipWithLeft', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
a : α
as : List α
b : β
bs : List β
⊢ (a :: as).zipLeft' (b :: bs) =
    let r := as.zipLeft' bs;
    ((a, some b) :: r.fst, r.snd)

Tactic:
rfl

Premises used: List.zipWithLeft', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
bs : List β
nil : Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] []) (map (fun (b : β) ↦ (none, b)) [], [])
cons :
  ∀ (head : β) (tail : List β),
    Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] (head :: tail))
      (map (fun (b : β) ↦ (none, b)) (head :: tail), [])
⊢ Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] bs) (map (fun (b : β) ↦ (none, b)) bs, [])

Tactic:
cases bs
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
⊢ Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] []) (map (fun (b : β) ↦ (none, b)) [], [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : β
tail : List β
⊢ Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] (head :: tail))
    (map (fun (b : β) ↦ (none, b)) (head :: tail), [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
as : List α
⊢ Eq (α := List (Prod.{u, v} (Option α) β) × List α) (as.zipRight' []) ([], as)

Tactic:
rfl

Premises used: List.zipWithLeft', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
b : β
bs : List β
⊢ Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] (b :: bs))
    ((none, b) :: map (fun (b : β) ↦ (none, b)) bs, [])

Tactic:
rfl

Premises used: List.map, List.zipWithLeft', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
a : α
as : List α
b : β
bs : List β
⊢ (a :: as).zipRight' (b :: bs) =
    let r := as.zipRight' bs;
    ((some a, b) :: r.fst, r.snd)

Tactic:
rfl

Premises used: List.zipWithLeft', rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
nil : map₂Left f [] [] = map (fun (a : α) ↦ f a none) []
cons : ∀ (head : α) (tail : List α), map₂Left f (head :: tail) [] = map (fun (a : α) ↦ f a none) (head :: tail)
⊢ map₂Left f as [] = map (fun (a : α) ↦ f a none) as

Tactic:
cases as
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
⊢ map₂Left f [] [] = map (fun (a : α) ↦ f a none) []

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head : α
tail : List α
⊢ map₂Left f (head :: tail) [] = map (fun (a : α) ↦ f a none) (head :: tail)

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x : List β
⊢ map₂Left f [] x = (map₂Left' f [] x).fst

Tactic:
simp
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
⊢ map₂Left f (a :: as) [] = (map₂Left' f (a :: as) []).fst

Tactic:
simp
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
⊢ map₂Left f (a :: as) (b :: bs) = (map₂Left' f (a :: as) (b :: bs)).fst

Tactic:
simp [map₂Left_eq_map₂Left']
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
h : length.{u} (α := α) [] ≤ length.{v} (α := β) []
⊢ map₂Left f [] [] = zipWith (fun (a : α) (b : β) ↦ f a (some b)) [] []

Tactic:
simp
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head : β
tail : List β
h : length.{u} (α := α) [] ≤ (head :: tail).length
⊢ map₂Left f [] (head :: tail) = zipWith (fun (a : α) (b : β) ↦ f a (some b)) [] (head :: tail)

Tactic:
simp
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
h : (a :: as).length ≤ length.{v} (α := β) []
⊢ map₂Left f (a :: as) [] = zipWith (fun (a : α) (b : β) ↦ f a (some b)) (a :: as) []

Tactic:
simp at h
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : (a :: as).length ≤ (b :: bs).length
⊢ as.length ≤ bs.length

Tactic:
simp only [length_cons, succ_le_succ_iff] at h

Premises used: List.length_cons, Nat.succ_le_succ_iff
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : as.length ≤ bs.length
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun (a : α) (b : β) ↦ f a (some b)) (a :: as) (b :: bs)

Tactic:
simp [h, map₂Left_eq_zipWith]
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
nil : map₂Right f [] [] = map (f none) []
cons : ∀ (head : β) (tail : List β), map₂Right f [] (head :: tail) = map (f none) (head :: tail)
⊢ map₂Right f [] bs = map (f none) bs

Tactic:
cases bs
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
⊢ map₂Right f [] [] = map (f none) []

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
head : β
tail : List β
⊢ map₂Right f [] (head :: tail) = map (f none) (head :: tail)

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
⊢ map₂Right f as [] = []

Tactic:
rfl

Premises used: List.map₂Left, List.map₂Right, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
b : β
bs : List β
⊢ map₂Right f [] (b :: bs) = f none b :: map (f none) bs

Tactic:
rfl

Premises used: List.map, List.map₂Left, List.map₂Right, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ map₂Right f (a :: as) (b :: bs) = f (some a) b :: map₂Right f as bs

Tactic:
rfl

Premises used: List.map₂Left, List.map₂Right, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
⊢ map₂Right f as bs = (map₂Right' f as bs).fst

Tactic:
simp only [map₂Right, map₂Right', map₂Left_eq_map₂Left']

Premises used: List.map₂Left_eq_map₂Left', List.map₂Right', List.map₂Right
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
h : bs.length ≤ as.length
⊢ Eq (α := (a : β) → (b : α) → γ) (fun (a : β) (b : α) ↦ flip f a (some b)) (flip fun (a : α) (b : β) ↦ f (some a) b)

Tactic:
have : (fun a b => flip f a (some b)) = flip fun a b => f (some a) b := rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
h : bs.length ≤ as.length
this :
  Eq (α := (a : β) → (b : α) → γ) (fun (a : β) (b : α) ↦ flip f a (some b)) (flip fun (a : α) (b : β) ↦ f (some a) b)
⊢ map₂Right f as bs = zipWith (fun (a : α) (b : β) ↦ f (some a) b) as bs

Tactic:
simp only [map₂Right, map₂Left_eq_zipWith, zipWith_flip, *]

Premises used: List.zipWith_flip, List.map₂Right, List.map₂Left_eq_zipWith
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
as : List α
nil : Eq (α := List (Prod.{u, v} α (Option β))) (zipLeft [] []) (map (fun (a : α) ↦ (a, none)) [])
cons :
  ∀ (head : α) (tail : List α),
    Eq (α := List (Prod.{u, v} α (Option β))) ((head :: tail).zipLeft []) (map (fun (a : α) ↦ (a, none)) (head :: tail))
⊢ Eq (α := List (Prod.{u, v} α (Option β))) (as.zipLeft []) (map (fun (a : α) ↦ (a, none)) as)

Tactic:
cases as
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
⊢ Eq (α := List (Prod.{u, v} α (Option β))) (zipLeft [] []) (map (fun (a : α) ↦ (a, none)) [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
tail : List α
⊢ Eq (α := List (Prod.{u, v} α (Option β))) ((head :: tail).zipLeft []) (map (fun (a : α) ↦ (a, none)) (head :: tail))

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
bs : List β
⊢ Eq (α := List (Prod.{u, v} α (Option β))) (zipLeft [] bs) []

Tactic:
rfl

Premises used: List.zipWithLeft, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
a : α
as : List α
⊢ Eq (α := List (Prod.{u, v} α (Option β))) ((a :: as).zipLeft []) ((a, none) :: map (fun (a : α) ↦ (a, none)) as)

Tactic:
rfl

Premises used: List.zipWithLeft, List.map, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
a : α
as : List α
b : β
bs : List β
⊢ (a :: as).zipLeft (b :: bs) = (a, some b) :: as.zipLeft bs

Tactic:
rfl

Premises used: List.zipWithLeft, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
bs : List β
⊢ Eq (α := List (Prod.{u, v} α (Option β))) (zipWithLeft Prod.mk [] bs) (Prod.fst (zipWithLeft' Prod.mk [] bs))

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
atl : List α
⊢ Eq (α := List (Prod.{u, v} α (Option β))) (zipWithLeft Prod.mk (head :: atl) [])
    (Prod.fst (zipWithLeft' Prod.mk (head :: atl) []))

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
atl : List α
head_1 : β
btl : List β
cons : zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst
⊢ zipWithLeft Prod.mk (head :: atl) (head_1 :: btl) = (zipWithLeft' Prod.mk (head :: atl) (head_1 :: btl)).fst

Tactic:
rw [zipWithLeft, zipWithLeft', cons_inj_right]

Premises used: List.zipWithLeft, List.cons_inj_right, List.zipWithLeft'
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
atl : List α
head_1 : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst

Tactic:
zipLeft_eq_zipLeft' atl btl