awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  ∀ (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)
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)

Tactic:
simpa using h (i + 1) (j + 1) (k + 1) (by lia) (by lia) (by lia)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Triplewise
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)
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 ⋯)
            (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)),
    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 ⋯)
          (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)
⊢ 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)

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)

Premises used: List.head, List.triplewise_cons, List.length_cons, List.pairwise_iff_getElem, List.tail, List.cons, List.nil
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
⊢ 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:
grind [pairwise_cons]

Premises used: List.pairwise_cons
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
head : α
tail : List α
tail_ih :
  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:
grind [pairwise_cons]

Premises used: List.pairwise_cons
-- Module: Mathlib.Data.List.Triplewise
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) []
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))
⊢ 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₁

Tactic:
induction l₁ with grind [pairwise_cons]

Premises used: List.pairwise_cons
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p (reverse []) ↔ Triplewise (fun (a b c : α) ↦ p c b a) []

Tactic:
simp
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
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:
simp [triplewise_append, pairwise_reverse, triplewise_cons, ih, and_comm]

Premises used: List.triplewise_append, List.triplewise_cons, and_comm, List.pairwise_reverse
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
nil : Triplewise p (reverse []) ↔ Triplewise (fun (a b c : α) ↦ p c b a) []
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)
⊢ Triplewise p l.reverse ↔ Triplewise (fun (a b c : α) ↦ p c b a) l

Tactic:
induction l with
  | nil => simp
  | cons h t ih =>
    simp [triplewise_append, pairwise_reverse, triplewise_cons, ih, and_comm]

Premises used: List.triplewise_append, List.triplewise_cons, and_comm, List.cons, List.pairwise_reverse, List.nil
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
⊢ RightInverse (α := Prod.{u, u_1} (List α) (List β)) unzip (uncurry zip)

Tactic:
grind [zip_unzip]

Premises used: List.zip_unzip
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
l₁ : List α
rw : Eq (α := List (β × α)) (map Prod.swap []) (zip [] l₁)
⊢ Eq (α := List (β × α)) (map Prod.swap (l₁.zip [])) (zip [] l₁)

Tactic:
rw [zip_nil_right]

Premises used: List.zip_nil_right
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
l₁ : List α
⊢ Eq (α := List (β × α)) (map Prod.swap []) (zip [] l₁)

Tactic:
rfl
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
a : α
l₁ : List α
b : β
l₂ : List β
⊢ map Prod.swap ((a :: l₁).zip (b :: l₂)) = (b :: l₂).zip (a :: l₁)

Tactic:
simp only [zip_cons_cons, map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]

Premises used: List.map_cons, Prod.swap_prod_mk, List.zip_cons_cons
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
h : length.{u} (α := α) [] = length.{u_1} (α := β) []
⊢ Forall p (zipWith f [] []) ↔ Forall₂ (fun (x : α) (y : β) ↦ p (f x y)) [] []

Tactic:
simp
-- Module: Mathlib.Data.List.Zip
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
⊢ l₁.length = l₂.length

Tactic:
simp only [length_cons, succ_inj] at h

Premises used: Nat.succ_inj, List.length_cons
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f : α → β → γ
p : γ → Prop
a : α
l₁ : List α
b : β
l₂ : List β
h : l₁.length = l₂.length
⊢ Forall p (zipWith f (a :: l₁) (b :: l₂)) ↔ Forall₂ (fun (x : α) (y : β) ↦ p (f x y)) (a :: l₁) (b :: l₂)

Tactic:
simp [forall_zipWith h]
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
l : List (α × β)
simp : (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = (map Prod.fst l, map Prod.snd l).swap
⊢ (map Prod.swap l).unzip = l.unzip.swap

Tactic:
simp only [unzip_eq_map, map_map]

Premises used: List.map_map, List.unzip_eq_map
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
l : List (α × β)
⊢ (map (Prod.fst ∘ Prod.swap) l, map (Prod.snd ∘ Prod.swap) l) = (map Prod.fst l, map Prod.snd l).swap

Tactic:
rfl
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
⊢ zipWith f [] [] = zipWith g [] []

Tactic:
rfl
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
a : α
b : β
l₁ : List α
l₂ : List β
hfg : f a b = g a b
h : 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:
congr_arg₂ _ hfg ih

Premises used: List.zipWith, congr_arg₂
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
a : α
b : β
l₁ : List α
l₂ : List β
hfg : f a b = g a b
h : 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:
exact congr_arg₂ _ hfg ih

Premises used: congr_arg₂
-- Module: Mathlib.Data.List.Zip
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 [] []
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₂)
⊢ zipWith f la lb = zipWith g la lb

Tactic:
induction h with
  | nil => rfl
  | cons hfg _ ih => exact congr_arg₂ _ hfg ih

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
ε : Type u_4
f : α → α → β
inst : IsSymmOp f
⊢ IsSymmOp (zipWith f)

Tactic:
⟨fun _ _ => zipWith_comm_of_comm IsSymmOp.symm_op⟩

Premises used: IsSymmOp.symm_op, IsSymmOp.mk, List.zipWith_comm_of_comm
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
l : List α
⊢ l.revzip.length = l.length

Tactic:
simp only [revzip, length_zip, length_reverse, min_self]

Premises used: List.revzip, List.length_reverse, min_self, List.length_zip
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
l : List α
⊢ l.revzip.unzip = (l, l.reverse)

Tactic:
unzip_zip length_reverse.symm

Premises used: List.revzip, List.length_reverse, List.unzip_zip, Eq.symm
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
l : List α
rw : l.revzip.unzip.fst = l
rw₁ rw₂ : (l, l.reverse).fst = l
⊢ map Prod.fst l.revzip = l

Tactic:
rw [← unzip_fst, unzip_revzip]

Premises used: List.unzip_revzip, List.unzip_fst
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
l : List α
rw : l.revzip.unzip.snd = l.reverse
rw₁ rw₂ : (l, l.reverse).snd = l.reverse
⊢ map Prod.snd l.revzip = l.reverse

Tactic:
rw [← unzip_snd, unzip_revzip]

Premises used: List.unzip_revzip, List.unzip_snd
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
l : List α
rw : l.revzip.reverse.unzip.fst.zip l.revzip.reverse.unzip.snd = l.reverse.revzip
⊢ l.revzip.reverse = l.reverse.revzip

Tactic:
rw [← zip_unzip (revzip l).reverse]

Premises used: List.revzip, List.zip_unzip, List.reverse
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
l : List α
⊢ l.revzip.reverse.unzip.fst.zip l.revzip.reverse.unzip.snd = l.reverse.revzip

Tactic:
simp [unzip_eq_map, revzip, map_reverse, map_fst_zip, map_snd_zip]

Premises used: List.revzip, List.map_fst_zip, List.map_reverse, List.map_snd_zip, List.unzip_eq_map
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
l : List α
⊢ map Prod.swap l.revzip = l.reverse.revzip

Tactic:
simp [revzip]

Premises used: List.revzip
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
l init tail : List α
nil :
  ∀ {init tail : List α},
    Membership.mem (γ := List (List α × List α)) (zip (inits []) (tails [])) (init, tail) ↔ init ++ tail = []
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
⊢ (init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l

Tactic:
induction l generalizing init tail
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
init tail : List α
⊢ Membership.mem (γ := List (List α × List α)) (([], []) :: zip [] []) (init, tail) ↔ init ++ tail = []

Tactic:
simp
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
init tail : List α
⊢ Membership.mem (γ := List (List α × List α)) (([], []) :: zip [] []) (init, tail) ↔ init ++ tail = []

Tactic:
case nil => simp

Premises used: List.nil
-- Module: Mathlib.Data.List.Zip
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
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)
⊢ 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
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
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
⊢ 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:
rw [mem_cons, zip_map_left, mem_map, Prod.exists]

Premises used: List.zip_map_left, List.mem_cons, List.mem_map, Prod.exists
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
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)
⊢ 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:
rw [mem_cons, zip_map_left, mem_map, Prod.exists]

Premises used: List.zip_map_left, List.mem_cons, List.mem_map, Prod.exists
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl

Tactic:
simp
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
w w_1 : List α
h : (w, w_1) ∈ tl.inits.zip tl.tails
⊢ (fun (t : List α) ↦ hd :: t) w ++ id w_1 = hd :: tl

Tactic:
simp [ih.mp h]

Premises used: Iff.mp
-- Module: Mathlib.Data.List.Zip
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)
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)
⊢ 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:
rcases init with - | ⟨hd', tl'⟩
-- Module: Mathlib.Data.List.Zip
Goal:
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
⊢ [] ++ 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:
simp
-- Module: Mathlib.Data.List.Zip
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
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)
⊢ (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:
right
-- Module: Mathlib.Data.List.Zip
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
h₁ : (tl', tail) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (tl', tail) = (hd' :: tl', tail)
⊢ ∃ (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:
use tl', tail
-- Module: Mathlib.Data.List.Zip
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
⊢ (tl', tail) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun (t : List α) ↦ hd :: t) id (tl', tail) = (hd' :: tl', tail)

Tactic:
simp_all
-- Module: Mathlib.Data.Matrix.Action
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
A : Matrix n n R
v : n → R
⊢ A • v = A *ᵥ v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Action
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Semiring R
A : (Matrix n n R)ᵐᵒᵖ
v : n → R
⊢ A • v = v ᵥ* MulOpposite.unop A

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
l : Type u_1
m_1 : Type u_2
n_1 : 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
n : Type u_14
m : Type u_15
inst : Finite m
inst_1 : Finite n
α : Type u_16
inst_2 : Finite α
⊢ Finite (Matrix m n α)

Tactic:
inferInstanceAs (Finite (m → n → α))

Premises used: _private.0.Matrix.instFinite._proof_1
-- Module: Mathlib.Data.Matrix.Basic
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 : Semiring α
inst_1 : Finite α
⊢ IsStablyFiniteRing α

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, IsStablyFiniteRing.mk
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
⊢ Eq (α := (a : m → n → α) → Matrix m n α) (⇑(ofLinearEquiv R) : (a : m → n → α) → Matrix m n α)
    (⇑of : (a : m → n → α) → Matrix m n α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst : Semiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
⊢ Eq (α := (a : Matrix m n α) → m → n → α) (⇑(LinearEquiv.symm (ofLinearEquiv R)) : (a : Matrix m n α) → m → n → α)
    (⇑(Equiv.symm of) : (a : Matrix m n α) → m → n → α)

Tactic:
rfl

Premises used: Matrix, rfl
-- Module: Mathlib.Data.Matrix.Basic
Goal:
m : Type u_2
n : Type u_3
α : Type u_11
β : Type u_12
inst : AddCommMonoid α
i : m
j : n
s : Finset β
g : β → Matrix m n α
⊢ Eq.{u_11 + 1} (α := α) ((∑ c ∈ s, g c) i j) (∑ c ∈ s, g c i j)

Tactic:
(congr_fun (s.sum_apply i g) j).trans (s.sum_apply j _)

Premises used: Matrix, Finset.sum_apply, congr_fun, Eq.trans
-- Module: Mathlib.Data.Matrix.Basic
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)
neg : ∀ (hi : ¬i = j), LE.le.{u_11} (α := α) 0 (1 i j)
⊢ LE.le.{u_11} (α := α) 0 (1 i j)

Tactic:
by_cases hi : i = j
-- Module: Mathlib.Data.Matrix.Basic
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
pos : LE.le.{u_11} (α := α) 0 (1 i i)
⊢ LE.le.{u_11} (α := α) 0 (1 i j)

Tactic:
subst hi
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Preorder α
inst_4 : ZeroLEOneClass α
i : n
⊢ LE.le.{u_11} (α := α) 0 (1 i i)

Tactic:
simp
-- Module: Mathlib.Data.Matrix.Basic
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)

Tactic:
simp [hi]
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
inst_3 : Preorder α
inst_4 : ZeroLEOneClass α
i : n
⊢ LE.le (α := n → α) 0 (1 i)

Tactic:
zero_le_one_elem i

Premises used: Matrix.zero_le_one_elem
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : AddMonoid α
l : List (Matrix n n α)
⊢ l.sum.diag = (List.map diag l).sum

Tactic:
map_list_sum (diagAddMonoidHom n α) l

Premises used: Matrix.diag, List.sum, Matrix.diagAddMonoidHom, map_list_sum
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : AddCommMonoid α
s : Multiset (Matrix n n α)
⊢ s.sum.diag = (Multiset.map diag s).sum

Tactic:
map_multiset_sum (diagAddMonoidHom n α) s

Premises used: Multiset.sum, map_multiset_sum, Matrix.diag, Multiset.foldr, Matrix.diagAddMonoidHom
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
ι : Type u_14
inst : AddCommMonoid α
s : Finset ι
f : ι → Matrix n n α
⊢ Eq (α := (i : n) → α) (diag (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).diag)

Tactic:
map_sum (diagAddMonoidHom n α) f s

Premises used: Multiset.sum, Matrix.diag, Multiset.foldr, Matrix.diagAddMonoidHom, map_sum, Finset.sum
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : Fintype n
inst_2 : DecidableEq n
v : n → α
k : ℕ
⊢ diagonal v ^ k = diagonal (v ^ k)

Tactic:
(map_pow (diagonalRingHom n α) v k).symm

Premises used: Matrix.diagonalRingHom, map_pow, Eq.symm, Matrix.diagonal
-- Module: Mathlib.Data.Matrix.Basic
Goal:
n : Type u_3
α : Type u_11
inst : Semiring α
inst_1 : DecidableEq n
inst_2 : Fintype n
a : α
⊢ Eq (α := Matrix n n α) ((scalar n : (a : α) → Matrix n n α) a : Matrix n n α)
    (diagonal fun (x : n) ↦ a : Matrix n n α)

Tactic:
rfl

Premises used: Matrix.diagonal, rfl, ite