awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
x y : α
mp :
  (∃ (i : ℕ),
      ∃ (h : i < l.length),
        ∃ (j : ℕ),
          ∃ (h_1 : j < l.length),
            ¬i = j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ = x ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯ = y) →
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y
mpr :
  (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧
        ¬x = y →
    ∃ (i : ℕ),
      ∃ (h : i < l.length),
        ∃ (j : ℕ),
          ∃ (h_1 : j < l.length),
            ¬i = j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ = x ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯ = y
⊢ (∃ (i : ℕ),
      ∃ (h : i < l.length),
        ∃ (j : ℕ),
          ∃ (h_1 : j < l.length),
            ¬i = j ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ = x ∧
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯ = y) ↔
    (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = x) ∧
      (∃ (i : ℕ), ∃ (h : i < l.length), getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h = y) ∧ ¬x = y

Tactic:
constructor
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hne : ¬i = j
⊢ (∃ (i_1 : ℕ),
      ∃ (h : i_1 < l.length),
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i_1 h =
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) ∧
    (∃ (i : ℕ),
        ∃ (h : i < l.length),
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h =
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯) ∧
      ¬getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ =
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯

Tactic:
⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, mt h.getElem_inj_iff.1 hne⟩

Premises used: List.Nodup.getElem_inj_iff, mt, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hne : ¬i = j
⊢ (∃ (i_1 : ℕ),
      ∃ (h : i_1 < l.length),
        getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i_1 h =
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯) ∧
    (∃ (i : ℕ),
        ∃ (h : i < l.length),
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i h =
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯) ∧
      ¬getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i ⋯ =
          getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j ⋯

Tactic:
exact ⟨⟨i, hi, rfl⟩, ⟨j, hj, rfl⟩, mt h.getElem_inj_iff.1 hne⟩
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hne :
  ¬getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
⊢ ∃ (i_1 : ℕ),
    ∃ (h : i_1 < l.length),
      ∃ (j_1 : ℕ),
        ∃ (h_1 : j_1 < l.length),
          ¬i_1 = j_1 ∧
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i_1 ⋯ =
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j_1 ⋯ =
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj

Tactic:
⟨i, hi, j, hj, mt h.getElem_inj_iff.2 hne, rfl, rfl⟩

Premises used: Iff.mpr, List.Nodup.getElem_inj_iff, mt, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hne :
  ¬getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
⊢ ∃ (i_1 : ℕ),
    ∃ (h : i_1 < l.length),
      ∃ (j_1 : ℕ),
        ∃ (h_1 : j_1 < l.length),
          ¬i_1 = j_1 ∧
            getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i_1 ⋯ =
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi ∧
              getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j_1 ⋯ =
                getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj

Tactic:
exact ⟨i, hi, j, hj, mt h.getElem_inj_iff.2 hne, rfl, rfl⟩
-- Module: Mathlib.Data.List.OffDiag
Goal:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map (Prod.map f f) l.offDiag = (map f l).offDiag

Tactic:
simp [offDiag, map_flatMap, zipIdx_map, flatMap_map, eraseIdx_map, Function.comp_def]

Premises used: List.offDiag, Function.comp_def, List.flatMap_map, List.zipIdx_map, List.map_flatMap, List.eraseIdx_map
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
H : Symmetric R
H₁ : ∀ (x : α), x ∈ l → R x x
H₂ rwa rwa₁ rwa₂ rwa₃ : Pairwise R l
⊢ Pairwise (flip R) l

Tactic:
rwa [H.flip_eq]

Premises used: Symmetric.flip_eq
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
H : Symmetric fun (x y : α) ↦ x ≠ y → R x y
H₁ : ∀ (x : α), x ∈ l → x ≠ x → R x x
H₂ : Pairwise (fun (x y : α) ↦ x ≠ y → R x y) l
⊢ ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b

Tactic:
apply Pairwise.forall_of_forall

Premises used: List.Pairwise.forall_of_forall
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Symmetric fun (x y : α) ↦ x ≠ y → R x y

Tactic:
fun a b h hne => hR (h hne.symm)

Premises used: Symmetric, Ne.symm
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Symmetric fun (x y : α) ↦ x ≠ y → R x y

Tactic:
exact fun a b h hne => hR (h hne.symm)
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

Tactic:
fun _ _ hx => (hx rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

Tactic:
exact fun _ _ hx => (hx rfl).elim
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
a b : α
h : R a b
h_1 : a ≠ b
⊢ R a b

Tactic:
h
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
a b : α
h : R a b
h_1 : a ≠ b
⊢ R a b

Tactic:
exact h
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hR : Symmetric R
hl : Pairwise R l
⊢ Pairwise (fun (x y : α) ↦ x ≠ y → R x y) l

Tactic:
exact hl.imp (@fun a b h _ => by exact h)

Premises used: List.Pairwise.imp
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
hl : Pairwise R l
hr : Symmetric R
⊢ Set.Pairwise {x : α | x ∈ l} R

Tactic:
hl.forall hr

Premises used: Set.Mem, setOf, Set.Pairwise, List.Pairwise.forall
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
rw : ∀ {a b : α}, [a, b] <+ l → R a b
⊢ Pairwise R l

Tactic:
rw [pairwise_iff_forall_sublist]

Premises used: List.pairwise_iff_forall_sublist
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : a = b
refl : ∀ (hab : [a, a] <+ l), R a a
⊢ R a b

Tactic:
cases heq
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a : α
hab : [a, a] <+ l
⊢ R a a

Tactic:
apply refl

Premises used: refl
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
a₁ : a ∈ l
a₂ : b ∈ l
a₃ : a ≠ b
⊢ R a b

Tactic:
apply h
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
a₁ : a ∈ [a, b]
⊢ a ∈ l

Tactic:
apply hab.subset

Premises used: List.Sublist.subset
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ [a, b]

Tactic:
simp
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
a₁ a₂ : a ∈ [a, b]
⊢ a ∈ l

Tactic:
try (apply hab.subset; simp)

Premises used: List.Sublist.subset
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
a₁ : b ∈ [a, b]
⊢ b ∈ l

Tactic:
apply hab.subset

Premises used: List.Sublist.subset
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ [a, b]

Tactic:
simp
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
a₁ a₂ : b ∈ [a, b]
⊢ b ∈ l

Tactic:
try (apply hab.subset; simp)

Premises used: List.Sublist.subset
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Tactic:
heq
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b

Tactic:
exact heq
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
inst : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
if : ∀ (heq : a = b), R a b
if₁ : ∀ (heq : ¬a = b), R a b
if₂ : ∀ (heq : a = b), R a b
if₃ if₄ : ∀ (heq : ¬a = b), R a b
⊢ R a b

Tactic:
if heq : a = b then
    cases heq; apply refl
  else
    apply h <;> try (apply hab.subset; simp)
    exact heq

Premises used: List.Sublist.subset, refl
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l.tail
⊢ R (l.head ⋯) a

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hhead : R (l.head ⋯) (l.head ⋯)
⊢ R (l.head ⋯) a

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
inst : Std.Refl R
h₁ : Pairwise R l
ha : a ∈ l
⊢ R (l.head ⋯) a

Tactic:
h₁.rel_head_of_rel_head_head ha (refl_of ..)

Premises used: refl_of, List.Pairwise.rel_head_of_rel_head_head
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise R l
ha : a ∈ l.dropLast
rw : ∀ (h : Pairwise (fun (b a : α) ↦ R a b) l.reverse) (ha : a ∈ l.dropLast), R a (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
rw [← pairwise_reverse] at h

Premises used: List.pairwise_reverse
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun (b a : α) ↦ R a b) l.reverse
ha : a ∈ l.dropLast
rw : R a (l.reverse.head ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
rw [getLast_eq_head_reverse]

Premises used: List.getLast_eq_head_reverse
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun (b a : α) ↦ R a b) l.reverse
ha : a ∈ l.dropLast
rwa : a ∈ l.dropLast.reverse
rwa₁ rwa₂ rwa₃ rwa₄ : a ∈ l.dropLast
⊢ a ∈ l.reverse.tail

Tactic:
rwa [tail_reverse, mem_reverse]

Premises used: List.tail_reverse, List.mem_reverse
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun (b a : α) ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ R a (l.reverse.head ⋯)

Tactic:
exact h.rel_head_tail (by rwa [tail_reverse, mem_reverse])

Premises used: List.Pairwise.rel_head_tail
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ a ∈ l.dropLast ∨ a = l.getLast ⋯

Tactic:
rw [← dropLast_concat_getLast (ne_nil_of_mem ha), mem_append, List.mem_singleton] at ha

Premises used: List.dropLast_concat_getLast, List.ne_nil_of_mem, List.mem_singleton, List.mem_append
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l
hlast : R (l.getLast ⋯) (l.getLast ⋯)
ha₁ : a ∈ l.dropLast ∨ a = l.getLast ⋯
⊢ R (l.getLast ⋯) (l.getLast ⋯)

Tactic:
rw [← dropLast_concat_getLast (ne_nil_of_mem ha), mem_append, List.mem_singleton] at ha

Premises used: List.dropLast_concat_getLast, List.ne_nil_of_mem, List.mem_singleton, List.mem_append
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha_1 : a ∈ l
ha : a ∈ l.dropLast ∨ a = l.getLast ⋯
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
ha.elim h₁.rel_dropLast_getLast (· ▸ hlast)

Premises used: List.Pairwise.rel_dropLast_getLast, Eq.rec, Or.elim, Eq.symm
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha_1 : a ∈ l
ha : a ∈ l.dropLast ∨ a = l.getLast ⋯
hlast : R (l.getLast ⋯) (l.getLast ⋯)
⊢ R a (l.getLast ⋯)

Tactic:
exact ha.elim h₁.rel_dropLast_getLast (· ▸ hlast)

Premises used: Or.elim
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
inst : Std.Refl R
h₁ : Pairwise R l
ha : a ∈ l
⊢ R a (l.getLast ⋯)

Tactic:
h₁.rel_getLast_of_rel_getLast_getLast ha (refl_of ..)

Premises used: refl_of, List.Pairwise.rel_getLast_of_rel_getLast_getLast
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
a : α
inst : Inhabited α
inst_1 : Std.Refl R
h : Pairwise R l
ha : a ∈ l
nil : ∀ (h : Pairwise R []) (ha : Membership.mem (γ := List α) [] a), R (head! []) a
cons : ∀ (head : α) (tail : List α) (h : Pairwise R (head :: tail)) (ha : a ∈ head :: tail), R (head :: tail).head! a
⊢ R l.head! a

Tactic:
cases l
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
a : α
inst : Inhabited α
inst_1 : Std.Refl R
h : Pairwise R []
ha : Membership.mem (γ := List α) [] a
⊢ R (head! []) a

Tactic:
contradiction
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
a : α
inst : Inhabited α
inst_1 : Std.Refl R
tail : List α
h : Pairwise R (a :: tail)
⊢ R (a :: tail).head! a

Tactic:
refl_of ..

Premises used: refl_of, List.head!
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
a : α
inst : Inhabited α
inst_1 : Std.Refl R
tail : List α
h : Pairwise R (a :: tail)
⊢ R (a :: tail).head! a

Tactic:
exact refl_of ..

Premises used: refl_of
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
a : α
inst : Inhabited α
inst_1 : Std.Refl R
head : α
tail : List α
h : Pairwise R (head :: tail)
h_1 : Mem a tail
⊢ a ∈ tail

Tactic:
assumption
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
a : α
inst : Inhabited α
inst_1 : Std.Refl R
head : α
tail : List α
h : Pairwise R (head :: tail)
h_1 : Mem a tail
⊢ R (head :: tail).head! a

Tactic:
exact rel_of_pairwise_cons h (by assumption)

Premises used: List.rel_of_pairwise_cons
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
a : α
inst : Inhabited α
inst_1 : Std.Refl R
head : α
tail : List α
h : Pairwise R (head :: tail)
ha : a ∈ head :: tail
cons : ∀ (h : Pairwise R (a :: tail)), R (a :: tail).head! a
cons₁ : Mem a tail → R (head :: tail).head! a
⊢ R (head :: tail).head! a

Tactic:
cases ha with
    | head => exact refl_of ..
    | tail => exact rel_of_pairwise_cons h (by assumption)

Premises used: List.head, refl_of, List.rel_of_pairwise_cons, List.Pairwise.tail
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
a : α
n : ℕ
inst : Std.Refl R
⊢ Pairwise R (replicate n a)

Tactic:
pairwise_replicate.mpr (Or.inr <| refl_of ..)

Premises used: Iff.mpr, refl_of, List.pairwise_replicate, Or.inr
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : IsTrans α R
l : List α
a b : α
simp_rw : IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)
⊢ Pairwise R (a :: b :: l) ↔ R a b ∧ Pairwise R (b :: l)

Tactic:
simp_rw [← isChain_iff_pairwise, isChain_cons_cons]

Premises used: List.isChain_cons_cons, List.isChain_iff_pairwise
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : IsTrans α R
l : List α
a b : α
simp_rw : R a b → Pairwise R (b :: l) → R a b ∧ Pairwise R (b :: l)
⊢ R a b → Pairwise R (b :: l) → Pairwise R (a :: b :: l)

Tactic:
simp_rw [pairwise_cons_cons_iff_of_trans]

Premises used: List.pairwise_cons_cons_iff_of_trans
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : IsTrans α R
l : List α
a b : α
⊢ R a b → Pairwise R (b :: l) → R a b ∧ Pairwise R (b :: l)

Tactic:
And.intro

Premises used: And.intro
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : IsTrans α R
l : List α
a b : α
⊢ R a b → Pairwise R (b :: l) → R a b ∧ Pairwise R (b :: l)

Tactic:
exact And.intro

Premises used: And.intro
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a < b
⊢ R (l.get a) (l.get b)

Tactic:
List.pairwise_iff_get.1 h _ _ hab

Premises used: List.pairwise_iff_get, Iff.mp
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
inl : ∀ (hab : a ≤ a), R (l.get a) (l.get a)
inr : ∀ (hlt : a < b), R (l.get a) (l.get b)
⊢ R (l.get a) (l.get b)

Tactic:
obtain rfl | hlt := Fin.eq_or_lt_of_le hab

Premises used: Fin.eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : Std.Refl R
l : List α
h : Pairwise R l
a : Fin l.length
hab : a ≤ a
⊢ R (l.get a) (l.get a)

Tactic:
refl _

Premises used: refl
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : Std.Refl R
l : List α
h : Pairwise R l
a b : Fin l.length
hab : a ≤ b
hlt : a < b
⊢ R (l.get a) (l.get b)

Tactic:
(pairwise_iff_get.1 h) _ _ hlt

Premises used: List.pairwise_iff_get, Iff.mp
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : Std.Refl R
l : List α
h : Pairwise R l
a : Fin l.length
hab : a ≤ a
⊢ R (l.get a) (l.get a)

Tactic:
exacts [refl _, (pairwise_iff_get.1 h) _ _ hlt]

Premises used: refl
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
l : List α
h_1 : Pairwise R l
a b : α
h : R a b
⊢ Decidable.decide (R a b) = true

Tactic:
simpa using h
-- Module: Mathlib.Data.List.Pairwise
Goal:
α : Type u_1
R : α → α → Prop
inst : DecidableRel R
l : List α
h : Pairwise R l
⊢ Pairwise (fun (a b : α) ↦ Decidable.decide (R a b) = true) l

Tactic:
refine h.imp fun {a b} h => by simpa using h

Premises used: List.Pairwise.imp
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
p : l.Palindrome
nil : Eq.{u_1 + 1} (α := List α) (reverse []) []
singleton : ∀ (x : α), [x].reverse = [x]
cons_concat : ∀ (x : α) {l : List α}, l.Palindrome → l.reverse = l → (x :: (l ++ [x])).reverse = x :: (l ++ [x])
⊢ l.reverse = l

Tactic:
induction p
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
⊢ Eq.{u_1 + 1} (α := List α) (reverse []) []

Tactic:
rfl

Premises used: List.reverseAux, List.reverse, rfl
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
⊢ Eq.{u_1 + 1} (α := List α) (reverse []) []

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
⊢ Eq.{u_1 + 1} (α := List α) (reverse []) []

Tactic:
try (exact rfl)

Premises used: rfl
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
x : α
⊢ [x].reverse = [x]

Tactic:
rfl

Premises used: List.reverseAux, List.reverse, rfl
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
x : α
⊢ [x].reverse = [x]

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
x : α
⊢ [x].reverse = [x]

Tactic:
try (exact rfl)

Premises used: rfl
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
x : α
l_1 : List α
h : l_1.Palindrome
a_ih : l_1.reverse = l_1
⊢ (x :: (l_1 ++ [x])).reverse = x :: (l_1 ++ [x])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
x : α
l_1 : List α
h : l_1.Palindrome
a_ih : l_1.reverse = l_1
⊢ (x :: (l_1 ++ [x])).reverse = x :: (l_1 ++ [x])

Tactic:
simpa
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
⊢ l.reverse = l → l.Palindrome

Tactic:
bidirectionalRecOn l (fun _ => Palindrome.nil) (fun a _ => Palindrome.singleton a) ?_

Premises used: List.bidirectionalRecOn
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
refine :
  ∀ (a : α) (l : List α) (b : α),
    (l.reverse = l → l.Palindrome) → (a :: (l ++ [b])).reverse = a :: (l ++ [b]) → (a :: (l ++ [b])).Palindrome
⊢ l.reverse = l → l.Palindrome

Tactic:
refine bidirectionalRecOn l (fun _ => Palindrome.nil) (fun a _ => Palindrome.singleton a) ?_
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : (x :: (l ++ [y])).reverse = x :: (l ++ [y])
⊢ [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])

Tactic:
rw [reverse_cons, reverse_append] at hr

Premises used: List.reverse_cons, List.reverse_append
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
rw : (x :: (l ++ [x])).Palindrome
⊢ (x :: (l ++ [y])).Palindrome

Tactic:
rw [head_eq_of_cons_eq hr]

Premises used: List.head_eq_of_cons_eq
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
⊢ l.Palindrome

Tactic:
have : Palindrome l := hp (append_inj_left' (tail_eq_of_cons_eq hr) rfl)
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
this : l.Palindrome
⊢ (x :: (l ++ [x])).Palindrome

Tactic:
Palindrome.cons_concat x this

Premises used: List.Palindrome.cons_concat
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l_1 : List α
x : α
l : List α
y : α
hp : l.reverse = l → l.Palindrome
hr : [y].reverse ++ l.reverse ++ [x] = x :: (l ++ [y])
this : l.Palindrome
⊢ (x :: (l ++ [x])).Palindrome

Tactic:
exact Palindrome.cons_concat x this

Premises used: List.Palindrome.cons_concat
-- Module: Mathlib.Data.List.Palindrome
Goal:
α : Type u_1
l : List α
⊢ l.Palindrome ↔ l.reverse = l

Tactic:
Iff.intro reverse_eq of_reverse_eq

Premises used: List.Palindrome.of_reverse_eq, List.Palindrome.reverse_eq, Iff.intro