-- Mathlib/Logic/Relation.lean
theorem church_rosser (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) : Join (ReflTransGen r) b c

Proof state:
case tail.intro.intro.single.intro.intro
α : Type 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 : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : 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⟩

Result:
no goals

Proof state:
case tail
α : Type 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 : α
a✝ : ReflTransGen r a d
hde : r d e
ih : Join (ReflTransGen r) d c
⊢ Join (ReflTransGen r) e c

Tactic:
rcases ih with ⟨b, hdb, hcb⟩

Result:
case tail.intro.intro
α : Type 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 : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
⊢ Join (ReflTransGen r) e c

Proof state:
case refl
α : Type 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 : α
a✝ : 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⟩

Result:
no goals

Proof state:
case tail.intro.intro
α : Type 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 : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f 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⟩

Result:
no goals

Proof state:
α : Type 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 : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
⊢ ∃ 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⟩

Result:
no goals

Proof state:
case tail.intro.intro
α : Type 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 : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
⊢ Join (ReflTransGen r) e c

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⟩

Result:
case tail.intro.intro
α : Type 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 : α
a✝ : 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
⊢ Join (ReflTransGen r) e c

Proof state:
case tail.intro.intro.intro.intro.refl
α : Type 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 : α
a✝ : 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⟩

Result:
no goals

Proof state:
case tail.intro.intro.refl
α : Type 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 : α
a✝¹ : ReflTransGen r a d
hde : r d e
b✝ f b : α
a✝ : 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⟩

Result:
no goals

Proof state:
α : Type 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
⊢ 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⟩

Result:
no goals

Proof state:
case tail.intro.intro.single
α : Type 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 : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Tactic:
rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩

Result:
case tail.intro.intro.single.intro.intro
α : Type 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 : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : 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

Proof state:
case refl
α : Type 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⟩

Result:
no goals

Proof state:
α : Type 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 : α
a✝ : 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:
clear hcb

Result:
α : Type 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 : α
a✝ : ReflTransGen r a d
hde : r d e
b : α
hdb : ReflTransGen r d b
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a

Proof state:
case tail
α : Type 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 : α
a✝¹ : ReflTransGen r a d
hde : r d e
b✝ f b : α
a✝ : 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

Tactic:
rcases ih with ⟨a, hea, hfa⟩

Result:
case tail.intro.intro
α : Type 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 : α
a✝¹ : ReflTransGen r a✝² d
hde : r d e
b✝ f b : α
a✝ : ReflTransGen r d f
hfb : r f b
a : α
hea : ReflTransGen r e a
hfa : ReflGen r f a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r b a