awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
nil : Eq.{u_1 + 1} (α := WithTop α) (minimum []) (minimum [])
cons : ∀ (x : α) {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.minimum = l₂.minimum → (x :: l₁).minimum = (x :: l₂).minimum
⊢ l.minimum = l'.minimum
have swap : ∀ (x y : α) (l : List α), (y :: x :: l).minimum = (x :: y :: l).minimum
Tactic: induction h with grind [minimum_cons]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
nil : Eq.{u_1 + 1} (α := WithTop α) (minimum []) (minimum [])
cons : ∀ (x : α) {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.minimum = l₂.minimum → (x :: l₁).minimum = (x :: l₂).minimum
swap : ∀ (x y : α) (l : List α), (y :: x :: l).minimum = (x :: y :: l).minimum
⊢ l.minimum = l'.minimum
have trans : ∀ {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁.minimum = l₂.minimum → l₂.minimum = l₃.minimum → l₁.minimum = l₃.minimum
Tactic: induction h with grind [minimum_cons]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : l.maximum = (↑y : WithBot α)
⊢ l.max?.getD d = WithBot.unbotD d (↑y : WithBot α)
have hy₁ : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
Tactic: rw [List.maximum_eq_coe_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = WithBot.unbotD d (↑y : WithBot α)
have coe : l.max?.getD d = y
Tactic: simp only [WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
⊢ (some z).getD d = y
have this : Std.Antisymm fun (x1 x2 : α) ↦ x1 ≤ x2
Tactic: have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
this : Std.Antisymm fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ (some z).getD d = y
have hz₁ : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
Tactic: rw [List.max?_eq_some_iff] at hz
Cleared hypotheses: hz, this
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ (some z).getD d = y
have coe : z = y
Tactic: rw [Option.getD_some]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
⊢ l.max?.getD d = y
have coe : ∀ (x : Option α) (hz : l.max? = x), x.getD d = y
Tactic: cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
d : α
⊢ l.max?.getD d = WithBot.unbotD d l.maximum
have cases : ∀ (x : WithBot α) (hy : l.maximum = x), l.max?.getD d = WithBot.unbotD d x
Tactic: cases hy : l.maximum with
  | bot => simp [List.maximum_eq_bot.mp hy]
  | coe y =>
    rw [List.maximum_eq_coe_iff] at hy
    simp only [WithBot.unbotD_coe]
    cases hz : l.max? with
    | none => simp [List.max?_eq_none_iff.mp hz] at hy
    | some z =>
      have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩
      rw [List.max?_eq_some_iff] at hz
      · rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
hd : α
tl : List α
IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum
h : hd :: tl ≠ []
⊢ (↑(foldr max ⊥ (hd :: tl)) : WithBot α) = (hd :: tl).maximum
have cons : max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
Tactic: rw [maximum_cons, foldr, WithBot.coe_max]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
hd : α
tl : List α
IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum
h : hd :: tl ≠ []
⊢ max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
have pos : ∀ (h : tl = []), max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
Tactic: by_cases h : tl = []
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
hd : α
tl : List α
IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum
h : hd :: tl ≠ []
pos : ∀ (h : tl = []), max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
⊢ max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
have neg : ∀ (h : ¬tl = []), max (↑hd : WithBot α) (↑(foldr max ⊥ tl) : WithBot α) = max (↑hd : WithBot α) tl.maximum
Tactic: by_cases h : tl = []
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
h : l ≠ []
⊢ (↑(foldr max ⊥ l) : WithBot α) = l.maximum
have nil : ∀ (h : Ne.{u_1 + 1} (α := List α) [] []), Eq.{u_1 + 1} (α := WithBot α) (↑(foldr max ⊥ []) : WithBot α) (maximum [])
Tactic: induction l with
  | nil => contradiction
  | cons hd tl IH =>
    rw [maximum_cons, foldr, WithBot.coe_max]
    by_cases h : tl = []
    · simp [h]
    · simp [IH h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
h : l ≠ []
nil :
  ∀ (h : Ne.{u_1 + 1} (α := List α) [] []), Eq.{u_1 + 1} (α := WithBot α) (↑(foldr max ⊥ []) : WithBot α) (maximum [])
⊢ (↑(foldr max ⊥ l) : WithBot α) = l.maximum
have cons : ∀ (hd : α) (tl : List α) (IH : ∀ (h : tl ≠ []), (↑(foldr max ⊥ tl) : WithBot α) = tl.maximum) (h : hd :: tl ≠ []),
  (↑(foldr max ⊥ (hd :: tl)) : WithBot α) = (hd :: tl).maximum
Tactic: induction l with
  | nil => contradiction
  | cons hd tl IH =>
    rw [maximum_cons, foldr, WithBot.coe_max]
    by_cases h : tl = []
    · simp [h]
    · simp [IH h]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
a : α
h : ∀ (x : α), x ∈ l → x ≤ a
⊢ foldr max ⊥ l ≤ a
have nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → x ≤ a), foldr max ⊥ [] ≤ a
Tactic: induction l with
  | nil => simp
  | cons y l IH => simpa [h y mem_cons_self] using IH fun x hx => h x <| mem_cons_of_mem _ hx
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
a : α
h : ∀ (x : α), x ∈ l → x ≤ a
nil : ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → x ≤ a), foldr max ⊥ [] ≤ a
⊢ foldr max ⊥ l ≤ a
have cons : ∀ (y : α) (l : List α) (IH : ∀ (h : ∀ (x : α), x ∈ l → x ≤ a), foldr max ⊥ l ≤ a) (h : ∀ (x : α), x ∈ y :: l → x ≤ a),
  foldr max ⊥ (y :: l) ≤ a
Tactic: induction l with
  | nil => simp
  | cons y l IH => simpa [h y mem_cons_self] using IH fun x hx => h x <| mem_cons_of_mem _ hx
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)
have cons : a ≤ foldr max ⊥ (x :: l)
Tactic: obtain hl | hl := hx
Cleared hypotheses: y, hx
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
hx : x ∈ y :: l
cons : a ≤ foldr max ⊥ (x :: l)
⊢ a ≤ foldr max ⊥ (y :: l)
have cons₁ : Mem x l → a ≤ foldr max ⊥ (y :: l)
Tactic: obtain hl | hl := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)
have cons : a ≤ max x (foldr max ⊥ l)
Tactic: simp only [foldr]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
a x : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max ⊥ l
have nil : ∀ (hx : Membership.mem (γ := List α) [] x), a ≤ foldr max ⊥ []
Tactic: induction l with
  | nil => exact absurd hx not_mem_nil
  | cons y l IH =>
    obtain hl | hl := hx
    · simp only [foldr]
      exact le_max_of_le_left h
    · exact le_max_of_le_right (IH (by assumption))
Cleared hypotheses: l, hx
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
l : List α
a x : α
hx : x ∈ l
h : a ≤ x
nil : ∀ (hx : Membership.mem (γ := List α) [] x), a ≤ foldr max ⊥ []
⊢ a ≤ foldr max ⊥ l
have cons : ∀ (y : α) (l : List α) (IH : ∀ (hx : x ∈ l), a ≤ foldr max ⊥ l) (hx : x ∈ y :: l), a ≤ foldr max ⊥ (y :: l)
Tactic: induction l with
  | nil => exact absurd hx not_mem_nil
  | cons y l IH =>
    obtain hl | hl := hx
    · simp only [foldr]
      exact le_max_of_le_left h
    · exact le_max_of_le_right (IH (by assumption))
Cleared hypotheses: l, hx
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ y :: l
⊢ a ≤ foldr max b (y :: l)
have cons : a ≤ max y (foldr max b l)
Tactic: simp only [List.foldr]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ y :: l
⊢ a ≤ max y (foldr max b l)
have cons : ∀ (hx : x ∈ x :: l), a ≤ max x (foldr max b l)
Tactic: obtain rfl | hl := mem_cons.mp hx
Cleared hypotheses: y, hx
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : ∀ (hx : x ∈ l), a ≤ foldr max b l
hx : x ∈ y :: l
cons : ∀ (hx : x ∈ x :: l), a ≤ max x (foldr max b l)
⊢ a ≤ max y (foldr max b l)
have cons₁ : ∀ (hl : x ∈ l), a ≤ max y (foldr max b l)
Tactic: obtain rfl | hl := mem_cons.mp hx
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a x b : α
hx : x ∈ l
h : a ≤ x
⊢ a ≤ foldr max b l
have nil : ∀ (hx : Membership.mem (γ := List α) [] x), a ≤ foldr max b []
Tactic: induction l with
  | nil => exact absurd hx List.not_mem_nil
  | cons y l IH =>
    simp only [List.foldr]
    obtain rfl | hl := mem_cons.mp hx
    · exact le_max_of_le_left h
    · exact le_max_of_le_right (IH hl)
Cleared hypotheses: l, hx
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a x b : α
hx : x ∈ l
h : a ≤ x
nil : ∀ (hx : Membership.mem (γ := List α) [] x), a ≤ foldr max b []
⊢ a ≤ foldr max b l
have cons : ∀ (y : α) (l : List α) (IH : ∀ (hx : x ∈ l), a ≤ foldr max b l) (hx : x ∈ y :: l), a ≤ foldr max b (y :: l)
Tactic: induction l with
  | nil => exact absurd hx List.not_mem_nil
  | cons y l IH =>
    simp only [List.foldr]
    obtain rfl | hl := mem_cons.mp hx
    · exact le_max_of_le_left h
    · exact le_max_of_le_right (IH hl)
Cleared hypotheses: l, hx
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (hd :: (tl ++ [a])) r = r.toListAppend (go f (hd :: (tl ++ [a])) #[])
have cons : go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (Array.push #[] hd))
Tactic: rw [modifyLast.go, modifyLast.go]
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
cons : go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (Array.push #[] hd))
⊢ go f (hd :: (tl ++ [a])) r = r.toListAppend (go f (hd :: (tl ++ [a])) #[])
have rw : tl ++ [a] = [] → False
Tactic: rw [modifyLast.go, modifyLast.go]
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ go f (tl ++ [a]) (r.push hd) = r.toListAppend (go f (tl ++ [a]) (Array.push #[] hd))
have cons : (r.push hd).toListAppend (go f (tl ++ [a]) #[]) =
  r.toListAppend ((Array.push #[] hd).toListAppend (go f (tl ++ [a]) #[]))
Tactic: rw [modifyLast.go_concat _ _ tl _, modifyLast.go_concat _ _ tl (Array.push #[] hd)]
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a : α
tl : List α
r : Array α
⊢ go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])
have nil : go f ([] ++ [a]) r = r.toListAppend (go f ([] ++ [a]) #[])
Tactic: cases tl with
  | nil =>
    simp only [nil_append, modifyLast.go]; rfl
  | cons hd tl =>
    simp only [cons_append]
    rw [modifyLast.go, modifyLast.go]
    case x_3 | x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
    rw [modifyLast.go_concat _ _ tl _, modifyLast.go_concat _ _ tl (Array.push #[] hd)]
    simp only [Array.toListAppend_eq, Array.toList_push, nil_append,
      append_assoc]
Cleared hypotheses: tl
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a : α
tl : List α
r : Array α
nil : go f ([] ++ [a]) r = r.toListAppend (go f ([] ++ [a]) #[])
⊢ go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])
have cons : ∀ (hd : α) (tl : List α), go f (hd :: tl ++ [a]) r = r.toListAppend (go f (hd :: tl ++ [a]) #[])
Tactic: cases tl with
  | nil =>
    simp only [nil_append, modifyLast.go]; rfl
  | cons hd tl =>
    simp only [cons_append]
    rw [modifyLast.go, modifyLast.go]
    case x_3 | x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
    rw [modifyLast.go_concat _ _ tl _, modifyLast.go_concat _ _ tl (Array.push #[] hd)]
    simp only [Array.toListAppend_eq, Array.toList_push, nil_append,
      append_assoc]
Cleared hypotheses: tl
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
⊢ modifyLast.go f (head :: (tl ++ [a])) #[] = head :: (tl ++ [f a])
have cons : modifyLast.go f (tl ++ [a]) (Array.push #[] head) = head :: (tl ++ [f a])
Tactic: rw [modifyLast.go]
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
cons : modifyLast.go f (tl ++ [a]) (Array.push #[] head) = head :: (tl ++ [f a])
⊢ modifyLast.go f (head :: (tl ++ [a])) #[] = head :: (tl ++ [f a])
have rw : tl ++ [a] = [] → False
Tactic: rw [modifyLast.go]
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a head : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (Array.push #[] head) = head :: (tl ++ [f a])
have cons : modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]
Tactic: rw [modifyLast.go_concat, Array.toListAppend_eq, Array.toList_push, List.toList_toArray,
      nil_append, cons_append, nil_append, cons_inj_right]
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a : α
l : List α
⊢ modifyLast f (l ++ [a]) = l ++ [f a]
have nil : modifyLast f ([] ++ [a]) = [] ++ [f a]
Tactic: cases l with
  | nil =>
    simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq]
  | cons _ tl =>
    simp only [cons_append, modifyLast]
    rw [modifyLast.go]
    case x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
    rw [modifyLast.go_concat, Array.toListAppend_eq, Array.toList_push, List.toList_toArray,
      nil_append, cons_append, nil_append, cons_inj_right]
    exact modifyLast_concat _ _ tl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
a : α
l : List α
nil : modifyLast f ([] ++ [a]) = [] ++ [f a]
⊢ modifyLast f (l ++ [a]) = l ++ [f a]
have cons : ∀ (head : α) (tl : List α), modifyLast f (head :: tl ++ [a]) = head :: tl ++ [f a]
Tactic: cases l with
  | nil =>
    simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq]
  | cons _ tl =>
    simp only [cons_append, modifyLast]
    rw [modifyLast.go]
    case x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
    rw [modifyLast.go_concat, Array.toListAppend_eq, Array.toList_push, List.toList_toArray,
      nil_append, cons_append, nil_append, cons_inj_right]
    exact modifyLast_concat _ _ tl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd hd' : α
tl' : List α
h : hd :: hd' :: tl' ≠ []
⊢ modifyLast f (l₁ ++ hd :: hd' :: tl') = l₁ ++ modifyLast f (hd :: hd' :: tl')
have rw : hd' :: tl' ≠ []
Tactic: rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)
have cons : [hd] ≠ [] → modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]
Tactic: cases tl with
    | nil => exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }
Cleared hypotheses: tl, h
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
l₁ : List α
hd : α
tl : List α
h : hd :: tl ≠ []
cons : [hd] ≠ [] → modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]
⊢ modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)
have cons₁ : ∀ (hd' : α) (tl' : List α),
  hd :: hd' :: tl' ≠ [] → modifyLast f (l₁ ++ hd :: hd' :: tl') = l₁ ++ modifyLast f (hd :: hd' :: tl')
Tactic: cases tl with
    | nil => exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }
Cleared hypotheses: tl, h
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
l₁ l₂ : List α
h : l₂ ≠ []
⊢ modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂
have nil : Ne.{u_1 + 1} (α := List α) [] [] → modifyLast f (l₁ ++ []) = l₁ ++ modifyLast f []
Tactic: cases l₂ with
  | nil => contradiction
  | cons hd tl =>
    cases tl with
    | nil => exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.ModifyLast (goal)
Goal:
α : Type u_1
f : α → α
l₁ l₂ : List α
h : l₂ ≠ []
nil : Ne.{u_1 + 1} (α := List α) [] [] → modifyLast f (l₁ ++ []) = l₁ ++ modifyLast f []
⊢ modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂
have cons : ∀ (hd : α) (tl : List α), hd :: tl ≠ [] → modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)
Tactic: cases l₂ with
  | nil => contradiction
  | cons hd tl =>
    cases tl with
    | nil => exact modifyLast_concat _ hd _
    | cons hd' tl' =>
      rw [append_cons, ← nil_append (hd :: hd' :: tl'), append_cons [], nil_append,
        modifyLast_append_of_right_ne_nil _ (l₁ ++ [hd]) (hd' :: tl') _,
        modifyLast_append_of_right_ne_nil _ [hd] (hd' :: tl') _,
        append_assoc]
      all_goals { exact cons_ne_nil _ _ }
Cleared hypotheses: l₂, h
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.fst + x.snd = n
have rcases : ∀ (x y : ℕ), (x, y) ∈ antidiagonal n ↔ (x, y).fst + (x, y).snd = n
Tactic: rcases x with ⟨x, y⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n x y : ℕ
⊢ (x, y) ∈ antidiagonal n ↔ (x, y).fst + (x, y).snd = n
have simp : x < n + 1 ∧ n - x = y ↔ x + y = n
Tactic: simp [antidiagonal]
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ (antidiagonal n).length = n + 1
have rw : length (α := ℕ × ℕ) (map (fun (i : ℕ) ↦ (i, n - i)) (range (n + 1))) = n + 1
Tactic: rw [antidiagonal, length_map, length_range]
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : length (α := ℕ × ℕ) (map (fun (i : ℕ) ↦ (i, n - i)) (range (n + 1))) = n + 1
⊢ (antidiagonal n).length = n + 1
have rw₁ : (range (n + 1)).length = n + 1
Tactic: rw [antidiagonal, length_map, length_range]
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
rw : length (α := ℕ × ℕ) (map (fun (i : ℕ) ↦ (i, n - i)) (range (n + 1))) = n + 1
rw₁ : (range (n + 1)).length = n + 1
⊢ (antidiagonal n).length = n + 1
have rw₂ : n + 1 = n + 1
Tactic: rw [antidiagonal, length_map, length_range]
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)
have simp : (0, n + 1) :: (Nat.succ 0, n) :: map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n) =
  (0, n + 1) :: (Nat.succ 0, n) :: map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n)
Tactic: simp only [antidiagonal, range_succ_eq_map, map_cons, Nat.add_succ_sub_one,
    Nat.add_zero, id, Nat.sub_zero, map_map, Prod.map_apply]
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ (0, n + 1) :: (Nat.succ 0, n) :: map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n) =
    (0, n + 1) :: (Nat.succ 0, n) :: map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n)
have apply : Eq (α := List (ℕ × ℕ)) (map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n))
  (map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n))
Tactic: apply congr rfl (congr rfl _)
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ Eq (α := List (ℕ × ℕ)) (map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n))
    (map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n))
have h : ∀ (i : ℕ) (a : ℕ × ℕ),
  getElem? (valid := fun (as : List (ℕ × ℕ)) (i : ℕ) ↦ i < as.length)
        (map ((fun (i : ℕ) ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n)) i =
      some a ↔
    getElem? (valid := fun (as : List (ℕ × ℕ)) (i : ℕ) ↦ i < as.length)
        (map (Prod.map Nat.succ id ∘ (fun (i : ℕ) ↦ (i, n - i)) ∘ Nat.succ) (range n)) i =
      some a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]
have rw : map (Prod.map id Nat.succ) ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)) ++ [(n + 1 + 1, 0)] =
  (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]
Tactic: rw [antidiagonal_succ', antidiagonal_succ]
-- Lean 4 proof step from Mathlib.Data.List.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ map Prod.swap (antidiagonal n) = (antidiagonal n).reverse
have rw : Eq (α := List (ℕ × ℕ)) (map (Prod.swap ∘ fun (i : ℕ) ↦ (i, n - i)) (range (n + 1)))
  (map ((fun (i : ℕ) ↦ (i, n - i)) ∘ fun (x : ℕ) ↦ 0 + (n + 1) - 1 - x) (range (n + 1)))
Tactic: rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ←
    range_eq_range', map_map]