awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁_1 l₂_1 : List β
a : β
h : l₁_1 <+ l₂_1
ih : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l₁_1), SublistForall₂ R l₁ l₂_1
l₁ : List α
hl1 : Forall₂ R l₁ (a :: l₁_1)
⊢ SublistForall₂ R l₁ (a :: l₂_1)
have mpr : ∀ {a_1 : α} {l₁ : List α} (hr : R a_1 a) (hl : Forall₂ R l₁ l₁_1), SublistForall₂ R (a_1 :: l₁) (a :: l₂_1)
Tactic: obtain - | ⟨hr, hl⟩ := hl1
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 β
hl2 : l <+ l₂
⊢ ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l), SublistForall₂ R l₁ l₂
have mpr : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ []), SublistForall₂ R l₁ []
Tactic: induction hl2 with
    | slnil =>
      intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil
    | cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
    | cons_cons _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)
Cleared hypotheses: hl2
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
hl2 : l <+ l₂
mpr : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ []), SublistForall₂ R l₁ []
⊢ ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l), SublistForall₂ R l₁ l₂
have mpr₁ : ∀ {l₁ l₂ : List β} (a : β),
  l₁ <+ l₂ →
    ∀ (ih : ∀ {l₁_1 : List α} (hl1 : Forall₂ R l₁_1 l₁), SublistForall₂ R l₁_1 l₂) {l₁_1 : List α}
      (hl1 : Forall₂ R l₁_1 l₁), SublistForall₂ R l₁_1 (a :: l₂)
Tactic: induction hl2 with
    | slnil =>
      intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil
    | cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
    | cons_cons _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)
Cleared hypotheses: hl2
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
hl2 : l <+ l₂
mpr : ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ []), SublistForall₂ R l₁ []
mpr₁ :
  ∀ {l₁ l₂ : List β} (a : β),
    l₁ <+ l₂ →
      ∀ (ih : ∀ {l₁_1 : List α} (hl1 : Forall₂ R l₁_1 l₁), SublistForall₂ R l₁_1 l₂) {l₁_1 : List α}
        (hl1 : Forall₂ R l₁_1 l₁), SublistForall₂ R l₁_1 (a :: l₂)
⊢ ∀ {l₁ : List α} (hl1 : Forall₂ R l₁ l), SublistForall₂ R l₁ l₂
have mpr₂ : ∀ {l₁ l₂ : List β} (a : β),
  l₁ <+ l₂ →
    ∀ (ih : ∀ {l₁_1 : List α} (hl1 : Forall₂ R l₁_1 l₁), SublistForall₂ R l₁_1 l₂) {l₁_1 : List α}
      (hl1 : Forall₂ R l₁_1 (a :: l₁)), SublistForall₂ R l₁_1 (a :: l₂)
Tactic: induction hl2 with
    | slnil =>
      intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil
    | cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
    | cons_cons _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)
Cleared hypotheses: hl2
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
a b c : List α
⊢ SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
have revert : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
Tactic: revert a b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
head : α
tail : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail → SublistForall₂ Rₐ a tail
a b : List α
h1 : SublistForall₂ Rₐ a b
h2 : SublistForall₂ Rₐ b (head :: tail)
⊢ SublistForall₂ Rₐ a (head :: tail)
have cons : ∀ (h1 : SublistForall₂ Rₐ a []), SublistForall₂ Rₐ a (head :: tail)
Tactic: obtain - | ⟨hbc, tbc⟩ | btc := h2
Cleared hypotheses: b, h1, h2
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
head : α
tail : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail → SublistForall₂ Rₐ a tail
a b : List α
h1 : SublistForall₂ Rₐ a b
h2 : SublistForall₂ Rₐ b (head :: tail)
cons : ∀ (h1 : SublistForall₂ Rₐ a []), SublistForall₂ Rₐ a (head :: tail)
⊢ SublistForall₂ Rₐ a (head :: tail)
have cons₁ : ∀ {a₁ : α} {l₁ : List α} (h1 : SublistForall₂ Rₐ a (a₁ :: l₁)) (hbc : Rₐ a₁ head) (tbc : SublistForall₂ Rₐ l₁ tail),
  SublistForall₂ Rₐ a (head :: tail)
Tactic: obtain - | ⟨hbc, tbc⟩ | btc := h2
Cleared hypotheses: b, h1, h2
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
head : α
tail : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail → SublistForall₂ Rₐ a tail
a b : List α
h1 : SublistForall₂ Rₐ a b
h2 : SublistForall₂ Rₐ b (head :: tail)
cons : ∀ (h1 : SublistForall₂ Rₐ a []), SublistForall₂ Rₐ a (head :: tail)
cons₁ :
  ∀ {a₁ : α} {l₁ : List α} (h1 : SublistForall₂ Rₐ a (a₁ :: l₁)) (hbc : Rₐ a₁ head) (tbc : SublistForall₂ Rₐ l₁ tail),
    SublistForall₂ Rₐ a (head :: tail)
⊢ SublistForall₂ Rₐ a (head :: tail)
have cons₂ : ∀ (btc : SublistForall₂ Rₐ b tail), SublistForall₂ Rₐ a (head :: tail)
Tactic: obtain - | ⟨hbc, tbc⟩ | btc := h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
head : α
tail : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail → SublistForall₂ Rₐ a tail
a : List α
h1 : SublistForall₂ Rₐ a []
⊢ SublistForall₂ Rₐ a (head :: tail)
have cons : SublistForall₂ Rₐ [] (head :: tail)
Tactic: cases h1
Cleared hypotheses: a, h1
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
head : α
tail : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail → SublistForall₂ Rₐ a tail
a : List α
a₁ : α
l₁ : List α
h1 : SublistForall₂ Rₐ a (a₁ :: l₁)
hbc : Rₐ a₁ head
tbc : SublistForall₂ Rₐ l₁ tail
⊢ SublistForall₂ Rₐ a (head :: tail)
have cons : SublistForall₂ Rₐ [] (head :: tail)
Tactic: obtain - | ⟨hab, tab⟩ | atb := h1
Cleared hypotheses: a, h1
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
head : α
tail : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail → SublistForall₂ Rₐ a tail
a : List α
a₁ : α
l₁ : List α
h1 : SublistForall₂ Rₐ a (a₁ :: l₁)
hbc : Rₐ a₁ head
tbc : SublistForall₂ Rₐ l₁ tail
cons : SublistForall₂ Rₐ [] (head :: tail)
⊢ SublistForall₂ Rₐ a (head :: tail)
have cons₁ : ∀ {a₁_1 : α} {l₁_1 : List α} (hab : Rₐ a₁_1 a₁) (tab : SublistForall₂ Rₐ l₁_1 l₁),
  SublistForall₂ Rₐ (a₁_1 :: l₁_1) (head :: tail)
Tactic: obtain - | ⟨hab, tab⟩ | atb := h1
Cleared hypotheses: a, h1
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
head : α
tail : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail → SublistForall₂ Rₐ a tail
a : List α
a₁ : α
l₁ : List α
h1 : SublistForall₂ Rₐ a (a₁ :: l₁)
hbc : Rₐ a₁ head
tbc : SublistForall₂ Rₐ l₁ tail
cons : SublistForall₂ Rₐ [] (head :: tail)
cons₁ :
  ∀ {a₁_1 : α} {l₁_1 : List α} (hab : Rₐ a₁_1 a₁) (tab : SublistForall₂ Rₐ l₁_1 l₁),
    SublistForall₂ Rₐ (a₁_1 :: l₁_1) (head :: tail)
⊢ SublistForall₂ Rₐ a (head :: tail)
have cons₂ : ∀ (atb : SublistForall₂ Rₐ a l₁), SublistForall₂ Rₐ a (head :: tail)
Tactic: obtain - | ⟨hab, tab⟩ | atb := h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
c : List α
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
have nil : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b [] → SublistForall₂ Rₐ a []
Tactic: induction c with
    | nil =>
      rintro _ _ h1 h2
      cases h2
      exact h1
    | cons _ _ ih =>
      rintro a b h1 h2
      obtain - | ⟨hbc, tbc⟩ | btc := h2
      · cases h1
        exact SublistForall₂.nil
      · obtain - | ⟨hab, tab⟩ | atb := h1
        · exact SublistForall₂.nil
        · exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
        · exact SublistForall₂.cons_right (ih _ _ atb tbc)
      · exact SublistForall₂.cons_right (ih _ _ h1 btc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst : IsTrans α Rₐ
c : List α
nil : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b [] → SublistForall₂ Rₐ a []
⊢ ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b c → SublistForall₂ Rₐ a c
have cons : ∀ (head : α) (tail : List α)
  (ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail → SublistForall₂ Rₐ a tail) (a b : List α),
  SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b (head :: tail) → SublistForall₂ Rₐ a (head :: tail)
Tactic: induction c with
    | nil =>
      rintro _ _ h1 h2
      cases h2
      exact h1
    | cons _ _ ih =>
      rintro a b h1 h2
      obtain - | ⟨hbc, tbc⟩ | btc := h2
      · cases h1
        exact SublistForall₂.nil
      · obtain - | ⟨hab, tab⟩ | atb := h1
        · exact SublistForall₂.nil
        · exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
        · exact SublistForall₂.cons_right (ih _ _ atb tbc)
      · exact SublistForall₂.cons_right (ih _ _ h1 btc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l₂
have simp : (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂) ↔
  ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
Tactic: simp only [sublistForall₂_iff]
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂) ↔
    ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
have mp : (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂) →
  ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
mp :
  (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂) →
    ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
⊢ (∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂) ↔
    ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
have mpr : (∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂) →
  ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
l1 : List β
h1 : Forall₂ R l₁ l1
h2 : l1 <+ map f l₂
⊢ ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
have mp : ∀ (l' : List γ) (hl1 : l' <+ l₂) (h1 : Forall₂ R l₁ (map f l')) (h2 : map f l' <+ map f l₂),
  ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
Tactic: obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2
Cleared hypotheses: l1, h1, h2
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ ∃ (l : List γ), Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l ∧ l <+ l₂
have h : Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l' ∧ l' <+ l₂
Tactic: use l'
-- Lean 4 proof step from Mathlib.Data.List.Forall2 (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun (a : α) (c : γ) ↦ R a (f c)) l₁ l1
h2 : l1 <+ l₂
⊢ ∃ (l : List β), Forall₂ R l₁ l ∧ l <+ map f l₂
have h : Forall₂ R l₁ (map f l1) ∧ map f l1 <+ map f l₂
Tactic: use l1.map f
-- Lean 4 proof step from Mathlib.Data.List.GetD (goal)
Goal:
α : Type u
l : List α
d : α
⊢ (Function.Surjective.{1, u + 1} (β := α) fun (x : ℕ) ↦ l.getD x d) ↔ ∀ (x : α), x = d ∨ x ∈ l
have h : ∀ (a : α), (∃ (a_1 : ℕ), (fun (x : ℕ) ↦ l.getD x d) a_1 = a) ↔ a = d ∨ a ∈ l
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.Data.List.GetD (hypothesis)
Goal:
α : Type u
l : List α
d : α
⊢ ∀ (a : α), (∃ (a_1 : ℕ), (fun (x : ℕ) ↦ l.getD x d) a_1 = a) ↔ a = d ∨ a ∈ l
have this : ∃ (x : ℕ), l.length ≤ x
Tactic: have : ∃ x, l.length ≤ x := ⟨_, Nat.le_refl _⟩
-- Lean 4 proof step from Mathlib.Data.List.GetD (goal)
Goal:
α : Type u
l : List α
d : α
this : ∃ (x : ℕ), l.length ≤ x
⊢ ∀ (a : α), (∃ (a_1 : ℕ), (fun (x : ℕ) ↦ l.getD x d) a_1 = a) ↔ a = d ∨ a ∈ l
have h : ∀ (a : α),
  (∃ (x : ℕ), ∃ (h : x < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x h = a) ∨
      True ∧ d = a ↔
    a = d ∨ ∃ (x : ℕ), ∃ (h : x < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x h = a
Tactic: simp only [getD_eq_getElem?_getD, getD_getElem?, dite_eq_iff, Nat.not_lt, exists_prop, exists_or,
    exists_and_right, this, mem_iff_getElem?, getElem?_eq_some_iff]
-- Lean 4 proof step from Mathlib.Data.List.GetD (goal)
Goal:
α : Type u
l : List α
inst : Inhabited α
n : ℕ
⊢ l.getI n = (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default
have rw : l.getD n default = (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default
Tactic: rw [← getD_default_eq_getI, getD_eq_getElem?_getD]
-- Lean 4 proof step from Mathlib.Data.List.GetD (goal)
Goal:
α : Type u
l : List α
inst : Inhabited α
n : ℕ
rw : l.getD n default = (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default
⊢ l.getI n = (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default
have rw₁ : (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default =
  (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD default
Tactic: rw [← getD_default_eq_getI, getD_eq_getElem?_getD]
-- Lean 4 proof step from Mathlib.Data.List.GetD (goal)
Goal:
α : Type u
l : List α
inst : Inhabited α
⊢ l.getI 0 = l.headI
have nil : Eq.{u + 1} (α := α) (getI [] 0) (headI [])
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.GetD (goal)
Goal:
α : Type u
l : List α
inst : Inhabited α
nil : Eq.{u + 1} (α := α) (getI [] 0) (headI [])
⊢ l.getI 0 = l.headI
have cons : ∀ (head : α) (tail : List α), (head :: tail).getI 0 = (head :: tail).headI
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Indexes (goal)
Goal:
α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ mapIdx f l = ofFn (n := l.length) fun (i : Fin l.length) ↦ f (↑i : ℕ) (l.get i)
have nil : ∀ (f : ℕ → α → β),
  mapIdx f [] = ofFn (n := length.{u} (α := α) []) fun (i : Fin (length.{u} (α := α) [])) ↦ f (↑i : ℕ) (get [] i)
Tactic: induction l generalizing f with
  | nil => simp
  | cons _ _ IH => simp [IH]
Cleared hypotheses: l, f
-- Lean 4 proof step from Mathlib.Data.List.Indexes (goal)
Goal:
α : Type u
β : Type v
l : List α
f : ℕ → α → β
nil :
  ∀ (f : ℕ → α → β),
    mapIdx f [] = ofFn (n := length.{u} (α := α) []) fun (i : Fin (length.{u} (α := α) [])) ↦ f (↑i : ℕ) (get [] i)
⊢ mapIdx f l = ofFn (n := l.length) fun (i : Fin l.length) ↦ f (↑i : ℕ) (l.get i)
have cons : ∀ (head : α) (tail : List α)
  (IH : ∀ (f : ℕ → α → β), mapIdx f tail = ofFn (n := tail.length) fun (i : Fin tail.length) ↦ f (↑i : ℕ) (tail.get i))
  (f : ℕ → α → β),
  mapIdx f (head :: tail) =
    ofFn (n := (head :: tail).length) fun (i : Fin (head :: tail).length) ↦ f (↑i : ℕ) ((head :: tail).get i)
Tactic: induction l generalizing f with
  | nil => simp
  | cons _ _ IH => simp [IH]
Cleared hypotheses: l, f
-- Lean 4 proof step from Mathlib.Data.List.Indexes (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
⊢ mapIdxMAux' f arr.size (head :: tail) = mapIdxM.go f (head :: tail) arr *> pure PUnit.unit
have cons : Eq (α := m PUnit)
  (do
    f arr.size head
    mapIdxMAux' f (arr.size + 1) tail)
  do
  let x ← f arr.size head
  let x ← mapIdxM.go f tail (arr.push x)
  pure (const (List PUnit) id x PUnit.unit)
Tactic: simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind_map, bind_pure_unit,
      LawfulMonad.bind_assoc, pure_bind, mapIdxM.go]
-- Lean 4 proof step from Mathlib.Data.List.Indexes (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
⊢ Eq (α := m PUnit)
    (do
      f arr.size head
      mapIdxMAux' f (arr.size + 1) tail)
    do
    let x ← f arr.size head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
have cons : ∀ (head : m PUnit),
  Eq (α := m PUnit)
    (do
      head
      mapIdxMAux' f (arr.size + 1) tail)
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
Tactic: generalize (f (Array.size arr) head) = head
-- Lean 4 proof step from Mathlib.Data.List.Indexes (hypothesis)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head_1 : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
⊢ Eq (α := m PUnit)
    (do
      head
      mapIdxMAux' f (arr.size + 1) tail)
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
have this : (arr.push PUnit.unit).size = arr.size + 1
Tactic: have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push _
-- Lean 4 proof step from Mathlib.Data.List.Indexes (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
head_1 : α
tail : List α
ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit
arr : Array PUnit
head : m PUnit
this : (arr.push PUnit.unit).size = arr.size + 1
⊢ Eq (α := m PUnit)
    (do
      head
      mapIdxMAux' f (arr.size + 1) tail)
    do
    let x ← head
    let x ← mapIdxM.go f tail (arr.push x)
    pure (const (List PUnit) id x PUnit.unit)
have cons : Eq (α := m PUnit)
  (do
    head
    mapIdxM.go f tail (arr.push PUnit.unit) *> pure PUnit.unit)
  do
  let x ← head
  let x ← mapIdxM.go f tail (arr.push x)
  pure (const (List PUnit) id x PUnit.unit)
Tactic: rw [← this, ih]
-- Lean 4 proof step from Mathlib.Data.List.Indexes (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
arr : Array PUnit
⊢ mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit
have nil : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size [] = mapIdxM.go f [] arr *> pure PUnit.unit
Tactic: induction as generalizing arr with
  | nil => simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]
  | cons head tail ih =>
    simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind_map, bind_pure_unit,
      LawfulMonad.bind_assoc, pure_bind, mapIdxM.go]
    generalize (f (Array.size arr) head) = head
    have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push _
    rw [← this, ih]
    simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]
Cleared hypotheses: as, arr
-- Lean 4 proof step from Mathlib.Data.List.Indexes (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
as : List α
arr : Array PUnit
nil : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size [] = mapIdxM.go f [] arr *> pure PUnit.unit
⊢ mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit
have cons : ∀ (head : α) (tail : List α)
  (ih : ∀ (arr : Array PUnit), mapIdxMAux' f arr.size tail = mapIdxM.go f tail arr *> pure PUnit.unit)
  (arr : Array PUnit), mapIdxMAux' f arr.size (head :: tail) = mapIdxM.go f (head :: tail) arr *> pure PUnit.unit
Tactic: induction as generalizing arr with
  | nil => simp only [mapIdxMAux', mapIdxM.go, seqRight_eq, map_pure, seq_pure]
  | cons head tail ih =>
    simp only [mapIdxMAux', seqRight_eq, map_eq_pure_bind, seq_eq_bind_map, bind_pure_unit,
      LawfulMonad.bind_assoc, pure_bind, mapIdxM.go]
    generalize (f (Array.size arr) head) = head
    have : (arr.push ⟨⟩).size = arr.size + 1 := Array.size_push _
    rw [← this, ih]
    simp only [seqRight_eq, map_eq_pure_bind, seq_pure, LawfulMonad.bind_assoc, pure_bind]
Cleared hypotheses: as, arr
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.drop n l₁ <+: List.drop n l₂
have rw : List.take (l₁.length - n) (List.drop n l₂) <+: List.drop n l₂
Tactic: rw [prefix_iff_eq_take.mp h, drop_take]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ l₃ : List α
h_1 : l₁.length ≤ l₂.length
h : l₁ <+: l₂ ++ l₃
⊢ l₁ <+: l₂
have rw : ∀ (h : l₁ = take l₁.length (l₂ ++ l₃)), l₁ = take l₁.length l₂
Tactic: rw [prefix_iff_eq_take] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ l₃ : List α
h_1 : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₁ = take l₁.length l₂
have nth_rw : l₃ = [] ∨ l₁.length ≤ l₂.length
Tactic: nth_rw 1 [h, take_eq_left_iff]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ l₃ : List α
h_1 : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₃ = [] ∨ l₁.length ≤ l₂.length
have tauto : ¬l₃ = [] → l₁.length ≤ l₂.length
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l : List α
m n : ℕ
⊢ take m l <+: take n l ↔ m ≤ n ∨ l.length ≤ n
have simp : min m l.length ≤ n ↔ m ≤ n ∨ l.length ≤ n
Tactic: simp [prefix_take_iff, take_prefix]
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <+: l₂
⊢ l₁.flatten <+: l₂.flatten
have rcases : ∀ (l : List (List α)), l₁.flatten <+: (l₁ ++ l).flatten
Tactic: rcases h with ⟨l, rfl⟩
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+ l₂
⊢ l₁.flatten <:+ l₂.flatten
have rcases : ∀ (l : List (List α)), l₁.flatten <:+ (l ++ l₁).flatten
Tactic: rcases h with ⟨l, rfl⟩
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+: l₂
⊢ l₁.flatten <:+: l₂.flatten
have rcases : ∀ (l l' : List (List α)), l₁.flatten <:+: (l ++ l₁ ++ l').flatten
Tactic: rcases h with ⟨l, l', rfl⟩
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Infix (goal)
Goal:
α : Type u_1
n m : ℕ
l : List α
⊢ dropSlice n m l = take n l ++ drop m (drop n l)
have rw : take n l ++ drop (n + m) l = take n l ++ drop m (drop n l)
Tactic: rw [dropSlice_eq, drop_drop, Nat.add_comm]