awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
U : Relator.RightUnique r
ab : ReflTransGen r a b
ac : ReflTransGen r a c
⊢ ReflTransGen r b c ∨ ReflTransGen r c b
have refl : ReflTransGen r a c ∨ ReflTransGen r c a
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)
Cleared hypotheses: ab
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
⊢ ReflTransGen r b c ∨ ReflTransGen r c b
have 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
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)
Cleared hypotheses: ab
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b
have single : ∀ {b : α} (h : r a b), ReflTransGen r a b
Tactic: induction h with
  | single h => exact ReflTransGen.single h
  | tail _ bc ab => exact ReflTransGen.tail ab bc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : TransGen r a b
single : ∀ {b : α} (h : r a b), ReflTransGen r a b
⊢ ReflTransGen r a b
have tail : ∀ {b c : α}, TransGen r a b → ∀ (bc : r b c) (ab : ReflTransGen r a b), ReflTransGen r a c
Tactic: induction h with
  | single h => exact ReflTransGen.single h
  | tail _ bc ab => exact ReflTransGen.tail ab bc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : TransGen r a b
hbc : ReflTransGen r b c
refl : TransGen r a b
⊢ TransGen r a c
have tail : ∀ {b_1 c : α}, ReflTransGen r b b_1 → ∀ (hcd : r b_1 c) (hac : TransGen r a b_1), TransGen r a c
Tactic: induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : r b c
⊢ TransGen r a c
have refl : ∀ {c : α} (hbc : r a c), TransGen r a c
Tactic: induction hab generalizing c with
  | refl => exact single hbc
  | tail _ hdb IH => exact tail (IH hdb) hbc
Cleared hypotheses: c, hab, hbc
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
⊢ TransGen r a c
have 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
Tactic: induction hab generalizing c with
  | refl => exact single hbc
  | tail _ hdb IH => exact tail (IH hdb) hbc
Cleared hypotheses: c, hab, hbc
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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 ⋯
⊢ motive a ⋯
have tail : ∀ {a : α} (h : r a b), motive a sorry
Tactic: apply h_ih
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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 ⋯
⊢ motive a ⋯
have tail₁ : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b), motive c_1 sorry → motive a sorry
Tactic: apply h_ih
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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 ⋯
⊢ motive a h
have single₁ : ∀ {b : α} (h : r a b) {motive : (a : α) → TransGen r a b → Prop} (single : ∀ {a : α} (h : r a b), motive a sorry)
  (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a sorry), motive a sorry
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 _
Cleared hypotheses: motive, h, single, head
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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 ⋯
⊢ motive a h
have 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 sorry)
      (head : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), motive c h → motive a sorry), motive a a_1)
  {motive : (a : α) → TransGen r a c → Prop} (single : ∀ {a : α} (h : r a c), motive a sorry)
  (head : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), motive c_1 h → motive a sorry), motive a sorry
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 _
Cleared hypotheses: motive, h, single, head
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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 ⋯
⊢ motive h
have single₁ : ∀ {b : α} (h : r a b), motive sorry
Tactic: induction h with
  | single h => exact single h
  | tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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 ⋯
⊢ motive h
have tail : ∀ {b c : α} (hab : TransGen r a b) (hbc : r b c) (h_ih : motive hab), motive sorry
Tactic: induction h with
  | single h => exact single h
  | tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
hab : ReflTransGen r a b
hbc : TransGen r b c
⊢ TransGen r a c
have single : ∀ {b_1 : α} (hbc : r b b_1), TransGen r a b_1
Tactic: induction hbc with
  | single hbc => exact tail' hab hbc
  | tail _ hcd hac => exact hac.tail hcd
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
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
⊢ TransGen r a c
have tail : ∀ {b_1 c : α}, TransGen r b b_1 → ∀ (hcd : r b_1 c) (hac : TransGen r a b_1), TransGen r a c
Tactic: induction hbc with
  | single hbc => exact tail' hab hbc
  | tail _ hcd hac => exact hac.tail hcd
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ (b : α), ReflTransGen r a b ∧ r b c
have refine : ∀ (h : TransGen r a c), ∃ (b : α), ReflTransGen r a b ∧ r b c
Tactic: refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ (b : α), ReflTransGen r a b ∧ r b c
have single : ∀ (hac : r a c), ∃ (b : α), ReflTransGen r a b ∧ r b c
Tactic: cases h with
  | single hac => exact ⟨_, by rfl, hac⟩
  | tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
h : TransGen r a c
single : ∀ (hac : r a c), ∃ (b : α), ReflTransGen r a b ∧ r b c
⊢ ∃ (b : α), ReflTransGen r a b ∧ r b c
have tail : ∀ {b : α} (hab : TransGen r a b) (hbc : r b c), ∃ (b : α), ReflTransGen r a b ∧ r b c
Tactic: cases h with
  | single hac => exact ⟨_, by rfl, hac⟩
  | tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ (b : α), r a b ∧ ReflTransGen r b c
have refine : ∀ (h : TransGen r a c), ∃ (b : α), r a b ∧ ReflTransGen r b c
Tactic: refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a c b c_1 : α
h : TransGen r a b
hbc : r b c_1
IH : ∃ (b_1 : α), r a b_1 ∧ ReflTransGen r b_1 b
⊢ ∃ (b : α), r a b ∧ ReflTransGen r b c_1
have tail : ∀ (d : α) (had : r a d) (hdb : ReflTransGen r d b), ∃ (b : α), r a b ∧ ReflTransGen r b c_1
Tactic: rcases IH with ⟨d, had, hdb⟩
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ (b : α), r a b ∧ ReflTransGen r b c
have single : ∀ {b : α} (hac : r a b), ∃ (b_1 : α), r a b_1 ∧ ReflTransGen r b_1 b
Tactic: induction h with
  | single hac => exact ⟨_, hac, by rfl⟩
  | tail _ hbc IH =>
  rcases IH with ⟨d, had, hdb⟩
  exact ⟨_, had, hdb.tail hbc⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
h : TransGen r a c
single : ∀ {b : α} (hac : r a b), ∃ (b_1 : α), r a b_1 ∧ ReflTransGen r b_1 b
⊢ ∃ (b : α), r a b ∧ ReflTransGen r b c
have tail : ∀ {b c : α},
  TransGen r a b →
    ∀ (hbc : r b c) (IH : ∃ (b_1 : α), r a b_1 ∧ ReflTransGen r b_1 b), ∃ (b : α), r a b ∧ ReflTransGen r b c
Tactic: induction h with
  | single hac => exact ⟨_, hac, by rfl⟩
  | tail _ hbc IH =>
  rcases IH with ⟨d, had, hdb⟩
  exact ⟨_, had, hdb.tail hbc⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
x y : α
h : TransGen r x y
⊢ TransGen r y x
have single : ∀ {b : α} (i : r x b), TransGen r b x
Tactic: induction h with
  | single i => exact .single (hr i)
  | tail _ h₁ h₂ => exact .head (hr h₁) h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
x y : α
h : TransGen r x y
single : ∀ {b : α} (i : r x b), TransGen r b x
⊢ TransGen r y x
have tail : ∀ {b c : α}, TransGen r x b → ∀ (h₁ : r b c) (h₂ : TransGen r b x), TransGen r c x
Tactic: induction h with
  | single i => exact .single (hr i)
  | tail _ h₁ h₂ => exact .head (hr h₁) h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
⊢ Eq.{max 1 u_1} (ReflGen r) r
have h : ∀ (x y : α), ReflGen r x y ↔ r x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
a b : α
h : TransGen r a b
⊢ r a b
have single : ∀ {b : α} (hc : r a b), r a b
Tactic: induction h with
      | single hc => exact hc
      | tail _ hcd hac => exact IsTrans.trans _ _ _ hac hcd
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
a b : α
h : TransGen r a b
single : ∀ {b : α} (hc : r a b), r a b
⊢ r a b
have tail : ∀ {b c : α}, TransGen r a b → ∀ (hcd : r b c) (hac : r a b), r a c
Tactic: induction h with
      | single hc => exact hc
      | tail _ hcd hac => exact IsTrans.trans _ _ _ hac hcd
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
hab : TransGen r a b
⊢ TransGen p (f a) (f b)
have single : ∀ {b : α} (hac : r a b), TransGen p (f a) (f b)
Tactic: induction hab with
  | single hac => exact TransGen.single (h a _ hac)
  | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
hab : TransGen r a b
single : ∀ {b : α} (hac : r a b), TransGen p (f a) (f b)
⊢ TransGen p (f a) (f b)
have tail : ∀ {b c : α}, TransGen r a b → ∀ (hcd : r b c) (hac : TransGen p (f a) (f b)), TransGen p (f a) (f c)
Tactic: induction hab with
  | single hac => exact TransGen.single (h a _ hac)
  | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : TransGen r b a
⊢ TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b
have single : ∀ {b_1 : α} (h : r b b_1), TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b_1 b
Tactic: induction h with
  | single h => exact TransGen.single h
  | tail _ hbc ih => exact ih.head hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : TransGen r b a
single : ∀ {b_1 : α} (h : r b b_1), TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b_1 b
⊢ TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b
have tail : ∀ {b_1 c : α},
  TransGen r b b_1 →
    ∀ (hbc : r b_1 c) (ih : TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b_1 b),
      TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) c b
Tactic: induction h with
  | single h => exact TransGen.single h
  | tail _ hbc ih => exact ih.head hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ ReflTransGen r a b ↔ b = a
have rw : (a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b) ↔ b = a
Tactic: rw [cases_head_iff]
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b
have refine_1 : ∀ (h : ReflTransGen r a b), b = a ∨ TransGen r a b
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
refine_1 : ∀ (h : ReflTransGen r a b), b = a ∨ TransGen r a b
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b
have refine_2 : ∀ (h : b = a ∨ TransGen r a b), ReflTransGen r a b
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b
have refine_1 : a = a ∨ TransGen r a a
Tactic: cases h with
    | refl => exact Or.inl rfl
    | tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
refine_1 : a = a ∨ TransGen r a a
⊢ b = a ∨ TransGen r a b
have refine_1₁ : ∀ {b_1 : α} (hac : ReflTransGen r a b_1) (hcb : r b_1 b), b = a ∨ TransGen r a b
Tactic: cases h with
    | refl => exact Or.inl rfl
    | tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b
have refine_2 : ReflTransGen r b b
Tactic: rcases h with (rfl | h)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
refine_2 : ReflTransGen r b b
⊢ ReflTransGen r a b
have refine_2₁ : ∀ (h : TransGen r a b), ReflTransGen r a b
Tactic: rcases h with (rfl | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : IsTrans α r
a b : α
h : ReflTransGen r a b
⊢ r a b
have refl : r a a
Tactic: induction h with
      | refl => exact refl a
      | tail _ h₂ IH => exact IsTrans.trans _ _ _ IH h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : IsTrans α r
a b : α
h : ReflTransGen r a b
refl : r a a
⊢ r a b
have tail : ∀ {b c : α}, ReflTransGen r a b → ∀ (h₂ : r b c) (IH : r a b), r a c
Tactic: induction h with
      | refl => exact refl a
      | tail _ h₂ IH => exact IsTrans.trans _ _ _ IH h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ReflTransGen r b a
⊢ ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b
have refl : ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b b
Tactic: induction h with
  | refl => rfl
  | tail _ hbc ih => exact ih.head hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ReflTransGen r b a
refl : ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b b
⊢ ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b
have tail : ∀ {b_1 c : α},
  ReflTransGen r b b_1 →
    ∀ (hbc : r b_1 c) (ih : ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b_1 b),
      ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) c b
Tactic: induction h with
  | refl => rfl
  | tail _ hbc ih => exact ih.head hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Eq.{max 1 u_1} (ReflGen (TransGen r)) (ReflTransGen r)
have h : ∀ (x y : α), ReflGen (TransGen r) x y ↔ ReflTransGen r x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
⊢ ReflGen (TransGen r) x y ↔ ReflTransGen r x y
have h : ReflGen (TransGen r) x y ↔ y = x ∨ TransGen r x y
Tactic: simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Eq.{max 1 u_1} (TransGen (ReflGen r)) (ReflTransGen r)
have h : ∀ (x y : α), TransGen (ReflGen r) x y ↔ ReflTransGen r x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
⊢ TransGen (ReflGen r) x y ↔ ReflTransGen r x y
have h : ∀ (h : TransGen (ReflGen r) x y), ReflTransGen r x y
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
h : ∀ (h : TransGen (ReflGen r) x y), ReflTransGen r x y
⊢ TransGen (ReflGen r) x y ↔ ReflTransGen r x y
have h₁ : ∀ (h : ReflTransGen r x y), TransGen (ReflGen r) x y
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y
have h₁ : ∀ (h : ReflTransGen r y y), TransGen (ReflGen r) y y
Tactic: obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
h₁ : ∀ (h : ReflTransGen r y y), TransGen (ReflGen r) y y
⊢ TransGen (ReflGen r) x y
have h₂ : ∀ (h : TransGen r x y), TransGen (ReflGen r) x y
Tactic: obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
⊢ Eq.{max 1 u_1} (ReflTransGen r) (TransGen r)
have rw : Eq.{max 1 u_1} (TransGen (ReflGen r)) (TransGen r)
Tactic: rw [← transGen_reflGen, reflGen_eq_self]
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
rw : Eq.{max 1 u_1} (TransGen (ReflGen r)) (TransGen r)
⊢ Eq.{max 1 u_1} (ReflTransGen r) (TransGen r)
have rw₁ : Eq.{max 1 u_1} (TransGen r) (TransGen r)
Tactic: rw [← transGen_reflGen, reflGen_eq_self]
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
⊢ Eq.{max 1 u_1} (ReflTransGen r) (ReflGen r)
have rw : Eq.{max 1 u_1} (ReflGen (TransGen r)) (ReflGen r)
Tactic: rw [← reflGen_transGen, transGen_eq_self]
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
rw : Eq.{max 1 u_1} (ReflGen (TransGen r)) (ReflGen r)
⊢ Eq.{max 1 u_1} (ReflTransGen r) (ReflGen r)
have rw₁ : Eq.{max 1 u_1} (ReflGen r) (ReflGen r)
Tactic: rw [← reflGen_transGen, transGen_eq_self]
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
h : EqvGen r a b
⊢ EqvGen p a b
have rel : ∀ (a b : α) (h : r a b), EqvGen p a b
Tactic: induction h with
  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
  | refl => exact EqvGen.refl _
  | symm a b _ ih => exact EqvGen.symm _ _ ih
  | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
h : EqvGen r a b
rel : ∀ (a b : α) (h : r a b), EqvGen p a b
⊢ EqvGen p a b
have refl : ∀ (x : α), EqvGen p x x
Tactic: induction h with
  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
  | refl => exact EqvGen.refl _
  | symm a b _ ih => exact EqvGen.symm _ _ ih
  | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
h : EqvGen r a b
rel : ∀ (a b : α) (h : r a b), EqvGen p a b
refl : ∀ (x : α), EqvGen p x x
⊢ EqvGen p a b
have symm : ∀ (a b : α), EqvGen r a b → ∀ (ih : EqvGen p a b), EqvGen p b a
Tactic: induction h with
  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
  | refl => exact EqvGen.refl _
  | symm a b _ ih => exact EqvGen.symm _ _ ih
  | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Logic.Relation (goal)
Goal:
α : Sort u_1
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
h : EqvGen r a b
rel : ∀ (a b : α) (h : r a b), EqvGen p a b
refl : ∀ (x : α), EqvGen p x x
symm : ∀ (a b : α), EqvGen r a b → ∀ (ih : EqvGen p a b), EqvGen p b a
⊢ EqvGen p a b
have trans : ∀ (a b c : α), EqvGen r a b → EqvGen r b c → ∀ (hab : EqvGen p a b) (hbc : EqvGen p b c), EqvGen p a c
Tactic: induction h with
  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
  | refl => exact EqvGen.refl _
  | symm a b _ ih => exact EqvGen.symm _ _ ih
  | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
Cleared hypotheses: h