awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
S T : Seq (Seq1 α)
⊢ ∃ (s : Seq α) (S_1 : Seq (Seq1 α)) (T_1 : Seq (Seq1 α)),
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)
have r : (S.append T).join = append nil (S.append T).join
Tactic: refine ⟨nil, S, T, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
S T : Seq (Seq1 α)
r : (S.append T).join = append nil (S.append T).join
⊢ ∃ (s : Seq α) (S_1 : Seq (Seq1 α)) (T_1 : Seq (Seq1 α)),
    (S.append T).join = s.append (S_1.append T_1).join ∧ S.join.append T.join = s.append (S_1.join.append T_1.join)
have r₁ : S.join.append T.join = append nil (S.join.append T.join)
Tactic: refine ⟨nil, S, T, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ (s.drop (k + 1)).get? m = s.get? (k + 1 + m)
have succ : (s.drop k).get? (m + 1) = s.get? (k + 1 + m)
Tactic: simp only [drop, get?_tail]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ (s.drop k).get? (m + 1) = s.get? (k + 1 + m)
have h : k + 1 + m = k + (m + 1)
Tactic: convert! ih using 2
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n m : ℕ
s : Seq α
⊢ (s.drop n).get? m = s.get? (n + m)
have zero : ∀ {m : ℕ}, (s.drop 0).get? m = s.get? (0 + m)
Tactic: induction n generalizing m with
  | zero => simp [drop]
  | succ k ih =>
    simp only [drop, get?_tail]
    convert! ih using 2
    lia
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n m : ℕ
s : Seq α
zero : ∀ {m : ℕ}, (s.drop 0).get? m = s.get? (0 + m)
⊢ (s.drop n).get? m = s.get? (n + m)
have succ : ∀ (k : ℕ) (ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)) {m : ℕ}, (s.drop (k + 1)).get? m = s.get? (k + 1 + m)
Tactic: induction n generalizing m with
  | zero => simp [drop]
  | succ k ih =>
    simp only [drop, get?_tail]
    convert! ih using 2
    lia
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (n + 1)
have rw : s.tail.drop n = s.drop (1 + n)
Tactic: rw [Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
have symm : s.drop (1 + n) = s.tail.drop n
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.drop (n + 1)).head = s.get? (n + 1)
have succ : (s.tail.drop n).head = s.tail.get? n
Tactic: rw [← get?_tail, ← dropn_tail]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (s.drop n).head = s.get? n
have zero : ∀ (s : Seq α), (s.drop 0).head = s.get? 0
Tactic: induction n generalizing s with
  | zero => rfl
  | succ n IH => rw [← get?_tail, ← dropn_tail]; apply IH
Cleared hypotheses: s, n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
zero : ∀ (s : Seq α), (s.drop 0).head = s.get? 0
⊢ (s.drop n).head = s.get? n
have succ : ∀ (n : ℕ) (IH : ∀ (s : Seq α), (s.drop n).head = s.get? n) (s : Seq α), (s.drop (n + 1)).head = s.get? (n + 1)
Tactic: induction n generalizing s with
  | zero => rfl
  | succ n IH => rw [← get?_tail, ← dropn_tail]; apply IH
Cleared hypotheses: s, n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := Seq α) (drop nil n) nil
have zero : Eq.{u + 1} (α := Seq α) (drop nil 0) nil
Tactic: induction n with
  | zero => simp [drop]
  | succ m ih => simp [← dropn_tail, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
zero : Eq.{u + 1} (α := Seq α) (drop nil 0) nil
⊢ Eq.{u + 1} (α := Seq α) (drop nil n) nil
have succ : ∀ (m : ℕ) (ih : Eq.{u + 1} (α := Seq α) (drop nil m) nil), Eq.{u + 1} (α := Seq α) (drop nil (m + 1)) nil
Tactic: induction n with
  | zero => simp [drop]
  | succ m ih => simp [← dropn_tail, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
⊢ ((cons x s).drop (n + 1)).length' = (cons x s).length' - (↑(n + 1) : ℕ∞)
have succ : (s.drop n).length' = s.length' + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
⊢ (s.drop n).length' = s.length' + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have h : s.length' + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = s.length' - (↑n : ℕ∞)
Tactic: convert! drop_length' using 1
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
⊢ s.length' + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = s.length' - (↑n : ℕ∞)
have h : ∀ (m : ℕ∞), m + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = m - (↑n : ℕ∞)
Tactic: generalize s.length' = m
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
m : ℕ∞
⊢ m + 1 - HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = m - (↑n : ℕ∞)
have h : ∀ (m : ℕ), m + 1 - (n + 1) = m - n
Tactic: enat_to_nat
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (s.drop (n + 1)).length' = s.length' - (↑(n + 1) : ℕ∞)
have succ : length'.{u} (α := α) (drop nil (n + 1)) = length'.{u} (α := α) nil - (↑(n + 1) : ℕ∞)
Tactic: cases s with
    | nil => simp
    | cons x s =>
      simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
      convert! drop_length' using 1
      generalize s.length' = m
      enat_to_nat
      lia
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
succ : length'.{u} (α := α) (drop nil (n + 1)) = length'.{u} (α := α) nil - (↑(n + 1) : ℕ∞)
⊢ (s.drop (n + 1)).length' = s.length' - (↑(n + 1) : ℕ∞)
have succ₁ : ∀ (x : α) (s : Seq α), ((cons x s).drop (n + 1)).length' = (cons x s).length' - (↑(n + 1) : ℕ∞)
Tactic: cases s with
    | nil => simp
    | cons x s =>
      simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
      convert! drop_length' using 1
      generalize s.length' = m
      enat_to_nat
      lia
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
s : Seq α
⊢ (s.drop n).length' = s.length' - (↑n : ℕ∞)
have zero : (s.drop 0).length' = s.length' - (↑0 : ℕ∞)
Tactic: cases n with
  | zero => simp
  | succ n =>
    cases s with
    | nil => simp
    | cons x s =>
      simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
      convert! drop_length' using 1
      generalize s.length' = m
      enat_to_nat
      lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
n : ℕ
s : Seq α
zero : (s.drop 0).length' = s.length' - (↑0 : ℕ∞)
⊢ (s.drop n).length' = s.length' - (↑n : ℕ∞)
have succ : ∀ (n : ℕ), (s.drop (n + 1)).length' = s.length' - (↑(n + 1) : ℕ∞)
Tactic: cases n with
  | zero => simp
  | succ n =>
    cases s with
    | nil => simp
    | cons x s =>
      simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
      convert! drop_length' using 1
      generalize s.length' = m
      enat_to_nat
      lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
n m : ℕ
⊢ List.drop m (take n s) = take (n - m) (s.drop m)
have h : ∀ (i : ℕ) (a : α),
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (List.drop m (take n s)) i = some a ↔
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (n - m) (s.drop m)) i = some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq α
⊢ zipWith f s nil = nil
have h : ∀ (n : ℕ), (zipWith f s nil).get? n = get? nil n
Tactic: ext1
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
⊢ zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s')
have h : ∀ (n : ℕ), (zipWith f (cons x s) (cons x' s')).get? n = (cons (f x x') (zipWith f s s')).get? n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? n = (cons (f x x') (zipWith f s s')).get? n
have h : (zipWith f (cons x s) (cons x' s')).get? 0 = (cons (f x x') (zipWith f s s')).get? 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n : ℕ
h : (zipWith f (cons x s) (cons x' s')).get? 0 = (cons (f x x') (zipWith f s s')).get? 0
⊢ (zipWith f (cons x s) (cons x' s')).get? n = (cons (f x x') (zipWith f s s')).get? n
have h₁ : ∀ (n : ℕ), (zipWith f (cons x s) (cons x' s')).get? (n + 1) = (cons (f x x') (zipWith f s s')).get? (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
x : α
⊢ (cons x s).enum = cons (0, x) (map (Prod.map Nat.succ id) s.enum)
have h : (cons x s).enum.get? 0 = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? 0
Tactic: ext ⟨n⟩ : 1
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
x : α
h : (cons x s).enum.get? 0 = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? 0
⊢ (cons x s).enum = cons (0, x) (map (Prod.map Nat.succ id) s.enum)
have h₁ : ∀ (n : ℕ), (cons x s).enum.get? (n + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n + 1)
Tactic: ext ⟨n⟩ : 1
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
s : Seq α
x : α
n : ℕ
⊢ (cons x s).enum.get? (n + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n + 1)
have h : Option.map (Prod.mk (n + 1)) (s.get? n) = Option.map (Prod.map Nat.succ id ∘ Prod.mk n) (s.get? n)
Tactic: simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
⊢ zipWith g (map f₁ s₁) (map f₂ s₂) = zipWith (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) s₁ s₂
have h : ∀ (n : ℕ), (zipWith g (map f₁ s₁) (map f₂ s₂)).get? n = get? (zipWith (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) s₁ s₂) n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ (zipWith g (map f₁ s₁) (map f₂ s₂)).get? n = get? (zipWith (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) s₁ s₂) n
have h : Option.map₂ g (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
  Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (s₁.get? n) (s₂.get? n)
Tactic: simp only [get?_zipWith, map_get?]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (s₁.get? n) (s₂.get? n)
have h : Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
  Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)
Tactic: cases s₁.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
h :
  Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)
⊢ Option.map₂ g (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (s₁.get? n) (s₂.get? n)
have h₁ : ∀ (val : α),
  Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) (s₂.get? n)
Tactic: cases s₁.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)
have h : Option.map₂ g (Option.map f₁ none) (Option.map f₂ none) = Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none none
Tactic: cases s₂.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
h :
  Option.map₂ g (Option.map f₁ none) (Option.map f₂ none) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none none
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)
have h₁ : ∀ (val : β),
  Option.map₂ g (Option.map f₁ none) (Option.map f₂ (some val)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) none (some val)
Tactic: cases s₂.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val : α
⊢ Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) (s₂.get? n)
have h : Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ none) =
  Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) none
Tactic: cases s₂.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val : α
h :
  Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ none) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) none
⊢ Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) (s₂.get? n)
have h₁ : ∀ (val_1 : β),
  Option.map₂ g (Option.map f₁ (some val)) (Option.map f₂ (some val_1)) =
    Option.map₂ (fun (a : α) (b : β) ↦ g (f₁ a) (f₂ b)) (some val) (some val_1)
Tactic: cases s₂.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
g : α' → β → γ
⊢ zipWith g (map f s₁) s₂ = zipWith (fun (a : α) (b : β) ↦ g (f a) b) s₁ s₂
have h : s₂ = map id s₂
Tactic: convert! zipWith_map _ _ _ (@id β) _
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
g : α → β' → γ
⊢ zipWith g s₁ (map f s₂) = zipWith (fun (a : α) (b : β) ↦ g a (f b)) s₁ s₂
have h : s₁ = map id s₁
Tactic: convert! zipWith_map _ _ (@id α) _ _
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
⊢ (map f₁ s₁).zip (map f₂ s₂) = map (Prod.map f₁ f₂) (s₁.zip s₂)
have h : ∀ (n : ℕ), ((map f₁ s₁).zip (map f₂ s₂)).get? n = (map (Prod.map f₁ f₂) (s₁.zip s₂)).get? n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ ((map f₁ s₁).zip (map f₂ s₂)).get? n = (map (Prod.map f₁ f₂) (s₁.zip s₂)).get? n
have h : Option.map₂ Prod.mk (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
  Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (s₁.get? n) (s₂.get? n))
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (s₁.get? n) (s₂.get? n))
have h : Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
  Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))
Tactic: cases s₁.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
h :
  Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))
⊢ Option.map₂ Prod.mk (Option.map f₁ (s₁.get? n)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (s₁.get? n) (s₂.get? n))
have h₁ : ∀ (val : α),
  Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) (s₂.get? n))
Tactic: cases s₁.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))
have h : Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ none) =
  Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none none)
Tactic: cases s₂.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
h :
  Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none none)
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))
have h₁ : ∀ (val : β),
  Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (some val)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (some val))
Tactic: cases s₂.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) (s₂.get? n))
have h : Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ none) =
  Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) none)
Tactic: cases s₂.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val : α
h :
  Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) none)
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) (s₂.get? n))
have h₁ : ∀ (val_1 : β),
  Option.map₂ Prod.mk (Option.map f₁ (some val)) (Option.map f₂ (some val_1)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val) (some val_1))
Tactic: cases s₂.get? n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
⊢ (map f s₁).zip s₂ = map (Prod.map f id) (s₁.zip s₂)
have h : s₂ = map id s₂
Tactic: convert! zip_map _ _ _ _
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
⊢ s₁.zip (map f s₂) = map (Prod.map id f) (s₁.zip s₂)
have h : s₁ = map id s₁
Tactic: convert! zip_map _ _ _ _
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ cons init
      (corec
        (fun (x : Prod.{v, u} β (Seq α)) ↦
          match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
          | none => none
          | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
        (init, cons x s)) =
    cons init
      (cons (f init x)
        (corec
          (fun (x : Prod.{v, u} β (Seq α)) ↦
            match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
            | none => none
            | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
          (f init x, s)))
have e_s : corec
    (fun (x : Prod.{v, u} β (Seq α)) ↦
      match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
      | none => none
      | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
    (init, cons x s) =
  cons (f init x)
    (corec
      (fun (x : Prod.{v, u} β (Seq α)) ↦
        match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
        | none => none
        | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
      (f init x, s))
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ corec
      (fun (x : Prod.{v, u} β (Seq α)) ↦
        match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
        | none => none
        | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
      (init, cons x s) =
    cons (f init x)
      (corec
        (fun (x : Prod.{v, u} β (Seq α)) ↦
          match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) x.2.destruct with
          | none => none
          | some (x_1, s) => some (f x.1 x_1, f x.1 x_1, s))
        (f init x, s))
have e_s : (match (motive := Option (Seq1 α) → Option (β × Prod.{v, u} β (Seq α))) (init, cons x s).2.destruct with
  | none => none
  | some (x_1, s_1) => some (f (init, cons x s).1 x_1, f (init, cons x s).1 x_1, s_1)) =
  some (f init x, f init x, s)
Tactic: rw [corec_cons]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
f : α → α
s : Seq α
n m : ℕ
⊢ (s.update n f).get? m = if m = n then Option.map f (s.get? m) else s.get? m
have simp : (if m = n then Option.map f (s.get? n) else s.get? m) = if m = n then Option.map f (s.get? m) else s.get? m
Tactic: simp [update, Function.update]
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
f : α → α
s : Seq α
n m : ℕ
⊢ (if m = n then Option.map f (s.get? n) else s.get? m) = if m = n then Option.map f (s.get? m) else s.get? m
have pos : ∀ (h_if : m = n), Option.map f (s.get? n) = Option.map f (s.get? m)
Tactic: split_ifs with h_if
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
f : α → α
s : Seq α
n m : ℕ
pos : ∀ (h_if : m = n), Option.map f (s.get? n) = Option.map f (s.get? m)
⊢ (if m = n then Option.map f (s.get? n) else s.get? m) = if m = n then Option.map f (s.get? m) else s.get? m
have neg : ∀ (h_if : ¬m = n), s.get? m = s.get? m
Tactic: split_ifs with h_if
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
f : α → α
n : ℕ
⊢ update nil n f = nil
have h : ∀ (m : ℕ), (update nil n f).get? m = get? nil m
Tactic: ext1 m
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
⊢ (cons hd tl).update 0 f = cons (f hd) tl
have h : ∀ (n : ℕ), ((cons hd tl).update 0 f).get? n = (cons (f hd) tl).get? n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ ((cons hd tl).update 0 f).get? n = (cons (f hd) tl).get? n
have h : ((cons hd tl).update 0 f).get? 0 = (cons (f hd) tl).get? 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Basic (goal)
Goal:
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
h : ((cons hd tl).update 0 f).get? 0 = (cons (f hd) tl).get? 0
⊢ ((cons hd tl).update 0 f).get? n = (cons (f hd) tl).get? n
have h₁ : ∀ (n : ℕ), ((cons hd tl).update 0 f).get? (n + 1) = (cons (f hd) tl).get? (n + 1)
Tactic: cases n
Cleared hypotheses: n