awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ (b : α), ReflTransGen r a b ∧ r b c

Tactic:
⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩

Premises used: Relation.TransGen.tail', _private.0.Relation.TransGen.tail'_iff.match_1, Relation.TransGen, Iff.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
refine : ∀ (h : TransGen r a c), ∃ (b : α), ReflTransGen r a b ∧ r b c
⊢ TransGen r a c ↔ ∃ (b : α), ReflTransGen r a b ∧ r b c

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
hac : r a c
⊢ ReflTransGen r a a

Tactic:
rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
hac : r a c
⊢ ∃ (b : α), ReflTransGen r a b ∧ r b c

Tactic:
exact ⟨_, by rfl, hac⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c b : α
hab : TransGen r a b
hbc : r b c
⊢ ∃ (b : α), ReflTransGen r a b ∧ r b c

Tactic:
⟨_, hab.to_reflTransGen, hbc⟩

Premises used: And.intro, Exists.intro, Relation.TransGen.to_reflTransGen
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c b : α
hab : TransGen r a b
hbc : r b c
⊢ ∃ (b : α), ReflTransGen r a b ∧ r b c

Tactic:
exact ⟨_, hab.to_reflTransGen, hbc⟩
-- Module: Mathlib.Logic.Relation
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
tail : ∀ {b : α} (hab : TransGen r a b) (hbc : r b c), ∃ (b : α), ReflTransGen r a b ∧ 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⟩

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

Tactic:
⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩

Premises used: _private.0.Relation.TransGen.head'_iff.match_1, Relation.TransGen.head', Relation.TransGen, Iff.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c : α
refine : ∀ (h : TransGen r a c), ∃ (b : α), r a b ∧ ReflTransGen r b c
⊢ TransGen r a c ↔ ∃ (b : α), r a b ∧ ReflTransGen r b c

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c b : α
hac : r a b
⊢ ReflTransGen r b b

Tactic:
rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c b : α
hac : r a b
⊢ ∃ (b_1 : α), r a b_1 ∧ ReflTransGen r b_1 b

Tactic:
exact ⟨_, hac, by rfl⟩
-- Module: Mathlib.Logic.Relation
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
tail : ∀ (d : α) (had : r a d) (hdb : ReflTransGen r d b), ∃ (b : α), r a b ∧ ReflTransGen r b c_1
⊢ ∃ (b : α), r a b ∧ ReflTransGen r b c_1

Tactic:
rcases IH with ⟨d, had, hdb⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c b c_1 : α
h : TransGen r a b
hbc : r b c_1
d : α
had : r a d
hdb : ReflTransGen r d b
⊢ ∃ (b : α), r a b ∧ ReflTransGen r b c_1

Tactic:
⟨_, had, hdb.tail hbc⟩

Premises used: And.intro, Relation.ReflTransGen.tail, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a c b c_1 : α
h : TransGen r a b
hbc : r b c_1
d : α
had : r a d
hdb : ReflTransGen r d b
⊢ ∃ (b : α), r a b ∧ ReflTransGen r b c_1

Tactic:
exact ⟨_, had, hdb.tail hbc⟩
-- Module: Mathlib.Logic.Relation
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
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
⊢ ∃ (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⟩

Premises used: Relation.TransGen.tail, Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
x y b : α
i : r x b
⊢ TransGen r b x

Tactic:
.single (hr i)

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
x y b : α
i : r x b
⊢ TransGen r b x

Tactic:
exact .single (hr i)
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
x y b c : α
h : TransGen r x b
h₁ : r b c
h₂ : TransGen r b x
⊢ TransGen r c x

Tactic:
.head (hr h₁) h₂

Premises used: Relation.TransGen.head
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
x y b c : α
h : TransGen r x b
h₁ : r b c
h₂ : TransGen r b x
⊢ TransGen r c x

Tactic:
exact .head (hr h₁) h₂
-- Module: Mathlib.Logic.Relation
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
tail : ∀ {b c : α}, TransGen r x b → ∀ (h₁ : r b c) (h₂ : TransGen r b x), TransGen r c x
⊢ TransGen r y x

Tactic:
induction h with
  | single i => exact .single (hr i)
  | tail _ h₁ h₂ => exact .head (hr h₁) h₂

Premises used: Relation.TransGen.tail, Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
h : ∀ (x y : α), ReflGen r x y ↔ r x y
⊢ Eq.{max 1 u_1} (ReflGen r) r

Tactic:
ext x y
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
x y : α
⊢ ReflGen r x y ↔ r x y

Tactic:
simpa only [reflGen_iff, or_iff_right_iff_imp] using fun h ↦ h ▸ refl y

Premises used: or_iff_right_iff_imp, Relation.reflGen_iff
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Refl (ReflGen r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r r' : α → α → Prop
inst : Std.Refl r'
h : ∀ (x y : α), r x y → r' x y
x y : α
hxy : ReflGen r x y
⊢ r' x y

Tactic:
simpa [reflGen_eq_self] using ReflGen.mono h hxy

Premises used: Relation.ReflGen.mono, Relation.reflGen_eq_self
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Eq.{max 1 u_1} (SymmGen (swap (φ := fun (a a_1 : α) ↦ Prop) r)) (SymmGen r)

Tactic:
funext₂ fun _ _ ↦ propext or_comm

Premises used: funext₂, propext, or_comm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
a b : α
r : α → α → Prop
⊢ SymmGen (swap (φ := fun (a a_1 : α) ↦ Prop) r) a b ↔ SymmGen r a b

Tactic:
or_comm

Premises used: or_comm, Relation.SymmGen
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ SymmGen r a b ↔ SymmGen r b a

Tactic:
or_comm

Premises used: or_comm, Relation.SymmGen
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Total r
a b : α
⊢ SymmGen r a b

Tactic:
Std.Total.total a b

Premises used: Std.Total.total, Relation.SymmGen
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a b c : α
⊢ IsTrans α (TransGen r)

Tactic:
⟨@TransGen.trans α r⟩

Premises used: IsTrans.mk, Relation.TransGen.trans
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
a b b_1 : α
hc : r a b_1
⊢ r a b_1

Tactic:
hc
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
a b b_1 : α
hc : r a b_1
⊢ r a b_1

Tactic:
exact hc
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
a b b_1 c : α
h : TransGen r a b_1
hcd : r b_1 c
hac : r a b_1
⊢ r a c

Tactic:
IsTrans.trans _ _ _ hac hcd

Premises used: IsTrans.trans
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
a b b_1 c : α
h : TransGen r a b_1
hcd : r b_1 c
hac : r a b_1
⊢ r a c

Tactic:
exact IsTrans.trans _ _ _ hac hcd

Premises used: IsTrans.trans
-- Module: Mathlib.Logic.Relation
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
tail : ∀ {b c : α}, TransGen r a b → ∀ (hcd : r b c) (hac : r a b), r a c
⊢ r a b

Tactic:
induction h with
      | single hc => exact hc
      | tail _ hcd hac => exact IsTrans.trans _ _ _ hac hcd
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ IsTrans α (TransGen r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Eq.{max 1 u_1} (TransGen (TransGen r)) (TransGen r)

Tactic:
transGen_eq_self

Premises used: Relation.transGen_eq_self
-- Module: Mathlib.Logic.Relation
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)
b_1 : α
hac : r a b_1
⊢ TransGen p (f a) (f b_1)

Tactic:
TransGen.single (h a _ hac)

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
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)
b_1 : α
hac : r a b_1
⊢ TransGen p (f a) (f b_1)

Tactic:
exact TransGen.single (h a _ hac)

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
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)
b_1 c : α
h_1 : TransGen r a b_1
hcd : r b_1 c
hac : TransGen p (f a) (f b_1)
⊢ TransGen p (f a) (f c)

Tactic:
TransGen.tail hac (h _ _ hcd)

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
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)
b_1 c : α
h_1 : TransGen r a b_1
hcd : r b_1 c
hac : TransGen p (f a) (f b_1)
⊢ TransGen p (f a) (f c)

Tactic:
exact TransGen.tail hac (h _ _ hcd)

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Logic.Relation
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)
tail : ∀ {b c : α}, TransGen r a b → ∀ (hcd : r b c) (hac : TransGen p (f a) (f b)), TransGen p (f a) (f c)
⊢ 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)

Premises used: Relation.TransGen.tail, Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → TransGen p (f a) (f b)
hab : TransGen r a b
⊢ TransGen p (f a) (f b)

Tactic:
simpa [transGen_eq_self] using hab.lift f h

Premises used: Relation.transGen_eq_self, Relation.TransGen.lift
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
p : α → α → Prop
⊢ (∀ (a b : α), r a b → TransGen p a b) → TransGen r a b → TransGen p a b

Tactic:
TransGen.lift' id

Premises used: id, Relation.TransGen.lift'
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
P : α → Prop
dc : ∀ {a b : α}, r a b → P b → P a
a b : α
h : TransGen r a b
⊢ P b → P a

Tactic:
h.head_induction_on dc fun hr _ hi ↦ dc hr ∘ hi

Premises used: Relation.TransGen.head_induction_on
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
p : α → α → Prop
⊢ (∀ (a b : α), r a b → p a b) → TransGen r a b → TransGen p a b

Tactic:
TransGen.lift id

Premises used: id, Relation.TransGen.lift
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r r' : α → α → Prop
inst : IsTrans α r'
h : ∀ (x y : α), r x y → r' x y
x y : α
hxy : TransGen r x y
⊢ r' x y

Tactic:
simpa [transGen_eq_self] using TransGen.mono h hxy

Premises used: Relation.TransGen.mono, Relation.transGen_eq_self
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 : α
h : r b b_1
⊢ TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b_1 b

Tactic:
TransGen.single h

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 : α
h : r b b_1
⊢ TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b_1 b

Tactic:
exact TransGen.single h

Premises used: Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 c : α
h : 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:
ih.head hbc

Premises used: Relation.TransGen.head
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 c : α
h : 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:
exact ih.head hbc
-- Module: Mathlib.Logic.Relation
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
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
⊢ TransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b

Tactic:
induction h with
  | single h => exact TransGen.single h
  | tail _ hbc ih => exact ih.head hbc

Premises used: Relation.TransGen.tail, Relation.TransGen.single
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ TransGen (swap (φ := fun (a a_1 : α) ↦ Prop) r) a b ↔ TransGen r b a

Tactic:
⟨TransGen.swap, TransGen.swap⟩

Premises used: Iff.intro, Relation.TransGen.swap
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
rw : (a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b) ↔ b = a
⊢ ReflTransGen r a b ↔ b = a

Tactic:
rw [cases_head_iff]

Premises used: Relation.ReflTransGen.cases_head_iff
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ (c : α), r a c ∧ ReflTransGen r c b) ↔ b = a

Tactic:
simp [h, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
refine_1 : ∀ (h : ReflTransGen r a b), b = a ∨ TransGen r a b
refine_2 : ∀ (h : b = a ∨ TransGen r a b), ReflTransGen r a b
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a : α
⊢ a = a ∨ TransGen r a a

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a : α
⊢ a = a ∨ TransGen r a a

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 : α
hac : ReflTransGen r a b_1
hcb : r b_1 b
⊢ b = a ∨ TransGen r a b

Tactic:
Or.inr (TransGen.tail' hac hcb)

Premises used: Relation.TransGen.tail', Or.inr
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 : α
hac : ReflTransGen r a b_1
hcb : r b_1 b
⊢ b = a ∨ TransGen r a b

Tactic:
exact Or.inr (TransGen.tail' hac hcb)

Premises used: Relation.TransGen.tail', Or.inr
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : ReflTransGen r a b
refine_1 : a = a ∨ TransGen r a a
refine_1₁ : ∀ {b_1 : α} (hac : ReflTransGen r a b_1) (hcb : r b_1 b), b = a ∨ TransGen r a 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)

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail, Or.inl, rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : b = a ∨ TransGen r a b
refine_2 : ReflTransGen r b b
refine_2₁ : ∀ (h : TransGen r a b), ReflTransGen r a b
⊢ ReflTransGen r a b

Tactic:
rcases h with (rfl | h)

Premises used: rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
b : α
⊢ ReflTransGen r b b

Tactic:
rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : TransGen r a b
⊢ ReflTransGen r a b

Tactic:
h.to_reflTransGen

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

Tactic:
exact h.to_reflTransGen

Premises used: Relation.TransGen.to_reflTransGen
-- Module: Mathlib.Logic.Relation
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 : ReflTransGen r a b
⊢ ReflTransGen p (f a) (f b)

Tactic:
ReflTransGen.trans_induction_on hab (fun _ ↦ refl) (ReflTransGen.single ∘ h _ _) fun _ _ ↦ trans

Premises used: Relation.ReflTransGen.trans_induction_on
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
p : α → α → Prop
⊢ (∀ (a b : α), r a b → p a b) → ReflTransGen r a b → ReflTransGen p a b

Tactic:
ReflTransGen.lift id

Premises used: Relation.ReflTransGen.lift, id
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : IsTrans α r
a b : α
⊢ r a a

Tactic:
refl a

Premises used: refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : IsTrans α r
a b : α
⊢ r a a

Tactic:
exact refl a

Premises used: refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : IsTrans α r
a b b_1 c : α
h : ReflTransGen r a b_1
h₂ : r b_1 c
IH : r a b_1
⊢ r a c

Tactic:
IsTrans.trans _ _ _ IH h₂

Premises used: IsTrans.trans
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : IsTrans α r
a b b_1 c : α
h : ReflTransGen r a b_1
h₂ : r b_1 c
IH : r a b_1
⊢ r a c

Tactic:
exact IsTrans.trans _ _ _ IH h₂

Premises used: IsTrans.trans
-- Module: Mathlib.Logic.Relation
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
tail : ∀ {b c : α}, ReflTransGen r a b → ∀ (h₂ : r b c) (IH : r a b), r a c
⊢ r a b

Tactic:
induction h with
      | refl => exact refl a
      | tail _ h₂ IH => exact IsTrans.trans _ _ _ IH h₂

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail, refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a b c : α
⊢ Std.Refl (ReflTransGen r)

Tactic:
⟨@ReflTransGen.refl α r⟩

Premises used: Std.Refl.mk, Relation.ReflTransGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Std.Refl (ReflTransGen r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
ε : Sort u_5
ζ : Sort u_6
r : α → α → Prop
a b c : α
⊢ IsTrans α (ReflTransGen r)

Tactic:
⟨@ReflTransGen.trans α r⟩

Premises used: IsTrans.mk, Relation.ReflTransGen.trans
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ IsTrans α (ReflTransGen r)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Eq.{max 1 u_1} (ReflTransGen (ReflTransGen r)) (ReflTransGen r)

Tactic:
reflTransGen_eq_self

Premises used: Relation.reflTransGen_eq_self
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
β : Sort u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → ReflTransGen p (f a) (f b)
hab : ReflTransGen r a b
⊢ ReflTransGen p (f a) (f b)

Tactic:
simpa [reflTransGen_eq_self] using hab.lift f h

Premises used: Relation.ReflTransGen.lift, Relation.reflTransGen_eq_self
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
p : α → α → Prop
⊢ (∀ (a b : α), r a b → ReflTransGen p a b) → ReflTransGen r a b → ReflTransGen p a b

Tactic:
ReflTransGen.lift' id

Premises used: id, Relation.ReflTransGen.lift'
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) b b

Tactic:
rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 c : α
h : 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:
ih.head hbc

Premises used: Relation.ReflTransGen.head
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b b_1 c : α
h : 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:
exact ih.head hbc
-- Module: Mathlib.Logic.Relation
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
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
⊢ ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b

Tactic:
induction h with
  | refl => rfl
  | tail _ hbc ih => exact ih.head hbc

Premises used: Relation.ReflTransGen.refl, Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
⊢ ReflTransGen (Function.swap (φ := fun (a a_1 : α) ↦ Prop) r) a b ↔ ReflTransGen r b a

Tactic:
⟨ReflTransGen.swap, ReflTransGen.swap⟩

Premises used: Relation.ReflTransGen.swap, Iff.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h : ∀ (x y : α), ReflGen (TransGen r) x y ↔ ReflTransGen r x y
⊢ Eq.{max 1 u_1} (ReflGen (TransGen r)) (ReflTransGen r)

Tactic:
ext x y
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
h : ReflGen (TransGen r) x y ↔ y = x ∨ TransGen r x y
⊢ ReflGen (TransGen r) x y ↔ ReflTransGen r x y

Tactic:
simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]

Premises used: Relation.reflTransGen_iff_eq_or_transGen, Relation.reflGen_iff
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h : ∀ (x y : α), TransGen (ReflGen r) x y ↔ ReflTransGen r x y
⊢ Eq.{max 1 u_1} (TransGen (ReflGen r)) (ReflTransGen r)

Tactic:
ext x y
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
⊢ TransGen (ReflGen r) x y ↔ ReflTransGen r x y

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
h : ∀ (h : TransGen (ReflGen r) x y), ReflTransGen r x y
h₁ : ∀ (h : ReflTransGen r x y), TransGen (ReflGen r) x y
⊢ TransGen (ReflGen r) x y ↔ ReflTransGen r x y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
h : TransGen (ReflGen r) x y
⊢ ReflTransGen r x y

Tactic:
simpa [reflTransGen_eq_self] using (h.mono fun _ _ ↦ ReflGen.to_reflTransGen).to_reflTransGen

Premises used: Relation.TransGen.mono, Relation.ReflGen.to_reflTransGen, Relation.reflTransGen_eq_self, Relation.TransGen.to_reflTransGen
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
h₁ : ∀ (h : ReflTransGen r y y), TransGen (ReflGen r) y y
h₂ : ∀ (h : TransGen r x y), TransGen (ReflGen r) x y
⊢ TransGen (ReflGen r) x y

Tactic:
obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h

Premises used: Relation.reflTransGen_iff_eq_or_transGen, Iff.mp, rfl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
y : α
h : ReflTransGen r y y
⊢ TransGen (ReflGen r) y y

Tactic:
.single .refl

Premises used: Relation.TransGen.single, Relation.ReflGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
y : α
h : ReflTransGen r y y
⊢ TransGen (ReflGen r) y y

Tactic:
exact .single .refl