awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
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₂
⊢ lookmap f l₁ ~ lookmap f l₂
have nil : ∀ (H : Pairwise (fun (a b : α) ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) []),
  lookmap f [] ~ lookmap f []
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
Cleared hypotheses: H, p
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
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 []
⊢ lookmap f l₁ ~ lookmap f l₂
have 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₂)
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
Cleared hypotheses: H, p
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
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₂)
⊢ lookmap f l₁ ~ lookmap f l₂
have 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)
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
Cleared hypotheses: H, p
-- Lean 4 proof step from Mathlib.Data.List.Lookmap (goal)
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)
⊢ lookmap f l₁ ~ lookmap f l₂
have 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₃
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
Cleared hypotheses: H, p
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left' f as [] = (map (fun (a : α) ↦ f a none) as, [])
have nil : map₂Left' f [] [] = (map (fun (a : α) ↦ f a none) [], [])
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
nil : map₂Left' f [] [] = (map (fun (a : α) ↦ f a none) [], [])
⊢ map₂Left' f as [] = (map (fun (a : α) ↦ f a none) as, [])
have cons : ∀ (head : α) (tail : List α), map₂Left' f (head :: tail) [] = (map (fun (a : α) ↦ f a none) (head :: tail), [])
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right' f [] bs = (map (f none) bs, [])
have nil : map₂Right' f [] [] = (map (f none) [], [])
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
nil : map₂Right' f [] [] = (map (f none) [], [])
⊢ map₂Right' f [] bs = (map (f none) bs, [])
have cons : ∀ (head : β) (tail : List β), map₂Right' f [] (head :: tail) = (map (f none) (head :: tail), [])
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List β
⊢ zipWith f [] l = []
have nil : zipWith f [] [] = []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List β
nil : zipWith f [] [] = []
⊢ zipWith f [] l = []
have cons : ∀ (head : β) (tail : List β), zipWith f [] (head :: tail) = []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List α
⊢ zipWith f l [] = []
have nil : zipWith f [] [] = []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List α
nil : zipWith f [] [] = []
⊢ zipWith f l [] = []
have cons : ∀ (head : α) (tail : List α), zipWith f (head :: tail) [] = []
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ zipWith (flip f) (b :: bs) (a :: as) = zipWith f (a :: as) (b :: bs)
have simp! : flip f b a = f a b
Tactic: simp! [zipWith_flip]
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
as : List α
⊢ Eq (α := List (Prod.{u, v} α (Option β)) × List β) (as.zipLeft' []) (map (fun (a : α) ↦ (a, none)) as, [])
have nil : Eq (α := List (Prod.{u, v} α (Option β)) × List β) (zipLeft' [] []) (map (fun (a : α) ↦ (a, none)) [], [])
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
as : List α
nil : Eq (α := List (Prod.{u, v} α (Option β)) × List β) (zipLeft' [] []) (map (fun (a : α) ↦ (a, none)) [], [])
⊢ Eq (α := List (Prod.{u, v} α (Option β)) × List β) (as.zipLeft' []) (map (fun (a : α) ↦ (a, none)) as, [])
have cons : ∀ (head : α) (tail : List α),
  Eq (α := List (Prod.{u, v} α (Option β)) × List β) ((head :: tail).zipLeft' [])
    (map (fun (a : α) ↦ (a, none)) (head :: tail), [])
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
bs : List β
⊢ Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] bs) (map (fun (b : β) ↦ (none, b)) bs, [])
have nil : Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] []) (map (fun (b : β) ↦ (none, b)) [], [])
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
bs : List β
nil : Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] []) (map (fun (b : β) ↦ (none, b)) [], [])
⊢ Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] bs) (map (fun (b : β) ↦ (none, b)) bs, [])
have cons : ∀ (head : β) (tail : List β),
  Eq (α := List (Prod.{u, v} (Option α) β) × List α) (zipRight' [] (head :: tail))
    (map (fun (b : β) ↦ (none, b)) (head :: tail), [])
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left f as [] = map (fun (a : α) ↦ f a none) as
have nil : map₂Left f [] [] = map (fun (a : α) ↦ f a none) []
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
nil : map₂Left f [] [] = map (fun (a : α) ↦ f a none) []
⊢ map₂Left f as [] = map (fun (a : α) ↦ f a none) as
have cons : ∀ (head : α) (tail : List α), map₂Left f (head :: tail) [] = map (fun (a : α) ↦ f a none) (head :: tail)
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : (a :: as).length ≤ (b :: bs).length
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun (a : α) (b : β) ↦ f a (some b)) (a :: as) (b :: bs)
have h₁ : as.length ≤ bs.length
Tactic: simp only [length_cons, succ_le_succ_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right f [] bs = map (f none) bs
have nil : map₂Right f [] [] = map (f none) []
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
nil : map₂Right f [] [] = map (f none) []
⊢ map₂Right f [] bs = map (f none) bs
have cons : ∀ (head : β) (tail : List β), map₂Right f [] (head :: tail) = map (f none) (head :: tail)
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
h : bs.length ≤ as.length
⊢ map₂Right f as bs = zipWith (fun (a : α) (b : β) ↦ f (some a) b) as bs
have this : 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
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
as : List α
⊢ Eq (α := List (Prod.{u, v} α (Option β))) (as.zipLeft []) (map (fun (a : α) ↦ (a, none)) as)
have nil : Eq (α := List (Prod.{u, v} α (Option β))) (zipLeft [] []) (map (fun (a : α) ↦ (a, none)) [])
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
as : List α
nil : Eq (α := List (Prod.{u, v} α (Option β))) (zipLeft [] []) (map (fun (a : α) ↦ (a, none)) [])
⊢ Eq (α := List (Prod.{u, v} α (Option β))) (as.zipLeft []) (map (fun (a : α) ↦ (a, none)) as)
have cons : ∀ (head : α) (tail : List α),
  Eq (α := List (Prod.{u, v} α (Option β))) ((head :: tail).zipLeft []) (map (fun (a : α) ↦ (a, none)) (head :: tail))
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
head : α
atl : List α
head_1 : β
btl : List β
⊢ zipWithLeft Prod.mk (head :: atl) (head_1 :: btl) = (zipWithLeft' Prod.mk (head :: atl) (head_1 :: btl)).fst
have cons : zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst
Tactic: rw [zipWithLeft, zipWithLeft', cons_inj_right]
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
bs : List β
head : α
atl : List α
⊢ zipWithLeft Prod.mk (head :: atl) bs = (zipWithLeft' Prod.mk (head :: atl) bs).fst
have cons : Eq (α := List (Prod.{u, v} α (Option β))) (zipWithLeft Prod.mk (head :: atl) [])
  (Prod.fst (zipWithLeft' Prod.mk (head :: atl) []))
Tactic: cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
bs : List β
head : α
atl : List α
cons :
  Eq (α := List (Prod.{u, v} α (Option β))) (zipWithLeft Prod.mk (head :: atl) [])
    (Prod.fst (zipWithLeft' Prod.mk (head :: atl) []))
⊢ zipWithLeft Prod.mk (head :: atl) bs = (zipWithLeft' Prod.mk (head :: atl) bs).fst
have cons₁ : ∀ (head_1 : β) (btl : List β),
  zipWithLeft Prod.mk (head :: atl) (head_1 :: btl) = (zipWithLeft' Prod.mk (head :: atl) (head_1 :: btl)).fst
Tactic: cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
as : List α
bs : List β
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst
have nil : Eq (α := List (Prod.{u, v} α (Option β))) (zipWithLeft Prod.mk [] bs) (Prod.fst (zipWithLeft' Prod.mk [] bs))
Tactic: cases as with
  | nil => rfl
  | cons _ atl =>
    cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
as : List α
bs : List β
nil : Eq (α := List (Prod.{u, v} α (Option β))) (zipWithLeft Prod.mk [] bs) (Prod.fst (zipWithLeft' Prod.mk [] bs))
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst
have cons : ∀ (head : α) (atl : List α), zipWithLeft Prod.mk (head :: atl) bs = (zipWithLeft' Prod.mk (head :: atl) bs).fst
Tactic: cases as with
  | nil => rfl
  | cons _ atl =>
    cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
bs : List β
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (map (fun (b : β) ↦ (none, b)) bs)
have nil : Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] []) (map (fun (b : β) ↦ (none, b)) [])
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
bs : List β
nil : Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] []) (map (fun (b : β) ↦ (none, b)) [])
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (map (fun (b : β) ↦ (none, b)) bs)
have cons : ∀ (head : β) (tail : List β),
  Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] (head :: tail)) (map (fun (b : β) ↦ (none, b)) (head :: tail))
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipRight bs = (as.zipRight' bs).fst
have nil : ∀ (bs : List β), Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (Prod.fst (zipRight' [] bs))
Tactic: induction as generalizing bs
Cleared hypotheses: as, bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
as : List α
bs : List β
nil : ∀ (bs : List β), Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (Prod.fst (zipRight' [] bs))
⊢ as.zipRight bs = (as.zipRight' bs).fst
have cons : ∀ (head : α) (tail : List α),
  (∀ (bs : List β), tail.zipRight bs = (tail.zipRight' bs).fst) →
    ∀ (bs : List β), (head :: tail).zipRight bs = ((head :: tail).zipRight' bs).fst
Tactic: induction as generalizing bs
Cleared hypotheses: as, bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
bs : List β
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (Prod.fst (zipRight' [] bs))
have nil : Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] []) (Prod.fst (zipRight' [] []))
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
bs : List β
nil : Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] []) (Prod.fst (zipRight' [] []))
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (Prod.fst (zipRight' [] bs))
have nil₁ : ∀ (head : β) (tail : List β),
  Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] (head :: tail)) (Prod.fst (zipRight' [] (head :: tail)))
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
head : α
tail : List α
tail_ih : ∀ (bs : List β), tail.zipRight bs = (tail.zipRight' bs).fst
bs : List β
⊢ (head :: tail).zipRight bs = ((head :: tail).zipRight' bs).fst
have cons : Eq (α := List (Prod.{u, v} (Option α) β)) ((head :: tail).zipRight []) (Prod.fst ((head :: tail).zipRight' []))
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.Map2 (goal)
Goal:
α : Type u
β : Type v
head : α
tail : List α
tail_ih : ∀ (bs : List β), tail.zipRight bs = (tail.zipRight' bs).fst
bs : List β
cons : Eq (α := List (Prod.{u, v} (Option α) β)) ((head :: tail).zipRight []) (Prod.fst ((head :: tail).zipRight' []))
⊢ (head :: tail).zipRight bs = ((head :: tail).zipRight' bs).fst
have cons₁ : ∀ (head_1 : β) (tail_1 : List β),
  (head :: tail).zipRight (head_1 :: tail_1) = ((head :: tail).zipRight' (head_1 :: tail_1)).fst
Tactic: cases bs
Cleared hypotheses: bs
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)
have simp : (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
  (Eq (α := Option α)
      (Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
          (fun (val : α) ↦ if r hd val then some hd else some val) (foldl (argAux r) o tl) :
        Option α)
      (none : Option α) ↔
    (tl = [] ∧ [hd] = []) ∧ o = none)
Tactic: simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil_iff]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (Eq (α := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
            (fun (val : α) ↦ if r hd val then some hd else some val) (foldl (argAux r) o tl) :
          Option α)
        (none : Option α) ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)
have none : (Eq.{u_1 + 1} (α := Option α) none none ↔ tl = [] ∧ o = none) →
  (Eq.{u_1 + 1} (α := Option α)
      (Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
          (fun (val : α) ↦ if r hd val then some hd else some val) none :
        Option α)
      (none : Option α) ↔
    (tl = [] ∧ [hd] = []) ∧ o = none)
Tactic: cases foldl (argAux r) o tl
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
none :
  (Eq.{u_1 + 1} (α := Option α) Option.none Option.none ↔ tl = [] ∧ o = Option.none) →
    (Eq.{u_1 + 1} (α := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
            (fun (val : α) ↦ if r hd val then some hd else some val) Option.none :
          Option α)
        (Option.none : Option α) ↔
      (tl = [] ∧ [hd] = []) ∧ o = Option.none)
⊢ (foldl (argAux r) o tl = Option.none ↔ tl = [] ∧ o = Option.none) →
    (Eq (α := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
            (fun (val : α) ↦ if r hd val then some hd else some val) (foldl (argAux r) o tl) :
          Option α)
        (Option.none : Option α) ↔
      (tl = [] ∧ [hd] = []) ∧ o = Option.none)
have some : ∀ (val : α),
  (some val = Option.none ↔ tl = [] ∧ o = Option.none) →
    (Eq (α := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
            (fun (val : α) ↦ if r hd val then some hd else some val) (some val) :
          Option α)
        (Option.none : Option α) ↔
      (tl = [] ∧ [hd] = []) ∧ o = Option.none)
Tactic: cases foldl (argAux r) o tl
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd val : α
⊢ (some val = none ↔ tl = [] ∧ o = none) →
    ((if r hd val then some hd else some val) = none ↔ (tl = [] ∧ [hd] = []) ∧ o = none)
have pos : r hd val → (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd val : α
pos : r hd val → (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)
⊢ (some val = none ↔ tl = [] ∧ o = none) →
    ((if r hd val then some hd else some val) = none ↔ (tl = [] ∧ [hd] = []) ∧ o = none)
have neg : ¬r hd val → (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l l_1 : List α
a : α
h : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l_1 → m ∈ a :: l_1
a_1 : α
⊢ ∀ (m : α), m ∈ foldl (argAux r) (some a_1) (l_1 ++ [a]) → m ∈ a_1 :: (l_1 ++ [a])
have simp : ∀ (m : α),
  Membership.mem (γ := Option α)
      (Option.rec (motive := fun (x : Option α) ↦ Option α) (some a)
          (fun (val : α) ↦ if r a val then some a else some val) (foldl (argAux r) (some a_1) l_1) :
        Option α)
      m →
    m ∈ a_1 :: (l_1 ++ [a])
Tactic: simp only [foldl_append, foldl_cons, foldl_nil, argAux]