awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih :
  Triplewise p tail ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail k hk)
⊢ ((∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length) (_hij : i < j),
        p head (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i _hi)
          (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j _hj)) ∧
      ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length),
        p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i ⋯)
          (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j ⋯)
          (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail k hk)) ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) i ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) j ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) k hk)
have cons : ((∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length) (_hij : i < j),
      p head (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i _hi)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j _hj)) ∧
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i sorry)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j sorry)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail k hk)) →
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1)
    (hh :
      ∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length) (_hij : i < j),
        p head (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i _hi)
          (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j _hj))
    (ht :
      ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length),
        p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i sorry)
          (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j sorry)
          (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail k hk)),
    p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) i sorry)
      (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) j sorry)
      (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) k hk)
Tactic: refine ⟨fun ⟨hh, ht⟩ i j k hij hjk hk ↦ ?_,
            fun h ↦ ⟨fun i j hi hj hij ↦ ?_, fun i j k hij hjk hk ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p l ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < l.length),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) l i ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) l j ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) l k hk)
have nil : Triplewise p [] ↔
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < length.{u_1} (α := α) []),
    p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] i sorry)
      (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] j sorry)
      (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] k hk)
Tactic: induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [triplewise_cons, length_cons, pairwise_iff_getElem, ih]
    refine ⟨fun ⟨hh, ht⟩ i j k hij hjk hk ↦ ?_,
            fun h ↦ ⟨fun i j hi hj hij ↦ ?_, fun i j k hij hjk hk ↦ ?_⟩⟩
    · grind
    · simpa using h 0 (i + 1) (j + 1) (by lia) (by lia) (by lia)
    · simpa using h (i + 1) (j + 1) (k + 1) (by lia) (by lia) (by lia)
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
nil :
  Triplewise p [] ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < length.{u_1} (α := α) []),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] i ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] j ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] k hk)
⊢ Triplewise p l ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < l.length),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) l i ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) l j ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) l k hk)
have cons : ∀ (head : α) (tail : List α)
  (ih :
    Triplewise p tail ↔
      ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length),
        p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i sorry)
          (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j sorry)
          (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail k hk)),
  Triplewise p (head :: tail) ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < (head :: tail).length),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) i sorry)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) j sorry)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) k hk)
Tactic: induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [triplewise_cons, length_cons, pairwise_iff_getElem, ih]
    refine ⟨fun ⟨hh, ht⟩ i j k hij hjk hk ↦ ?_,
            fun h ↦ ⟨fun i j hi hj hij ↦ ?_, fun i j k hij hjk hk ↦ ?_⟩⟩
    · grind
    · simpa using h 0 (i + 1) (j + 1) (by lia) (by lia) (by lia)
    · simpa using h (i + 1) (j + 1) (k + 1) (by lia) (by lia) (by lia)
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
⊢ Triplewise p (l₁ ++ l₂) ↔
    Triplewise p l₁ ∧
      Triplewise p l₂ ∧
        (∀ (a : α), a ∈ l₁ → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun (x y : α) ↦ p x y a) l₁
have nil : Triplewise p ([] ++ l₂) ↔
  Triplewise p [] ∧
    Triplewise p l₂ ∧
      (∀ (a : α), Membership.mem (γ := List α) [] a → Pairwise (p a) l₂) ∧
        ∀ (a : α), a ∈ l₂ → Pairwise (fun (x y : α) ↦ p x y a) []
Tactic: induction l₁ with grind [pairwise_cons]
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
nil :
  Triplewise p ([] ++ l₂) ↔
    Triplewise p [] ∧
      Triplewise p l₂ ∧
        (∀ (a : α), Membership.mem (γ := List α) [] a → Pairwise (p a) l₂) ∧
          ∀ (a : α), a ∈ l₂ → Pairwise (fun (x y : α) ↦ p x y a) []
⊢ Triplewise p (l₁ ++ l₂) ↔
    Triplewise p l₁ ∧
      Triplewise p l₂ ∧
        (∀ (a : α), a ∈ l₁ → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun (x y : α) ↦ p x y a) l₁
have cons : ∀ (head : α) (tail : List α),
  (Triplewise p (tail ++ l₂) ↔
      Triplewise p tail ∧
        Triplewise p l₂ ∧
          (∀ (a : α), a ∈ tail → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun (x y : α) ↦ p x y a) tail) →
    (Triplewise p (head :: tail ++ l₂) ↔
      Triplewise p (head :: tail) ∧
        Triplewise p l₂ ∧
          (∀ (a : α), a ∈ head :: tail → Pairwise (p a) l₂) ∧
            ∀ (a : α), a ∈ l₂ → Pairwise (fun (x y : α) ↦ p x y a) (head :: tail))
Tactic: induction l₁ with grind [pairwise_cons]
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p l.reverse ↔ Triplewise (fun (a b c : α) ↦ p c b a) l
have nil : Triplewise p (reverse []) ↔ Triplewise (fun (a b c : α) ↦ p c b a) []
Tactic: induction l with
  | nil => simp
  | cons h t ih =>
    simp [triplewise_append, pairwise_reverse, triplewise_cons, ih, and_comm]
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
nil : Triplewise p (reverse []) ↔ Triplewise (fun (a b c : α) ↦ p c b a) []
⊢ Triplewise p l.reverse ↔ Triplewise (fun (a b c : α) ↦ p c b a) l
have cons : ∀ (h : α) (t : List α) (ih : Triplewise p t.reverse ↔ Triplewise (fun (a b c : α) ↦ p c b a) t),
  Triplewise p (h :: t).reverse ↔ Triplewise (fun (a b c : α) ↦ p c b a) (h :: t)
Tactic: induction l with
  | nil => simp
  | cons h t ih =>
    simp [triplewise_append, pairwise_reverse, triplewise_cons, ih, and_comm]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
β : Type u_1
l₁ : List α
⊢ Eq (α := List (β × α)) (map Prod.swap (l₁.zip [])) (zip [] l₁)
have rw : Eq (α := List (β × α)) (map Prod.swap []) (zip [] l₁)
Tactic: rw [zip_nil_right]
-- Lean 4 proof step from Mathlib.Data.List.Zip (hypothesis)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : (a :: l₁).length = (b :: l₂).length
⊢ Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun (x : α) (y : β) ↦ p (f x y)) (a :: l₁) (b :: l₂)
have h₁ : l₁.length = l₂.length
Tactic: simp only [length_cons, succ_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
β : Type u_1
l : List (α × β)
⊢ (map Prod.swap l).unzip = l.unzip.swap
have simp : (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = (map Prod.fst l, map Prod.snd l).swap
Tactic: simp only [unzip_eq_map, map_map]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
h : Forall₂ (fun (a : α) (b : β) ↦ f a b = g a b) la lb
⊢ zipWith f la lb = zipWith g la lb
have nil : zipWith f [] [] = zipWith g [] []
Tactic: induction h with
  | nil => rfl
  | cons hfg _ ih => exact congr_arg₂ _ hfg ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
h : Forall₂ (fun (a : α) (b : β) ↦ f a b = g a b) la lb
nil : zipWith f [] [] = zipWith g [] []
⊢ zipWith f la lb = zipWith g la lb
have cons : ∀ {a : α} {b : β} {l₁ : List α} {l₂ : List β} (hfg : f a b = g a b),
  Forall₂ (fun (a : α) (b : β) ↦ f a b = g a b) l₁ l₂ →
    ∀ (ih : zipWith f l₁ l₂ = zipWith g l₁ l₂), zipWith f (a :: l₁) (b :: l₂) = zipWith g (a :: l₁) (b :: l₂)
Tactic: induction h with
  | nil => rfl
  | cons hfg _ ih => exact congr_arg₂ _ hfg ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
l : List α
⊢ map Prod.fst l.revzip = l
have rw : l.revzip.unzip.fst = l
Tactic: rw [← unzip_fst, unzip_revzip]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
l : List α
rw : l.revzip.unzip.fst = l
⊢ map Prod.fst l.revzip = l
have rw₁ : (l, l.reverse).fst = l
Tactic: rw [← unzip_fst, unzip_revzip]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
l : List α
⊢ map Prod.snd l.revzip = l.reverse
have rw : l.revzip.unzip.snd = l.reverse
Tactic: rw [← unzip_snd, unzip_revzip]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
l : List α
rw : l.revzip.unzip.snd = l.reverse
⊢ map Prod.snd l.revzip = l.reverse
have rw₁ : (l, l.reverse).snd = l.reverse
Tactic: rw [← unzip_snd, unzip_revzip]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
l : List α
⊢ l.revzip.reverse = l.reverse.revzip
have rw : l.revzip.reverse.unzip.fst.zip l.revzip.reverse.unzip.snd = l.reverse.revzip
Tactic: rw [← zip_unzip (revzip l).reverse]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
l init tail : List α
⊢ (init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l
have nil : ∀ {init tail : List α},
  Membership.mem (γ := List (List α × List α)) (zip (inits []) (tails [])) (init, tail) ↔ init ++ tail = []
Tactic: induction l generalizing init tail
Cleared hypotheses: l, init, tail
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
l init tail : List α
nil :
  ∀ {init tail : List α},
    Membership.mem (γ := List (List α × List α)) (zip (inits []) (tails [])) (init, tail) ↔ init ++ tail = []
⊢ (init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l
have cons : ∀ (head : α) (tail : List α),
  (∀ {init tail_1 : List α}, (init, tail_1) ∈ tail.inits.zip tail.tails ↔ init ++ tail_1 = tail) →
    ∀ {init tail_1 : List α},
      (init, tail_1) ∈ (head :: tail).inits.zip (head :: tail).tails ↔ init ++ tail_1 = head :: tail
Tactic: induction l generalizing init tail
Cleared hypotheses: l, init, tail
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ Membership.mem (γ := List (List α × List α))
      (([], hd :: tl) :: zip (map (fun (t : List α) ↦ hd :: t) tl.inits) tl.tails) (init, tail) ↔
    init ++ tail = hd :: tl
have mp : Membership.mem (γ := List (List α × List α))
    (([], hd :: tl) :: zip (map (fun (t : List α) ↦ hd :: t) tl.inits) tl.tails) (init, tail) →
  init ++ tail = hd :: tl
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
mp :
  Membership.mem (γ := List (List α × List α))
      (([], hd :: tl) :: zip (map (fun (t : List α) ↦ hd :: t) tl.inits) tl.tails) (init, tail) →
    init ++ tail = hd :: tl
⊢ Membership.mem (γ := List (List α × List α))
      (([], hd :: tl) :: zip (map (fun (t : List α) ↦ hd :: t) tl.inits) tl.tails) (init, tail) ↔
    init ++ tail = hd :: tl
have mpr : init ++ tail = hd :: tl →
  Membership.mem (γ := List (List α × List α))
    (([], hd :: tl) :: zip (map (fun (t : List α) ↦ hd :: t) tl.inits) tl.tails) (init, tail)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ Membership.mem (γ := List (List α × List α))
      (([], hd :: tl) :: zip (map (fun (t : List α) ↦ hd :: t) tl.inits) tl.tails) (init, tail) →
    init ++ tail = hd :: tl
have mp : ((init, tail) = ([], hd :: tl) ∨
    ∃ (a : List α),
      ∃ (b : List α), (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (a, b) = (init, tail)) →
  init ++ tail = hd :: tl
Tactic: rw [mem_cons, zip_map_left, mem_map, Prod.exists]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    Membership.mem (γ := List (List α × List α))
      (([], hd :: tl) :: zip (map (fun (t : List α) ↦ hd :: t) tl.inits) tl.tails) (init, tail)
have mpr : init ++ tail = hd :: tl →
  (init, tail) = ([], hd :: tl) ∨
    ∃ (a : List α),
      ∃ (b : List α), (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (a, b) = (init, tail)
Tactic: rw [mem_cons, zip_map_left, mem_map, Prod.exists]
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ (a : List α),
        ∃ (b : List α), (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (a, b) = (init, tail)
have mpr : [] ++ tail = hd :: tl →
  Eq (α := List α × List α) ([], tail) ([], hd :: tl) ∨
    ∃ (a : List α),
      ∃ (b : List α),
        (a, b) ∈ tl.inits.zip tl.tails ∧
          Eq (α := List α × List α) (Prod.map (fun (t : List α) ↦ hd :: t) id (a, b)) ([], tail)
Tactic: rcases init with - | ⟨hd', tl'⟩
Cleared hypotheses: init
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
mpr :
  [] ++ tail = hd :: tl →
    Eq (α := List α × List α) ([], tail) ([], hd :: tl) ∨
      ∃ (a : List α),
        ∃ (b : List α),
          (a, b) ∈ tl.inits.zip tl.tails ∧
            Eq (α := List α × List α) (Prod.map (fun (t : List α) ↦ hd :: t) id (a, b)) ([], tail)
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ (a : List α),
        ∃ (b : List α), (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (a, b) = (init, tail)
have mpr₁ : ∀ (hd' : α) (tl' : List α),
  hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ (a : List α),
        ∃ (b : List α),
          (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (a, b) = (hd' :: tl', tail)
Tactic: rcases init with - | ⟨hd', tl'⟩
Cleared hypotheses: init
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (hd' :: tl', tail) = ([], hd :: tl) ∨
    ∃ (a : List α),
      ∃ (b : List α),
        (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (a, b) = (hd' :: tl', tail)
have mpr : ∃ (a : List α),
  ∃ (b : List α), (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (a, b) = (hd' :: tl', tail)
Tactic: right
-- Lean 4 proof step from Mathlib.Data.List.Zip (goal)
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ ∃ (a : List α),
    ∃ (b : List α),
      (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (a, b) = (hd' :: tl', tail)
have h₁ : (tl', tail) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (tl', tail) = (hd' :: tl', tail)
Tactic: use tl', tail
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
n : Type u_3
α : Type u_11
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Preorder α
inst_4 : ZeroLEOneClass α
i j : n
⊢ LE.le.{u_11} (α := α) 0 (1 i j)
have pos : ∀ (hi : i = j), LE.le.{u_11} (α := α) 0 (1 i j)
Tactic: by_cases hi : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
n : Type u_3
α : Type u_11
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Preorder α
inst_4 : ZeroLEOneClass α
i j : n
pos : ∀ (hi : i = j), LE.le.{u_11} (α := α) 0 (1 i j)
⊢ LE.le.{u_11} (α := α) 0 (1 i j)
have neg : ∀ (hi : ¬i = j), LE.le.{u_11} (α := α) 0 (1 i j)
Tactic: by_cases hi : i = j
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
n : Type u_3
α : Type u_11
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Preorder α
inst_4 : ZeroLEOneClass α
i j : n
hi : i = j
⊢ LE.le.{u_11} (α := α) 0 (1 i j)
have pos : LE.le.{u_11} (α := α) 0 (1 i i)
Tactic: subst hi
Cleared hypotheses: j, hi
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : Fintype m
r : α
M : Matrix m n α
⊢ HMul.hMul (α := Matrix m m α) ((scalar m : (a : α) → Matrix m m α) r : Matrix m m α) M =
      HMul.hMul (β := Matrix n n α) M ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α) ↔
    r • M = MulOpposite.op r • M
have simp_rw : HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ r) M =
    HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ r) ↔
  r • M = MulOpposite.op r • M
Tactic: simp_rw [scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : Fintype m
r : α
M : Matrix m n α
simp_rw :
  HMul.hMul (α := Matrix m m α) (diagonal fun (x : m) ↦ r) M =
      HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ r) ↔
    r • M = MulOpposite.op r • M
⊢ HMul.hMul (α := Matrix m m α) ((scalar m : (a : α) → Matrix m m α) r : Matrix m m α) M =
      HMul.hMul (β := Matrix n n α) M ((scalar n : (a : α) → Matrix n n α) r : Matrix n n α) ↔
    r • M = MulOpposite.op r • M
have simp_rw₁ : r • M = HMul.hMul (β := Matrix n n α) M (diagonal fun (x : n) ↦ r) ↔ r • M = MulOpposite.op r • M
Tactic: simp_rw [scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Algebra R α
inst_6 : Algebra R β
r : R
x : Matrix n n α
⊢ r • x =
    HMul.hMul (α := Matrix n n α) ((RingHom.comp (scalar n) (algebraMap R α) : (a : R) → Matrix n n α) r : Matrix n n α)
      x
have a : ∀ (i j : n),
  (r • x) i j =
    HMul.hMul (α := Matrix n n α) ((RingHom.comp (scalar n) (algebraMap R α) : (a : R) → Matrix n n α) r : Matrix n n α)
      x i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommSemiring R
inst_3 : Semiring α
inst_4 : Semiring β
inst_5 : Algebra R α
inst_6 : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α : (a : R) → α) r) = (algebraMap R β : (a : R) → β) r
⊢ Eq (α := Matrix n n β) (map ((algebraMap R (Matrix n n α) : (a : R) → Matrix n n α) r) f)
    ((algebraMap R (Matrix n n β) : (a : R) → Matrix n n β) r)
have rw : Eq (α := Matrix n n β) (diagonal fun (m : n) ↦ f ((algebraMap R (n → α) : (a : R) → n → α) r m))
  (diagonal ((algebraMap R (n → β) : (a : R) → n → β) r))
Tactic: rw [algebraMap_eq_diagonal, algebraMap_eq_diagonal, diagonal_map hf]
-- Lean 4 proof step from Mathlib.Data.Matrix.Basic (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α_1 : Type u_11
β : Type u_12
γ : Type u_13
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : NonAssocSemiring α_1
inst_3 : NonAssocSemiring β
inst_4 : NonAssocSemiring γ
α : Type u_14
inst_5 : Mul α
inst_6 : AddCommMonoid α
x x_1 : Matrix.{u_2, u_2, u_14} m m αᵐᵒᵖ
⊢ unop (op ((x * x_1)ᵀ.map unop)) = unop (op (xᵀ.map unop) * op (x_1ᵀ.map unop))
have a : ∀ (i j : m), unop (op ((x * x_1)ᵀ.map unop)) i j = unop (op (xᵀ.map unop) * op (x_1ᵀ.map unop)) i j
Tactic: ext