awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop} (refl : motive b ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → ReflTransGen r a c → Prop
refl : motive c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ motive b ⋯

Tactic:
exact head hbc _ refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop} (refl : motive b ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → ReflTransGen r a c → Prop
refl : motive c ⋯
head : ∀ {a c_2 : α} (h' : r a c_2) (h : ReflTransGen r c_2 c), motive c_2 h → motive a ⋯
a_1 c_1 : α
⊢ ∀ (h' : r a_1 c_1) (h : ReflTransGen r c_1 b), motive c_1 ⋯ → motive a_1 ⋯

Tactic:
fun h1 h2 ↦ head h1 (h2.tail hbc)

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {motive : (a : α) → ReflTransGen r a b → Prop} (refl : motive b ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → ReflTransGen r a c → Prop
refl : motive c ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
exact fun h1 h2 ↦ head h1 (h2.tail hbc)
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b : α
motive : (a : α) → ReflTransGen r a b → Prop
a : α
h : ReflTransGen r a b
refl : motive b ⋯
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯
refl₁ :
  ∀ {motive : (a_1 : α) → ReflTransGen r a_1 a → Prop} (refl : motive a ⋯)
    (head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), motive c h → motive a_1 ⋯), motive a ⋯
tail :
  ∀ {b c : α} (a_1 : ReflTransGen r a b) (hbc : r b c)
    (ih :
      ∀ {motive : (a : α) → ReflTransGen r a b → Prop} (refl : motive b ⋯)
        (head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a ⋯), motive a a_1)
    {motive : (a : α) → ReflTransGen r a c → Prop} (refl : motive c ⋯)
    (head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), motive c_1 h → motive a ⋯), motive a ⋯
⊢ motive a h

Tactic:
induction h with
  | refl => exact refl
  | @tail b c _ hbc ih =>
  apply ih
  · exact head hbc _ refl
  · exact fun h1 h2 ↦ head h1 (h2.tail hbc)

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
refl : ∀ (a : α), motive (a := a) ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive (a := a) ⋯

Tactic:
refl a
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
refl : ∀ (a : α), motive (a := a) ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
⊢ motive (a := a) ⋯

Tactic:
exact refl a
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
refl : ∀ (a : α), motive (a := a) ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
b_1 c : α
hab : ReflTransGen r a b_1
hbc : r b_1 c
ih : motive hab
⊢ motive ⋯

Tactic:
trans hab (.single hbc) ih (single hbc)

Premises used: Relation.ReflTransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
refl : ∀ (a : α), motive (a := a) ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
b_1 c : α
hab : ReflTransGen r a b_1
hbc : r b_1 c
ih : motive hab
⊢ motive ⋯

Tactic:
exact trans hab (.single hbc) ih (single hbc)

Premises used: Relation.ReflTransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
refl : ∀ (a : α), motive (a := a) ⋯
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ → motive ⋯
refl₁ : motive (a := a) ⋯
tail : ∀ {b c : α} (hab : ReflTransGen r a b) (hbc : r b c) (ih : motive hab), motive ⋯
⊢ motive h

Tactic:
induction h with
  | refl => exact refl a
  | tail hab hbc ih => exact trans hab (.single hbc) ih (single hbc)

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
refl : b = b ∨ ∃ (c : α), r b c ∧ ReflTransGen r c b
head :
  ∀ {a c : α},
    r a c →
      ReflTransGen r c b →
        (c = b ∨ ∃ (c_1 : α), r c c_1 ∧ ReflTransGen r c_1 b) → a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b
⊢ a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b

Tactic:
induction h using Relation.ReflTransGen.head_induction_on
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ b = b ∨ ∃ (c : α), r b c ∧ ReflTransGen r c b

Tactic:
grind
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b a_1 c : α
h' : r a_1 c
h : ReflTransGen r c b
h_1 : c = b ∨ ∃ (c_1 : α), r c c_1 ∧ ReflTransGen r c_1 b
⊢ a_1 = b ∨ ∃ (c : α), r a_1 c ∧ ReflTransGen r c b

Tactic:
grind
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
mpr : (a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b) → ReflTransGen r a b
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b

Tactic:
use cases_head

Premises used: Relation.ReflTransGen.cases_head
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b

Tactic:
head hac hcb

Premises used: Relation.ReflTransGen.head
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b

Tactic:
exact head hac hcb

Premises used: Relation.ReflTransGen.head
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
⊢ ReflTransGen r a c ∨ ReflTransGen r c a

Tactic:
Or.inl ac

Premises used: Or.inl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
⊢ ReflTransGen r a c ∨ ReflTransGen r c a

Tactic:
exact Or.inl ac

Premises used: Or.inl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c ∨ ReflTransGen r c b_1
tail : ∀ (IH : ReflTransGen r b_1 c), ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
tail₁ : ∀ (IH : ReflTransGen r c b_1), ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1

Tactic:
rcases IH with (IH | IH)
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c
tail : ∀ (ac : ReflTransGen r a b_1) (IH : ReflTransGen r b_1 b_1), ReflTransGen r c_1 b_1 ∨ ReflTransGen r b_1 c_1
tail₁ : ∀ (e : α) (be : r b_1 e) (ec : ReflTransGen r e c), ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1

Tactic:
rcases cases_head IH with (rfl | ⟨e, be, ec⟩)

Premises used: Relation.ReflTransGen.cases_head, rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
U : Relator.RightUnique r
b_1 c : α
h : ReflTransGen r a b_1
bd : r b_1 c
ac : ReflTransGen r a b_1
IH : ReflTransGen r b_1 b_1
⊢ ReflTransGen r c b_1 ∨ ReflTransGen r b_1 c

Tactic:
Or.inr (single bd)

Premises used: Relation.ReflTransGen.single, Or.inr
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
U : Relator.RightUnique r
b_1 c : α
h : ReflTransGen r a b_1
bd : r b_1 c
ac : ReflTransGen r a b_1
IH : ReflTransGen r b_1 b_1
⊢ ReflTransGen r c b_1 ∨ ReflTransGen r b_1 c

Tactic:
exact Or.inr (single bd)

Premises used: Relation.ReflTransGen.single, Or.inr
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c
e : α
be : r b_1 e
ec : ReflTransGen r e c
⊢ r b_1 c_1

Tactic:
cases U bd be
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c
e : α
be : r b_1 e
ec : ReflTransGen r e c
be₁ : r b_1 c_1
⊢ ReflTransGen r c_1 c

Tactic:
cases U bd be
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c
be : r b_1 c_1
ec : ReflTransGen r c_1 c
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1

Tactic:
Or.inl ec

Premises used: Or.inl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r b_1 c
be : r b_1 c_1
ec : ReflTransGen r c_1 c
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1

Tactic:
exact Or.inl ec

Premises used: Or.inl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r c b_1
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1

Tactic:
Or.inr (IH.tail bd)

Premises used: Relation.ReflTransGen.tail, Or.inr
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b_1 c_1 : α
h : ReflTransGen r a b_1
bd : r b_1 c_1
IH : ReflTransGen r c b_1
⊢ ReflTransGen r c_1 c ∨ ReflTransGen r c c_1

Tactic:
exact Or.inr (IH.tail bd)

Premises used: Relation.ReflTransGen.tail, Or.inr
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ab : ReflTransGen r a b
ac : ReflTransGen r a c
refl : ReflTransGen r a c ∨ ReflTransGen r c a
tail :
  ∀ {b c_1 : α},
    ReflTransGen r a b →
      ∀ (bd : r b c_1) (IH : ReflTransGen r b c ∨ ReflTransGen r c b), ReflTransGen r c_1 c ∨ ReflTransGen r c c_1
⊢ ReflTransGen r b c ∨ ReflTransGen r c b

Tactic:
induction ab with
  | refl => exact Or.inl ac
  | tail _ bd IH =>
    rcases IH with (IH | IH)
    · rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
      · exact Or.inr (single bd)
      · cases U bd be
        exact Or.inl ec
    · exact Or.inr (IH.tail bd)

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail, Or.inl, rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 : α
h : r a b_1
⊢ ReflTransGen r a b_1

Tactic:
ReflTransGen.single h

Premises used: Relation.ReflTransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 : α
h : r a b_1
⊢ ReflTransGen r a b_1

Tactic:
exact ReflTransGen.single h

Premises used: Relation.ReflTransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 c : α
h : TransGen r a b_1
bc : r b_1 c
ab : ReflTransGen r a b_1
⊢ ReflTransGen r a c

Tactic:
ReflTransGen.tail ab bc

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 c : α
h : TransGen r a b_1
bc : r b_1 c
ab : ReflTransGen r a b_1
⊢ ReflTransGen r a c

Tactic:
exact ReflTransGen.tail ab bc

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : TransGen r a b
single : ∀ {b : α} (h : r a b), ReflTransGen r a b
tail : ∀ {b c : α}, TransGen r a b → ∀ (bc : r b c) (ab : ReflTransGen r a b), ReflTransGen r a c
⊢ ReflTransGen r a b

Tactic:
induction h with
  | single h => exact ReflTransGen.single h
  | tail _ bc ab => exact ReflTransGen.tail ab bc

Premises used: Relation.TransGen.tail, Relation.TransGen.single, Relation.ReflTransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
⊢ TransGen r a b

Tactic:
assumption
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
b_1 c_1 : α
h : ReflTransGen r b b_1
hcd : r b_1 c_1
hac : TransGen r a b_1
⊢ TransGen r a c_1

Tactic:
hac.tail hcd

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
b_1 c_1 : α
h : ReflTransGen r b b_1
hcd : r b_1 c_1
hac : TransGen r a b_1
⊢ TransGen r a c_1

Tactic:
exact hac.tail hcd

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
hbc : ReflTransGen r b c
refl : TransGen r a b
tail : ∀ {b_1 c : α}, ReflTransGen r b b_1 → ∀ (hcd : r b_1 c) (hac : TransGen r a b_1), TransGen r a c
⊢ TransGen r a c

Tactic:
induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd

Premises used: Relation.TransGen.tail, refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
hbc : ReflTransGen r b c
⊢ TransGen r a c

Tactic:
trans_left (single hab) hbc

Premises used: Relation.TransGen.trans_left, Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hbc : r a c
⊢ TransGen r a c

Tactic:
single hbc

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hbc : r a c
⊢ TransGen r a c

Tactic:
exact single hbc

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 c_1 : α
h : ReflTransGen r a b_1
hdb : r b_1 c_1
IH : ∀ {c : α} (hbc : r b_1 c), TransGen r a c
c : α
hbc : r c_1 c
⊢ TransGen r a c

Tactic:
tail (IH hdb) hbc

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 c_1 : α
h : ReflTransGen r a b_1
hdb : r b_1 c_1
IH : ∀ {c : α} (hbc : r b_1 c), TransGen r a c
c : α
hbc : r c_1 c
⊢ TransGen r a c

Tactic:
exact tail (IH hdb) hbc

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : r b c
refl : ∀ {c : α} (hbc : r a c), TransGen r a c
tail :
  ∀ {b c : α},
    ReflTransGen r a b →
      ∀ (hdb : r b c) (IH : ∀ {c : α} (hbc : r b c), TransGen r a c) {c_1 : α} (hbc : r c c_1), TransGen r a c_1
⊢ TransGen r a c

Tactic:
induction hab generalizing c with
  | refl => exact single hbc
  | tail _ hdb IH => exact tail (IH hdb) hbc

Premises used: Relation.TransGen.tail, Relation.TransGen.single, refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : r a b
hbc : TransGen r b c
⊢ TransGen r a c

Tactic:
head' hab hbc.to_reflTransGen

Premises used: Relation.TransGen.head', Relation.TransGen.to_reflTransGen
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b a b_1 : α
h : r a b_1
motive : (a : α) → TransGen r a b_1 → Prop
single : ∀ {a : α} (h : r a b_1), motive a ⋯
head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b_1), motive c h → motive a ⋯
⊢ motive a ⋯

Tactic:
single h
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b a b_1 : α
h : r a b_1
motive : (a : α) → TransGen r a b_1 → Prop
single : ∀ {a : α} (h : r a b_1), motive a ⋯
head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b_1), motive c h → motive a ⋯
⊢ motive a ⋯

Tactic:
exact single h
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop} (single : ∀ {a : α} (h : r a b), motive a ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
tail : ∀ {a : α} (h : r a b), motive a ⋯
tail₁ : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), motive c_1 ⋯ → motive a ⋯
⊢ motive a ⋯

Tactic:
apply h_ih
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop} (single : ∀ {a : α} (h : r a b), motive a ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
a_1 : α
⊢ ∀ (h : r a_1 b), motive a_1 ⋯

Tactic:
fun h ↦ head h (.single hbc) (single hbc)

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop} (single : ∀ {a : α} (h : r a b), motive a ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a : α} (h : r a b), motive a ⋯

Tactic:
exact fun h ↦ head h (.single hbc) (single hbc)

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop} (single : ∀ {a : α} (h : r a b), motive a ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_2 : α} (h' : r a c_2) (h : TransGen r c_2 c), motive c_2 h → motive a ⋯
a_1 c_1 : α
⊢ ∀ (h' : r a_1 c_1) (h : TransGen r c_1 b), motive c_1 ⋯ → motive a_1 ⋯

Tactic:
fun hab hbc ↦ head hab _

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b_1 a b c : α
h : TransGen r a b
hbc : r b c
h_ih :
  ∀ {motive : (a : α) → TransGen r a b → Prop} (single : ∀ {a : α} (h : r a b), motive a ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯), motive a h
motive : (a : α) → TransGen r a c → Prop
single : ∀ {a : α} (h : r a c), motive a ⋯
head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), motive c_1 ⋯ → motive a ⋯

Tactic:
exact fun hab hbc ↦ head hab _
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b : α
motive : (a : α) → TransGen r a b → Prop
a : α
h : TransGen r a b
single : ∀ {a : α} (h : r a b), motive a ⋯
head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯
single₁ :
  ∀ {b : α} (h : r a b) {motive : (a : α) → TransGen r a b → Prop} (single : ∀ {a : α} (h : r a b), motive a ⋯)
    (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯), motive a ⋯
tail :
  ∀ {b c : α} (a_1 : TransGen r a b) (hbc : r b c)
    (h_ih :
      ∀ {motive : (a : α) → TransGen r a b → Prop} (single : ∀ {a : α} (h : r a b), motive a ⋯)
        (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a ⋯), motive a a_1)
    {motive : (a : α) → TransGen r a c → Prop} (single : ∀ {a : α} (h : r a c), motive a ⋯)
    (head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a ⋯), motive a ⋯
⊢ motive a h

Tactic:
induction h with
  | single h => exact single h
  | @tail b c _ hbc h_ih =>
  apply h_ih
  · exact fun h ↦ head h (.single hbc) (single hbc)
  · exact fun hab hbc ↦ head hab _

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
b_1 : α
h : r a b_1
⊢ motive ⋯

Tactic:
single h
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
b_1 : α
h : r a b_1
⊢ motive ⋯

Tactic:
exact single h
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
b_1 c : α
hab : TransGen r a b_1
hbc : r b_1 c
h_ih : motive hab
⊢ motive ⋯

Tactic:
trans hab (.single hbc) h_ih (single hbc)

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
b_1 c : α
hab : TransGen r a b_1
hbc : r b_1 c
h_ih : motive hab
⊢ motive ⋯

Tactic:
exact trans hab (.single hbc) h_ih (single hbc)

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
motive : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
single : ∀ {a b : α} (h : r a b), motive ⋯
trans : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ → motive ⋯
single₁ : ∀ {b : α} (h : r a b), motive ⋯
tail : ∀ {b c : α} (hab : TransGen r a b) (hbc : r b c) (h_ih : motive hab), motive ⋯
⊢ motive h

Tactic:
induction h with
  | single h => exact single h
  | tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b_1 : α
hbc : r b b_1
⊢ TransGen r a b_1

Tactic:
tail' hab hbc

Premises used: Relation.TransGen.tail'
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b_1 : α
hbc : r b b_1
⊢ TransGen r a b_1

Tactic:
exact tail' hab hbc

Premises used: Relation.TransGen.tail'
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b_1 c_1 : α
h : TransGen r b b_1
hcd : r b_1 c_1
hac : TransGen r a b_1
⊢ TransGen r a c_1

Tactic:
hac.tail hcd

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
b_1 c_1 : α
h : TransGen r b b_1
hcd : r b_1 c_1
hac : TransGen r a b_1
⊢ TransGen r a c_1

Tactic:
exact hac.tail hcd

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : TransGen r b c
single : ∀ {b_1 : α} (hbc : r b b_1), TransGen r a b_1
tail : ∀ {b_1 c : α}, TransGen r b b_1 → ∀ (hcd : r b_1 c) (hac : TransGen r a b_1), TransGen r a c
⊢ TransGen r a c

Tactic:
induction hbc with
  | single hbc => exact tail' hab hbc
  | tail _ hcd hac => exact hac.tail hcd

Premises used: Relation.TransGen.tail, Relation.TransGen.single