awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
x y : α
h_1 : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
TransGen.mono (fun _ _ ↦ .single) h

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

Tactic:
exact TransGen.mono (fun _ _ ↦ .single) h

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

Tactic:
simp only [← transGen_reflGen, reflGen_eq_self]

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

Tactic:
simp only [← reflGen_transGen, transGen_eq_self]

Premises used: Relation.reflGen_transGen, Relation.transGen_eq_self
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
rw : Eq.{max 1 u_1} (TransGen (ReflGen r)) (TransGen r)
rw₁ rw₂ : Eq.{max 1 u_1} (TransGen r) (TransGen r)
⊢ Eq.{max 1 u_1} (ReflTransGen r) (TransGen r)

Tactic:
rw [← transGen_reflGen, reflGen_eq_self]

Premises used: Relation.transGen_reflGen, Relation.reflGen_eq_self
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
rw : Eq.{max 1 u_1} (ReflGen (TransGen r)) (ReflGen r)
rw₁ rw₂ : Eq.{max 1 u_1} (ReflGen r) (ReflGen r)
⊢ Eq.{max 1 u_1} (ReflTransGen r) (ReflGen r)

Tactic:
rw [← reflGen_transGen, transGen_eq_self]

Premises used: Relation.reflGen_transGen, Relation.transGen_eq_self
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Equivalence (EqvGen r)

Tactic:
Equivalence.mk EqvGen.refl (EqvGen.symm _ _) (EqvGen.trans _ _ _)

Premises used: Relation.EqvGen.trans, Relation.EqvGen.refl, Equivalence.mk, Relation.EqvGen.symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
a_1 b_1 : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
h : r a b
⊢ EqvGen p a b

Tactic:
EqvGen.rel _ _ (hrp _ _ h)

Premises used: Relation.EqvGen.rel
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
a_1 b_1 : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
h : r a b
⊢ EqvGen p a b

Tactic:
exact EqvGen.rel _ _ (hrp _ _ h)

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

Tactic:
EqvGen.refl _

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

Tactic:
exact EqvGen.refl _

Premises used: Relation.EqvGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
a_1 b_1 : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
h : EqvGen r a b
ih : EqvGen p a b
⊢ EqvGen p b a

Tactic:
EqvGen.symm _ _ ih

Premises used: Relation.EqvGen.symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
a_1 b_1 : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
h : EqvGen r a b
ih : EqvGen p a b
⊢ EqvGen p b a

Tactic:
exact EqvGen.symm _ _ ih

Premises used: Relation.EqvGen.symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
a_1 b_1 : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b c : α
h : EqvGen r a b
h_1 : EqvGen r b c
hab : EqvGen p a b
hbc : EqvGen p b c
⊢ EqvGen p a c

Tactic:
EqvGen.trans _ _ _ hab hbc

Premises used: Relation.EqvGen.trans
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
a_1 b_1 : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b c : α
h : EqvGen r a b
h_1 : EqvGen r b c
hab : EqvGen p a b
hbc : EqvGen p b c
⊢ EqvGen p a c

Tactic:
exact EqvGen.trans _ _ _ hab hbc

Premises used: Relation.EqvGen.trans
-- Module: Mathlib.Logic.Relation
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
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
⊢ 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

Premises used: Relation.EqvGen.trans, Relation.EqvGen.refl, Relation.EqvGen.rel, Relation.EqvGen.symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) a c

Tactic:
⟨c, hac, refl⟩

Premises used: Relation.ReflTransGen.refl, Relation.Join, And.intro, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
⊢ Join (ReflTransGen r) a c

Tactic:
exact ⟨c, hac, refl⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
ih : Join (ReflTransGen r) d c
tail : ∀ (b : α) (hdb : ReflTransGen r d b) (hcb : ReflTransGen r c b), Join (ReflTransGen r) e c
⊢ Join (ReflTransGen r) e c

Tactic:
rcases ih with ⟨b, hdb, hcb⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r d a

Tactic:
⟨e, refl, ReflGen.single hde⟩

Premises used: Relation.ReflTransGen.refl, Relation.ReflGen.single, And.intro, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r d a

Tactic:
exact ⟨e, refl, ReflGen.single hde⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
ih : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r f a
tail : ∀ (a : α) (hea : ReflTransGen r e a) (hfa : ReflGen r f a), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
rcases ih with ⟨a, hea, hfa⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
hea : ReflTransGen r e f
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
⟨b, hea.tail hfb, ReflGen.refl⟩

Premises used: And.intro, Relation.ReflTransGen.tail, Exists.intro, Relation.ReflGen.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
hea : ReflTransGen r e f
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
exact ⟨b, hea.tail hfb, ReflGen.refl⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
tail : ∀ (c : α) (hbc : ReflGen r b c) (hac : ReflTransGen r a c), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c_1 : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac_1 : ReflTransGen r a_1 c_1
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
c : α
hbc : ReflGen r b c
hac : ReflTransGen r a c
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
⟨c, hea.trans hac, hbc⟩

Premises used: Relation.ReflTransGen.trans, And.intro, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c_1 : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac_1 : ReflTransGen r a_1 c_1
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
c : α
hbc : ReflGen r b c
hac : ReflTransGen r a c
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
exact ⟨c, hea.trans hac, hbc⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b_2 f b : α
h_2 : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f a
tail : ∀ (hea : ReflTransGen r e f), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
tail₁ : ∀ (hfa : r f a), ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
refl : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r d a
tail :
  ∀ {f b : α},
    ReflTransGen r d f →
      ∀ (hfb : r f b) (ih : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r f a),
        ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
⊢ ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a

Tactic:
have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
this : ∃ (a : α), ReflTransGen r e a ∧ ReflGen r b a
tail : ∀ (a : α) (hea : ReflTransGen r e a) (hba : ReflGen r b a), Join (ReflTransGen r) e c
⊢ Join (ReflTransGen r) e c

Tactic:
rcases this with ⟨a, hea, hba⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
hea : ReflTransGen r e b
⊢ Join (ReflTransGen r) e c

Tactic:
⟨b, hea, hcb⟩

Premises used: Relation.Join, And.intro, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
d e : α
h_1 : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
hea : ReflTransGen r e b
⊢ Join (ReflTransGen r) e c

Tactic:
exact ⟨b, hea, hcb⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : r b a
⊢ Join (ReflTransGen r) e c

Tactic:
⟨a, hea, hcb.tail hba⟩

Premises used: Relation.Join, And.intro, Relation.ReflTransGen.tail, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : r b a
⊢ Join (ReflTransGen r) e c

Tactic:
exact ⟨a, hea, hcb.tail hba⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a_1 b_1 c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a_1 c
d e : α
h_1 : ReflTransGen r a_1 d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : ReflGen r b a
tail : ∀ (hea : ReflTransGen r e b), Join (ReflTransGen r) e c
tail₁ : ∀ (hba : r b a), Join (ReflTransGen r) e c
⊢ Join (ReflTransGen r) e c

Tactic:
cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b c : α
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
hab : ReflTransGen r a b
hac : ReflTransGen r a c
refl : Join (ReflTransGen r) a c
tail : ∀ {d e : α}, ReflTransGen r a d → ∀ (hde : r d e) (ih : Join (ReflTransGen r) d c), Join (ReflTransGen r) e c
⊢ Join (ReflTransGen r) b c

Tactic:
induction hab with
  | refl => exact ⟨c, hac, refl⟩
  | @tail d e _ hde ih =>
    rcases ih with ⟨b, hdb, hcb⟩
    have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
    rcases this with ⟨a, hea, hba⟩
    cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩

Premises used: Relation.ReflTransGen.tail
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
inst : Std.Refl r
hab : r a b
⊢ Join r a b

Tactic:
⟨b, hab, refl b⟩

Premises used: Relation.Join, And.intro, Exists.intro, refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
⊢ Symmetric (Join r)

Tactic:
fun _ _ ⟨c, hac, hcb⟩ ↦ ⟨c, hcb, hac⟩

Premises used: Symmetric, Relation.Join, And.intro, _private.0.Relation.symmetric_join.match_1, Exists.intro
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
h : ∀ (a b c : α), r a b → r a c → Join r b c
⊢ IsTrans α (Join r)

Tactic:
⟨fun _a b _c ⟨x, hax, hbx⟩ ⟨y, hby, hcy⟩ ↦
  let ⟨z, hxz, hyz⟩ := h b x y hbx hby
  ⟨z, trans_of r hax hxz, trans_of r hcy hyz⟩⟩

Premises used: IsTrans.mk, Relation.Join, And.intro, _private.0.Relation.symmetric_join.match_1, Exists.intro, trans_of
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Refl r
inst_1 : IsTrans α r
h : ∀ (a b c : α), r a b → r a c → Join r b c
⊢ Equivalence (Join r)

Tactic:
⟨reflexive_join.refl, @symmetric_join α r, isTrans_join h |>.trans _ _ _⟩

Premises used: Std.Refl.refl, IsTrans.trans, Relation.symmetric_join, Equivalence.mk
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h : ∀ (a b c : α), r a b → r a c → ∃ (d : α), ReflGen r b d ∧ ReflTransGen r c d
⊢ Equivalence (Join (ReflTransGen r))

Tactic:
equivalence_join fun _ _ _ ↦ church_rosser h

Premises used: Relation.equivalence_join, Relation.church_rosser
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
r' : α → α → Prop
inst : Std.Refl r
inst_1 : IsTrans α r
h : ∀ (a b : α), r' a b → r a b
h' : ReflTransGen r' a b
⊢ r a b

Tactic:
simpa [reflTransGen_eq_self] using ReflTransGen.mono h h'

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

Tactic:
@reflTransGen_of_isTrans_reflexive _ _ _ _ _ hr.stdRefl hr.isTrans

Premises used: Relation.reflTransGen_of_isTrans_reflexive
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
H : mk r a = mk r b
⊢ EqvGen r a b

Tactic:
@Quotient.exact _ (EqvGen.setoid r) a b (congrArg
    (Quot.lift (Quotient.mk (EqvGen.setoid r)) (fun x y h ↦ Quot.sound (EqvGen.rel x y h))) H)

Premises used: Quot.sound, congrArg, Quot.lift, Quotient.mk, Relation.EqvGen.setoid, Quotient.exact, Relation.EqvGen.rel
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
H : EqvGen r a b
⊢ mk r a = mk r b

Tactic:
EqvGen.rec
    (fun _ _ h ↦ Quot.sound h)
    (fun _ ↦ rfl)
    (fun _ _ _ IH ↦ Eq.symm IH)
    (fun _ _ _ _ _ IH₁ IH₂ ↦ Eq.trans IH₁ IH₂)
    H

Premises used: Relation.EqvGen.rec
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : Equivalence r
x y : α
h_1 : r x y
⊢ r x y

Tactic:
assumption
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : Equivalence r
x : α
⊢ r x x

Tactic:
h.1 _

Premises used: Equivalence.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : Equivalence r
x : α
⊢ r x x

Tactic:
exact h.1 _

Premises used: Equivalence.refl
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : Equivalence r
x y : α
h_1 : EqvGen r x y
a_ih symm : r x y
⊢ r y x

Tactic:
apply h.symm

Premises used: Equivalence.symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : Equivalence r
x y : α
h_1 : EqvGen r x y
a_ih : r x y
⊢ r x y

Tactic:
assumption
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : Equivalence r
x y z : α
h_1 : EqvGen r x y
h_2 : EqvGen r y z
hab : r x y
hbc : r y z
⊢ r x z

Tactic:
h.trans hab hbc

Premises used: Equivalence.trans
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h : Equivalence r
x y z : α
h_1 : EqvGen r x y
h_2 : EqvGen r y z
hab : r x y
hbc : r y z
⊢ r x z

Tactic:
exact h.trans hab hbc

Premises used: Equivalence.trans
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
a b : α
h_1 : Equivalence r
h : EqvGen r a b
rel : ∀ (x y : α), r x y → r x y
refl : ∀ (x : α), r x x
symm : ∀ (x y : α), EqvGen r x y → r x y → r y x
trans : ∀ (x y z : α), EqvGen r x y → EqvGen r y z → ∀ (hab : r x y) (hbc : r y z), r x z
⊢ r a b

Tactic:
induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc

Premises used: Equivalence.symm, Equivalence.refl, Equivalence.trans, Relation.EqvGen.symm
-- Module: Mathlib.Logic.Relation
Goal:
α : Sort u_1
r : α → α → Prop
h : Equivalence r
⊢ Eq.{max 1 u_1} (EqvGen r) r

Tactic:
funext fun _ ↦ funext fun _ ↦ propext <| h.eqvGen_iff

Premises used: funext, propext, Equivalence.eqvGen_iff
-- Module: Mathlib.Logic.Relator
Goal:
α : Sort u₁
β : Sort u₂
R : α → β → Prop
h : RightTotal R
⊢ ((R ⇒ fun (x1 : Sort u_1) (x2 : Prop) ↦ ∀ (a : x1), x2) ⇒ fun (x1 : Sort (imax u₁ u_1)) (x2 : Prop) ↦ ∀ (a : x1), x2)
    (fun (p : α → Sort u_1) ↦ (i : α) → p i) fun (q : β → Prop) ↦ ∀ (i : β), q i

Tactic:
fun _ _ Hrel H b => Exists.elim (h b) (fun _ Rab => Hrel Rab (H _))

Premises used: Relator.LiftFun, Exists.elim
-- Module: Mathlib.Logic.Relator
Goal:
α : Sort u₁
β : Sort u₂
R : α → β → Prop
h : LeftTotal R
⊢ LiftFun.{max u₁ 1, max u₂ 1, 1, 1} (R ⇒ fun (x1 x2 : Prop) ↦ x1 → x2) (fun (x1 x2 : Prop) ↦ x1 → x2)
    (fun (p : α → Prop) ↦ ∃ (i : α), p i) fun (q : β → Prop) ↦ ∃ (i : β), q i

Tactic:
fun _ _ Hrel ⟨a, pa⟩ => (h a).imp fun _ Rab => Hrel Rab pa

Premises used: _private.0.Relator.LeftTotal.rel_exists.match_1, Exists, Exists.imp, Relator.LiftFun
-- Module: Mathlib.Logic.Relator
Goal:
α : Sort u₁
β : Sort u₂
R : α → β → Prop
h : BiTotal R
⊢ LiftFun.{max u₁ 1, max u₂ 1, 1, 1} (R ⇒ Iff) Iff (fun (p : α → Prop) ↦ ∀ (i : α), p i) fun (q : β → Prop) ↦
    ∀ (i : β), q i

Tactic:
fun _ _ Hrel =>
    ⟨fun H b => Exists.elim (h.right b) (fun _ Rab => (Hrel Rab).mp (H _)),
      fun H a => Exists.elim (h.left a) (fun _ Rab => (Hrel Rab).mpr (H _))⟩

Premises used: Iff.mpr, And.right, And.left, Iff.intro, Iff.mp, Relator.LiftFun, Exists.elim
-- Module: Mathlib.Logic.Relator
Goal:
α : Sort u₁
β : Sort u₂
R : α → β → Prop
h : BiTotal R
⊢ LiftFun.{max u₁ 1, max u₂ 1, 1, 1} (R ⇒ Iff) Iff (fun (p : α → Prop) ↦ ∃ (i : α), p i) fun (q : β → Prop) ↦
    ∃ (i : β), q i

Tactic:
fun _ _ Hrel =>
    ⟨fun ⟨a, pa⟩ => (h.left a).imp fun _ Rab => (Hrel Rab).1 pa,
      fun ⟨b, qb⟩ => (h.right b).imp fun _ Rab => (Hrel Rab).2 qb⟩

Premises used: Iff.mpr, _private.0.Relator.LeftTotal.rel_exists.match_1, Exists, Exists.imp, And.right, And.left, Iff.intro, Iff.mp, Relator.LiftFun
-- Module: Mathlib.Logic.Relator
Goal:
α : Sort u₁
β : Sort u₂
R : α → β → Prop
eq' : β → β → Prop
he : (R ⇒ R ⇒ Iff) Eq eq'
⊢ LeftUnique R

Tactic:
fun a b c (ac : R a c) (bc : R b c) => (he ac bc).mpr ((he bc bc).mp rfl)

Premises used: Iff.mpr, Iff.mp, rfl, Relator.LeftUnique
-- Module: Mathlib.Logic.Relator
Goal:
⊢ (Iff ⇒ Iff ⇒ Iff) (fun (x1 x2 : Prop) ↦ x1 → x2) fun (x1 x2 : Prop) ↦ x1 → x2

Tactic:
fun _ _ h _ _ l => imp_congr h l

Premises used: imp_congr, Relator.LiftFun
-- Module: Mathlib.Logic.Relator
Goal:
⊢ (Iff ⇒ Iff) Not Not

Tactic:
fun _ _ h => not_congr h

Premises used: not_congr, Relator.LiftFun
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u₁
⊢ BiTotal.{u₁ + 1, u₁ + 1} (α := α) Eq

Tactic:
{ left := fun a => ⟨a, rfl⟩, right := fun a => ⟨a, rfl⟩ }

Premises used: And.intro, Exists.intro, Relator.BiTotal, rfl
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
h : LeftUnique r
⊢ RightUnique (_root_.flip r)

Tactic:
fun _ _ _ h₁ h₂ => h h₁ h₂

Premises used: Relator.RightUnique
-- Module: Mathlib.Logic.Relator
Goal:
⊢ LiftFun (γ := Prop → Prop) (δ := Prop → Prop) (fun (x1 x2 : Prop) ↦ x1 ↔ x2)
    ((fun (x1 x2 : Prop) ↦ x1 ↔ x2) ⇒ fun (x1 x2 : Prop) ↦ x1 ↔ x2) (fun (x1 x2 : Prop) ↦ x1 ∧ x2) fun (x1 x2 : Prop) ↦
    x1 ∧ x2

Tactic:
fun _ _ h₁ _ _ h₂ => and_congr h₁ h₂

Premises used: and_congr, Relator.LiftFun
-- Module: Mathlib.Logic.Relator
Goal:
⊢ LiftFun (γ := Prop → Prop) (δ := Prop → Prop) (fun (x1 x2 : Prop) ↦ x1 ↔ x2)
    ((fun (x1 x2 : Prop) ↦ x1 ↔ x2) ⇒ fun (x1 x2 : Prop) ↦ x1 ↔ x2) (fun (x1 x2 : Prop) ↦ x1 ∨ x2) fun (x1 x2 : Prop) ↦
    x1 ∨ x2

Tactic:
fun _ _ h₁ _ _ h₂ => or_congr h₁ h₂

Premises used: or_congr, Relator.LiftFun