awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
h : ¬Membership.mem (γ := List (List α)) [] []
⊢ IsChain R (flatten []) ↔
    (∀ (l : List α), Membership.mem (γ := List (List α)) [] l → IsChain R l) ∧
      IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) []

Tactic:
simp
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l : List α
h : ¬[] ∈ [l]
⊢ IsChain R [l].flatten ↔
    (∀ (l_1 : List α), l_1 ∈ [l] → IsChain R l_1) ∧
      IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) [l]

Tactic:
simp [flatten]

Premises used: List.flatten
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : ¬[] ∈ l₁ :: l₂ :: L
⊢ [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L

Tactic:
rw [mem_cons, not_or, ← Ne] at hL

Premises used: Ne, not_or, List.mem_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
rw :
  (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
⊢ IsChain R (l₁ :: l₂ :: L).flatten ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₁ :: l₂ :: L)

Tactic:
rw [flatten_cons, isChain_append, isChain_flatten hL.2, forall_mem_cons, isChain_cons_cons]

Premises used: List.isChain_append, List.isChain_cons_cons, And.right, List.forall_mem_cons, List.flatten_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ ¬[] ∈ l₂ :: L
⊢ [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L

Tactic:
rw [mem_cons, not_or, ← Ne] at hL

Premises used: Ne, not_or, List.mem_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
simp :
  (IsChain R l₁ ∧
      IsChain R l₂ ∧
        (∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L) ∧
            ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    IsChain R l₁ ∧
      IsChain R l₂ ∧
        (∀ (x : List α), x ∈ L → IsChain R x) ∧
          (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
            IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)
⊢ (IsChain R l₁ ∧
      ((IsChain R l₂ ∧ ∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)) ∧
        ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ (l₂ :: L).flatten.head? → R x y) ↔
    (∀ (l : List α), l ∈ l₁ :: l₂ :: L → IsChain R l) ∧
      (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
        IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
simp only [forall_mem_cons, and_assoc, flatten_cons, head?_append_of_ne_nil _ hL.2.1.symm]

Premises used: Ne.symm, And.right, And.left, List.forall_mem_cons, List.head?_append_of_ne_nil, List.flatten_cons, and_assoc
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (IsChain R l₁ ∧
      IsChain R l₂ ∧
        (∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L) ∧
            ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    IsChain R l₁ ∧
      IsChain R l₂ ∧
        (∀ (x : List α), x ∈ L → IsChain R x) ∧
          (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
            IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)

Premises used: Iff.rfl, and_comm, Iff.and
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
L : List (List α)
hL : [] ≠ l₁ ∧ [] ≠ l₂ ∧ ¬[] ∈ L
⊢ (IsChain R l₁ ∧
      IsChain R l₂ ∧
        (∀ (x : List α), x ∈ L → IsChain R x) ∧
          IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L) ∧
            ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    IsChain R l₁ ∧
      IsChain R l₂ ∧
        (∀ (x : List α), x ∈ L → IsChain R x) ∧
          (∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ∧
            IsChain (fun (l₁ l₂ : List α) ↦ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) (l₂ :: L)

Tactic:
exact Iff.rfl.and (Iff.rfl.and <| Iff.rfl.and and_comm)

Premises used: Iff.rfl, and_comm, Iff.and
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
p : α → Prop
r : { a : α // p a } → { a : α // p a } → Prop
h : ∀ (x : α), Membership.mem (γ := List α) [] x → p x
⊢ IsChain r (attachWith [] p h) ↔
    IsChain
      (fun (a b : α) ↦
        ∃ (ha : p a),
          ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
      []

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
p : α → Prop
r : { a : α // p a } → { a : α // p a } → Prop
head : α
tail : List α
tail_ih :
  ∀ (h : ∀ (x : α), x ∈ tail → p x),
    IsChain r (tail.attachWith p h) ↔
      IsChain
        (fun (a b : α) ↦
          ∃ (ha : p a),
            ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
        tail
h : ∀ (x : α), x ∈ head :: tail → p x
⊢ IsChain r ((head :: tail).attachWith p h) ↔
    IsChain
      (fun (a b : α) ↦
        ∃ (ha : p a),
          ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
      (head :: tail)

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
l : List α
p : α → Prop
h : ∀ (x : α), x ∈ l → p x
r : { a : α // p a } → { a : α // p a } → Prop
nil :
  ∀ (h : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
    IsChain r (attachWith [] p h) ↔
      IsChain
        (fun (a b : α) ↦
          ∃ (ha : p a),
            ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
        []
cons :
  ∀ (head : α) (tail : List α),
    (∀ (h : ∀ (x : α), x ∈ tail → p x),
        IsChain r (tail.attachWith p h) ↔
          IsChain
            (fun (a b : α) ↦
              ∃ (ha : p a),
                ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
            tail) →
      ∀ (h : ∀ (x : α), x ∈ head :: tail → p x),
        IsChain r ((head :: tail).attachWith p h) ↔
          IsChain
            (fun (a b : α) ↦
              ∃ (ha : p a),
                ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
            (head :: tail)
⊢ IsChain r (l.attachWith p h) ↔
    IsChain
      (fun (a b : α) ↦
        ∃ (ha : p a),
          ∃ (hb : p b), r (Subtype.mk (p := fun (a : α) ↦ p a) a ha) (Subtype.mk (p := fun (a : α) ↦ p a) b hb))
      l

Tactic:
induction l with grind +splitIndPred
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
l : List α
r : { a : α // a ∈ l } → { a : α // a ∈ l } → Prop
⊢ IsChain r l.attach ↔
    IsChain
      (fun (a b : α) ↦
        ∃ (ha : a ∈ l),
          ∃ (hb : b ∈ l), r (Subtype.mk (p := fun (a : α) ↦ a ∈ l) a ha) (Subtype.mk (p := fun (a : α) ↦ a ∈ l) b hb))
      l

Tactic:
isChain_attachWith fun _ ↦ id

Premises used: List.isChain_attachWith, id
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ (l : List α), IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
Relation.ReflTransGen.head_induction_on h ?_ ?_

Premises used: Relation.ReflTransGen.head_induction_on
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
refine_1 : ∃ (l : List α), IsChain r (b :: l) ∧ (b :: l).getLast ⋯ = b
refine_2 :
  ∀ {a c : α} (h' : r a c) (h : Relation.ReflTransGen r c b),
    (∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) →
      ∃ (l : List α), IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
⊢ ∃ (l : List α), IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
refine Relation.ReflTransGen.head_induction_on h ?_ ?_
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ (l : List α), IsChain r (b :: l) ∧ (b :: l).getLast ⋯ = b

Tactic:
⟨[], .singleton _, rfl⟩

Premises used: List.IsChain.singleton, And.intro, Exists.intro, rfl, List.nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ (l : List α), IsChain r (b :: l) ∧ (b :: l).getLast ⋯ = b

Tactic:
exact ⟨[], .singleton _, rfl⟩
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
refine_2 :
  Relation.ReflTransGen r d b →
    (∃ (l : List α), IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b) →
      ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
⊢ ∀ (h : Relation.ReflTransGen r d b),
    (∃ (l : List α), IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b) →
      ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
_
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h_1 : Relation.ReflTransGen r d b
ih : ∃ (l : List α), IsChain r (d :: l) ∧ (d :: l).getLast ⋯ = b
refine_2 :
  ∀ (l : List α) (hl₁ : IsChain r (d :: l)) (hl₂ : (d :: l).getLast ⋯ = b),
    ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b
⊢ ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := ih
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h_1 : Relation.ReflTransGen r d b
l : List α
hl₁ : IsChain r (d :: l)
hl₂ : (d :: l).getLast ⋯ = b
⊢ ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
⟨d :: l, .cons_cons e hl₁, ?_⟩

Premises used: List.IsChain.cons_cons, List.cons, And.intro, Exists.intro
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h_1 : Relation.ReflTransGen r d b
l : List α
hl₁ : IsChain r (d :: l)
hl₂ : (d :: l).getLast ⋯ = b
refine_2 : (c :: d :: l).getLast ⋯ = b
⊢ ∃ (l : List α), IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b

Tactic:
refine ⟨d :: l, .cons_cons e hl₁, ?_⟩
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h_1 : Relation.ReflTransGen r d b
l : List α
hl₁ : IsChain r (d :: l)
hl₂ : (d :: l).getLast ⋯ = b
refine_2 refine_2₁ refine_2₂ refine_2₃ : (d :: l).getLast ⋯ = b
⊢ (c :: d :: l).getLast ⋯ = b

Tactic:
rwa [getLast_cons_cons]

Premises used: List.getLast_cons_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
rcases :
  ∀ (l : List α),
    IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b →
      ∃ (l : List α), ∃ (hl : l ≠ []), IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b
⊢ ∃ (l : List α), ∃ (hl : l ≠ []), IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b

Tactic:
rcases exists_isChain_cons_of_relationReflTransGen h with ⟨l, _⟩

Premises used: List.exists_isChain_cons_of_relationReflTransGen
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
l : List α
h_1 : IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b
⊢ ∃ (l : List α), ∃ (hl : l ≠ []), IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
h : IsChain r []
initial : ∀ (lne : Ne.{u + 1} (α := List α) [] []), p (head [] lne)
⊢ ∀ (i : α), Membership.mem (γ := List α) [] i → p i

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x : α
h : IsChain r [x]
initial : ∀ (lne : [x] ≠ []), p ([x].head lne)
⊢ ∀ (i : α), i ∈ [x] → p i

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
x y : α
xs : List α
h_1 : ∀ (h : IsChain r xs) (initial : ∀ (lne : xs ≠ []), p (xs.head lne)) (i : α), i ∈ xs → p i
h_2 :
  ∀ (y : α) (h : IsChain r (y :: xs)) (initial : ∀ (lne : y :: xs ≠ []), p ((y :: xs).head lne)) (i : α),
    i ∈ y :: xs → p i
h : IsChain r (x :: y :: xs)
initial : ∀ (lne : x :: y :: xs ≠ []), p ((x :: y :: xs).head lne)
⊢ ∀ (i : α), i ∈ x :: y :: xs → p i

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : ∀ (lne : l ≠ []), p (l.head lne)
nil :
  ∀ (h : IsChain r []) (initial : ∀ (lne : Ne.{u + 1} (α := List α) [] []), p (head [] lne)) (i : α),
    Membership.mem (γ := List α) [] i → p i
singleton : ∀ (x : α) (h : IsChain r [x]) (initial : ∀ (lne : [x] ≠ []), p ([x].head lne)) (i : α), i ∈ [x] → p i
cons_cons :
  ∀ (x y : α) (xs : List α),
    (∀ (h : IsChain r xs) (initial : ∀ (lne : xs ≠ []), p (xs.head lne)) (i : α), i ∈ xs → p i) →
      (∀ (y : α) (h : IsChain r (y :: xs)) (initial : ∀ (lne : y :: xs ≠ []), p ((y :: xs).head lne)) (i : α),
          i ∈ y :: xs → p i) →
        ∀ (h : IsChain r (x :: y :: xs)) (initial : ∀ (lne : x :: y :: xs ≠ []), p ((x :: y :: xs).head lne)) (i : α),
          i ∈ x :: y :: xs → p i
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
induction l using twoStepInduction with grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a : α
p : α → Prop
l : List α
h : IsChain r (a :: l)
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : p a
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
fun _ hi =>
  h.induction _ _ carries (fun _ => initial) _ (mem_cons_of_mem _ hi)

Premises used: List.IsChain.induction, List.mem_cons_of_mem, List.cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : IsChain r (l ++ [b])
hb : (l ++ [b]).head ⋯ = a
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : p a
⊢ ∀ (i : α), i ∈ l ++ [b] → p i

Tactic:
h.induction _ _ carries (fun _ => hb ▸ initial)

Premises used: List.IsChain.induction, Eq.rec, Eq.symm
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : IsChain r (l ++ [b])
hb : (l ++ [b]).head ⋯ = a
carries : ∀ ⦃x y : α⦄, r x y → p x → p y
initial : p a
⊢ p b

Tactic:
(IsChain.concat_induction p l h hb carries initial) _ mem_concat_self

Premises used: List.IsChain.concat_induction, List.mem_concat_self
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
⊢ IsChain (flip (flip r)) l

Tactic:
have H : IsChain (flip (flip r)) l := h
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
H : IsChain (flip (flip r)) l
⊢ ∀ (initial : ∀ (lne : l.reverse ≠ []), p (l.reverse.head lne)) (i : α), i ∈ l.reverse → p i

Tactic:
replace H := (isChain_reverse.mpr H).induction _ _ (fun _ _ h ↦ carries h)
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
p : α → Prop
l : List α
h : IsChain r l
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : ∀ (lne : l ≠ []), p (l.getLast lne)
H : ∀ (initial : ∀ (lne : l.reverse ≠ []), p (l.reverse.head lne)) (i : α), i ∈ l.reverse → p i
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
b : α
p : α → Prop
l : List α
h : IsChain r (l ++ [b])
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
⊢ ∀ (i : α), i ∈ l → p i

Tactic:
fun _ hi =>
  h.backwards_induction _ _ carries (fun _ => getLast_concat ▸ final) _ (mem_append_left _ hi)

Premises used: List.getLast_concat, Eq.rec, List.mem_append_left, List.IsChain.backwards_induction, List.cons, Eq.symm, HAppend.hAppend, List.nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : IsChain r (a :: l)
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
⊢ ∀ (i : α), i ∈ a :: l → p i

Tactic:
h.backwards_induction _ _ carries (fun _ => hb ▸ final)

Premises used: Eq.rec, List.IsChain.backwards_induction, Eq.symm
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
p : α → Prop
l : List α
h : IsChain r (a :: l)
hb : (a :: l).getLast ⋯ = b
carries : ∀ ⦃x y : α⦄, r x y → p y → p x
final : p b
⊢ p a

Tactic:
(IsChain.backwards_cons_induction p l h hb carries final) _ mem_cons_self

Premises used: List.mem_cons_self, List.IsChain.backwards_cons_induction
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
l : List α
hl₁ : IsChain r l
hne : l ≠ []
⊢ Relation.ReflTransGen r (l.head hne) (l.getLast hne)

Tactic:
IsChain.induction (Relation.ReflTransGen r (head l hne) ·) l hl₁
  (fun _ _ h₁ h₂ => Trans.trans h₂ h₁) (fun _ => Relation.ReflTransGen.refl) _ (getLast_mem _)

Premises used: List.head, Trans.trans, List.IsChain.induction, Relation.ReflTransGen.refl, List.getLast_mem, Relation.ReflTransGen
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
r : α → α → Prop
a b : α
l : List α
hl₁ : IsChain r (a :: l)
hl₂ : (a :: l).getLast ⋯ = b
⊢ Relation.ReflTransGen r a b

Tactic:
IsChain.backwards_cons_induction_head _ l hl₁ hl₂ (fun _ _ => Relation.ReflTransGen.head)
  Relation.ReflTransGen.refl

Premises used: List.IsChain.backwards_cons_induction_head, Relation.ReflTransGen
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a : α
as : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: as)
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) []
hmas : [] ≤ as
⊢ IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]

Tactic:
grind
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a : α
as : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
cons : a > b
⊢ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: b :: bs)

Tactic:
apply hm.cons_cons

Premises used: List.IsChain.cons_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]
hmas : b :: bs ≤ []
⊢ b :: bs < []

Tactic:
simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas

Premises used: reduceCtorEq, le_iff_lt_or_eq, or_false
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]
hmas : b :: bs < []
⊢ a > b

Tactic:
(List.not_lt_nil _ hmas).elim

Premises used: False.elim, List.not_lt_nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]
hmas : b :: bs < []
⊢ a > b

Tactic:
exact (List.not_lt_nil _ hmas).elim

Premises used: False.elim, List.not_lt_nil
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)

Tactic:
rw [List.isChain_cons_cons] at ha

Premises used: List.isChain_cons_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: a' :: as)
hmas : b :: bs ≤ a' :: as
ha₁ : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
⊢ b :: bs ≤ a' :: as

Tactic:
rw [List.isChain_cons_cons] at ha

Premises used: List.isChain_cons_cons
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ a > b

Tactic:
lt_of_le_of_lt ?_ ha.1

Premises used: lt_of_le_of_lt, And.left
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs ≤ a' :: as
cons : b ≤ a'
⊢ a > b

Tactic:
refine lt_of_le_of_lt ?_ ha.1

Premises used: lt_of_le_of_lt, And.left
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs ≤ a' :: as
⊢ b :: bs < a' :: as ∨ b :: bs = a' :: as

Tactic:
rw [le_iff_lt_or_eq] at hmas

Premises used: le_iff_lt_or_eq
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as ∨ b :: bs = a' :: as
cons : ∀ (hmas : b :: bs < a' :: as), b ≤ a'
cons₁ : ∀ (hmas : b :: bs = a' :: as), b ≤ a'
⊢ b ≤ a'

Tactic:
rcases hmas with hmas | hmas
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ b ≤ a'

Tactic:
head_le_of_lt hmas

Premises used: List.head_le_of_lt
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs < a' :: as
⊢ b ≤ a'

Tactic:
exact head_le_of_lt hmas

Premises used: List.head_le_of_lt
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
a' : α
as : List α
ha : a > a' ∧ IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a' :: as)
hmas : b :: bs = a' :: as
⊢ b ≤ a'

Tactic:
simp_all only [List.cons.injEq, le_refl]

Premises used: le_refl, List.cons.injEq
-- Module: Mathlib.Data.List.Chain
Goal:
α : Type u
inst : LinearOrder α
a : α
as : List α
ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
cons : ∀ (ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) [a]) (hmas : b :: bs ≤ []), a > b
cons₁ :
  ∀ (a' : α) (as : List α) (ha : IsChain (fun (x1 x2 : α) ↦ x1 > x2) (a :: a' :: as)) (hmas : b :: bs ≤ a' :: as), a > b
⊢ a > b

Tactic:
cases as with
    | nil =>
      simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas
      exact (List.not_lt_nil _ hmas).elim
    | cons a' as =>
      rw [List.isChain_cons_cons] at ha
      refine lt_of_le_of_lt ?_ ha.1
      rw [le_iff_lt_or_eq] at hmas
      rcases hmas with hmas | hmas
      · exact head_le_of_lt hmas
      · simp_all only [List.cons.injEq, le_refl]

Premises used: reduceCtorEq, le_refl, False.elim, List.not_lt_nil, List.IsChain.cons, List.cons.injEq, List.isChain_cons_cons, le_iff_lt_or_eq, List.IsChain.nil, or_false