[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
⊢ r x y
[PROOFSTEP]
by_cases hxy : x = y
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : x = y
⊢ r x y
[PROOFSTEP]
exact hxy ▸ h x
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
h : Reflexive r
x y : α
hr : x ≠ y → r x y
hxy : ¬x = y
⊢ r x y
[PROOFSTEP]
exact hr hxy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : Prop → α → Prop
⊢ (fun x x_1 => x ↔ x_1) ∘r r = r
[PROOFSTEP]
have : (· ↔ ·) = (· = ·) := by funext a b; exact iff_eq_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : Prop → α → Prop
⊢ (fun x x_1 => x ↔ x_1) = fun x x_1 => x = x_1
[PROOFSTEP]
funext a b
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : Prop → α → Prop
a b : Prop
⊢ (a ↔ b) = (a = b)
[PROOFSTEP]
exact iff_eq_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : Prop → α → Prop
this : (fun x x_1 => x ↔ x_1) = fun x x_1 => x = x_1
⊢ (fun x x_1 => x ↔ x_1) ∘r r = r
[PROOFSTEP]
rw [this, eq_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : α → Prop → Prop
⊢ (r ∘r fun x x_1 => x ↔ x_1) = r
[PROOFSTEP]
have : (· ↔ ·) = (· = ·) := by funext a b; exact iff_eq_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : α → Prop → Prop
⊢ (fun x x_1 => x ↔ x_1) = fun x x_1 => x = x_1
[PROOFSTEP]
funext a b
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : α → Prop → Prop
a b : Prop
⊢ (a ↔ b) = (a = b)
[PROOFSTEP]
exact iff_eq_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
r : α → Prop → Prop
this : (fun x x_1 => x ↔ x_1) = fun x x_1 => x = x_1
⊢ (r ∘r fun x x_1 => x ↔ x_1) = r
[PROOFSTEP]
rw [this, comp_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q
[PROOFSTEP]
funext a d
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d = (r ∘r p ∘r q) a d
[PROOFSTEP]
apply propext
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d ↔ (r ∘r p ∘r q) a d
[PROOFSTEP]
constructor
[GOAL]
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ ((r ∘r p) ∘r q) a d → (r ∘r p ∘r q) a d
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d
[PROOFSTEP]
exact fun ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩
[GOAL]
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
a : α
d : δ
⊢ (r ∘r p ∘r q) a d → ((r ∘r p) ∘r q) a d
[PROOFSTEP]
exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ flip (r ∘r p) = flip p ∘r flip r
[PROOFSTEP]
funext c a
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a = (flip p ∘r flip r) c a
[PROOFSTEP]
apply propext
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a
[PROOFSTEP]
constructor
[GOAL]
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a
[PROOFSTEP]
exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩
[GOAL]
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a
[PROOFSTEP]
exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a : α
ha : Acc rα a
⊢ Acc rβ (f a)
[PROOFSTEP]
induction' ha with a _ ih
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)
[PROOFSTEP]
refine' Acc.intro (f a) fun b hr ↦ _
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
b : β
hr : rβ b (f a)
⊢ Acc rβ b
[PROOFSTEP]
obtain ⟨a', hr', rfl⟩ := fib hr
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
a' : α
hr' : rα a' a
hr : rβ (f a') (f a)
⊢ Acc rβ (f a')
[PROOFSTEP]
exact ih a' hr'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b c d a : α
⊢ ReflTransGen r a a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b c d : α
p : α → α → Prop
hp : ∀ (a b : α), r a b → p a b
a : α
⊢ ReflGen p a a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c
[PROOFSTEP]
induction hbc
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
⊢ ReflTransGen r a b
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝
[PROOFSTEP]
case refl => assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
⊢ ReflTransGen r a b
[PROOFSTEP]
case refl => assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
⊢ ReflTransGen r a b
[PROOFSTEP]
assumption
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝
[PROOFSTEP]
case tail c d _ hcd hac => exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d✝ : α
hab : ReflTransGen r a b
c d : α
a✝ : ReflTransGen r b c
hcd : r c d
hac : ReflTransGen r a c
⊢ ReflTransGen r a d
[PROOFSTEP]
case tail c d _ hcd hac => exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d✝ : α
hab : ReflTransGen r a b
c d : α
a✝ : ReflTransGen r b c
hcd : r c d
hac : ReflTransGen r a c
⊢ ReflTransGen r a d
[PROOFSTEP]
exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : r a b
hbc : ReflTransGen r b c
⊢ ReflTransGen r a c
[PROOFSTEP]
induction hbc
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : r a b
⊢ ReflTransGen r a b
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝
[PROOFSTEP]
case refl => exact refl.tail hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : r a b
⊢ ReflTransGen r a b
[PROOFSTEP]
case refl => exact refl.tail hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : r a b
⊢ ReflTransGen r a b
[PROOFSTEP]
exact refl.tail hab
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : ReflTransGen r a b✝
⊢ ReflTransGen r a c✝
[PROOFSTEP]
case tail c d _ hcd hac => exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d✝ : α
hab : r a b
c d : α
a✝ : ReflTransGen r b c
hcd : r c d
hac : ReflTransGen r a c
⊢ ReflTransGen r a d
[PROOFSTEP]
case tail c d _ hcd hac => exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d✝ : α
hab : r a b
c d : α
a✝ : ReflTransGen r b c
hcd : r c d
hac : ReflTransGen r a c
⊢ ReflTransGen r a d
[PROOFSTEP]
exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : Symmetric r
⊢ Symmetric (ReflTransGen r)
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h✝ : Symmetric r
x y : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x
[PROOFSTEP]
induction' h with z w _ b c
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : Symmetric r
x y : α
⊢ ReflTransGen r x x
[PROOFSTEP]
rfl
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c✝ d : α
h : Symmetric r
x y z w : α
a✝ : ReflTransGen r x z
b : r z w
c : ReflTransGen r z x
⊢ ReflTransGen r w x
[PROOFSTEP]
apply Relation.ReflTransGen.head (h b) c
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b c d : α
P : (a : α) → ReflTransGen r a b → Prop
a : α
h : ReflTransGen r a b
refl : P b (_ : ReflTransGen r b b)
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)
⊢ P a h
[PROOFSTEP]
induction h
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b c d a : α
P : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : P a (_ : ReflTransGen r a a)
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), P c h → P a_1 (_ : ReflTransGen r a_1 a)
⊢ P a (_ : ReflTransGen r a a)
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b c d a b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ :
  ∀ {P : (a : α) → ReflTransGen r a b✝ → Prop},
    P b✝ (_ : ReflTransGen r b✝ b✝) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b✝), P c h → P a (_ : ReflTransGen r a b✝)) → P a a✝¹
P : (a : α) → ReflTransGen r a c✝ → Prop
refl : P c✝ (_ : ReflTransGen r c✝ c✝)
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c c✝), P c h → P a (_ : ReflTransGen r a c✝)
⊢ P a (_ : ReflTransGen r a c✝)
[PROOFSTEP]
case refl => exact refl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b c d a : α
P : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : P a (_ : ReflTransGen r a a)
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), P c h → P a_1 (_ : ReflTransGen r a_1 a)
⊢ P a (_ : ReflTransGen r a a)
[PROOFSTEP]
case refl => exact refl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b c d a : α
P : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : P a (_ : ReflTransGen r a a)
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), P c h → P a_1 (_ : ReflTransGen r a_1 a)
⊢ P a (_ : ReflTransGen r a a)
[PROOFSTEP]
exact refl
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b c d a b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ :
  ∀ {P : (a : α) → ReflTransGen r a b✝ → Prop},
    P b✝ (_ : ReflTransGen r b✝ b✝) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b✝), P c h → P a (_ : ReflTransGen r a b✝)) → P a a✝¹
P : (a : α) → ReflTransGen r a c✝ → Prop
refl : P c✝ (_ : ReflTransGen r c✝ c✝)
head : ∀ {a c : α} (h' : r a c) (h : ReflTransGen r c c✝), P c h → P a (_ : ReflTransGen r a c✝)
⊢ P a (_ : ReflTransGen r a c✝)
[PROOFSTEP]
case tail b c _ hbc ih =>
  -- Porting note: Lean 3 figured out the motive and `apply ih` worked
  refine @ih (λ {a : α} (hab : ReflTransGen r a b) => P a (ReflTransGen.tail hab hbc)) ?_ ?_
  {exact head hbc _ refl
  }
  {exact fun h1 h2 ↦ head h1 (h2.tail hbc)
  }
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ P a (_ : ReflTransGen r a c)
[PROOFSTEP]
case tail b c _ hbc ih =>
  -- Porting note: Lean 3 figured out the motive and `apply ih` worked
  refine @ih (λ {a : α} (hab : ReflTransGen r a b) => P a (ReflTransGen.tail hab hbc)) ?_ ?_
  {exact head hbc _ refl
  }
  {exact fun h1 h2 ↦ head h1 (h2.tail hbc)
  }
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ P a (_ : ReflTransGen r a c)
[PROOFSTEP]
refine @ih (λ {a : α} (hab : ReflTransGen r a b) => P a (ReflTransGen.tail hab hbc)) ?_ ?_
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r b b)
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b),
    (fun {a} hab => P a (_ : ReflTransGen r a c)) h →
      (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r a b)
[PROOFSTEP]
{exact head hbc _ refl
}
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r b b)
[PROOFSTEP]
exact head hbc _ refl
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b),
    (fun {a} hab => P a (_ : ReflTransGen r a c)) h →
      (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r a b)
[PROOFSTEP]
{exact fun h1 h2 ↦ head h1 (h2.tail hbc)
}
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : ReflTransGen r a b
hbc : r b c
ih :
  ∀ {P : (a : α) → ReflTransGen r a b → Prop},
    P b (_ : ReflTransGen r b b) →
      (∀ {a c : α} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (_ : ReflTransGen r a b)) → P a a✝
P : (a : α) → ReflTransGen r a c → Prop
refl : P c (_ : ReflTransGen r c c)
head : ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 c), P c_1 h → P a (_ : ReflTransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : ReflTransGen r c_1 b),
    (fun {a} hab => P a (_ : ReflTransGen r a c)) h →
      (fun {a} hab => P a (_ : ReflTransGen r a c)) (_ : ReflTransGen r a b)
[PROOFSTEP]
exact fun h1 h2 ↦ head h1 (h2.tail hbc)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
h : ReflTransGen r a b
ih₁ : ∀ (a : α), P (_ : ReflTransGen r a a)
ih₂ : ∀ {a b : α} (h : r a b), P (_ : ReflTransGen r a b)
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (_ : ReflTransGen r a c)
⊢ P h
[PROOFSTEP]
induction h
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
ih₁ : ∀ (a : α), P (_ : ReflTransGen r a a)
ih₂ : ∀ {a b : α} (h : r a b), P (_ : ReflTransGen r a b)
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (_ : ReflTransGen r a c)
⊢ P (_ : ReflTransGen r a a)
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c d : α
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
ih₁ : ∀ (a : α), P (_ : ReflTransGen r a a)
ih₂ : ∀ {a b : α} (h : r a b), P (_ : ReflTransGen r a b)
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (_ : ReflTransGen r a c)
b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : P a✝¹
⊢ P (_ : ReflTransGen r a c✝)
[PROOFSTEP]
case refl => exact ih₁ a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
ih₁ : ∀ (a : α), P (_ : ReflTransGen r a a)
ih₂ : ∀ {a b : α} (h : r a b), P (_ : ReflTransGen r a b)
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (_ : ReflTransGen r a c)
⊢ P (_ : ReflTransGen r a a)
[PROOFSTEP]
case refl => exact ih₁ a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
ih₁ : ∀ (a : α), P (_ : ReflTransGen r a a)
ih₂ : ∀ {a b : α} (h : r a b), P (_ : ReflTransGen r a b)
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (_ : ReflTransGen r a c)
⊢ P (_ : ReflTransGen r a a)
[PROOFSTEP]
exact ih₁ a
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c d : α
P : {a b : α} → ReflTransGen r a b → Prop
a b : α
ih₁ : ∀ (a : α), P (_ : ReflTransGen r a a)
ih₂ : ∀ {a b : α} (h : r a b), P (_ : ReflTransGen r a b)
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (_ : ReflTransGen r a c)
b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : P a✝¹
⊢ P (_ : ReflTransGen r a c✝)
[PROOFSTEP]
case tail b c hab hbc ih => exact ih₃ hab (single hbc) ih (ih₂ hbc)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c✝ d : α
P : {a b : α} → ReflTransGen r a b → Prop
a b✝ : α
ih₁ : ∀ (a : α), P (_ : ReflTransGen r a a)
ih₂ : ∀ {a b : α} (h : r a b), P (_ : ReflTransGen r a b)
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (_ : ReflTransGen r a c)
b c : α
hab : ReflTransGen r a b
hbc : r b c
ih : P hab
⊢ P (_ : ReflTransGen r a c)
[PROOFSTEP]
case tail b c hab hbc ih => exact ih₃ hab (single hbc) ih (ih₂ hbc)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c✝ d : α
P : {a b : α} → ReflTransGen r a b → Prop
a b✝ : α
ih₁ : ∀ (a : α), P (_ : ReflTransGen r a a)
ih₂ : ∀ {a b : α} (h : r a b), P (_ : ReflTransGen r a b)
ih₃ : ∀ {a b c : α} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (_ : ReflTransGen r a c)
b c : α
hab : ReflTransGen r a b
hbc : r b c
ih : P hab
⊢ P (_ : ReflTransGen r a c)
[PROOFSTEP]
exact ih₃ hab (single hbc) ih (ih₂ hbc)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : ReflTransGen r a b
⊢ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b
[PROOFSTEP]
induction h using Relation.ReflTransGen.head_induction_on
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
⊢ b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b
[PROOFSTEP]
left
[GOAL]
case refl.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
⊢ b = b
[PROOFSTEP]
rfl
[GOAL]
case head
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b
[PROOFSTEP]
right
[GOAL]
case head.h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ ∃ c, r a✝¹ c ∧ ReflTransGen r c b
[PROOFSTEP]
exact ⟨_, by assumption, by assumption⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ r a✝¹ ?m.17056
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ ReflTransGen r c✝ b
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b
[PROOFSTEP]
use cases_head
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) → ReflTransGen r a b
[PROOFSTEP]
rintro (rfl | ⟨c, hac, hcb⟩)
[GOAL]
case mpr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a c d : α
⊢ ReflTransGen r a a
[PROOFSTEP]
rfl
[GOAL]
case mpr.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b
[PROOFSTEP]
exact head hac hcb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
U : Relator.RightUnique r
ab : ReflTransGen r a b
ac : ReflTransGen r a c
⊢ ReflTransGen r b c ∨ ReflTransGen r c b
[PROOFSTEP]
induction' ab with b d _ bd IH
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
⊢ ReflTransGen r a c ∨ ReflTransGen r c a
[PROOFSTEP]
exact Or.inl ac
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c ∨ ReflTransGen r c b
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
[PROOFSTEP]
rcases IH with (IH | IH)
[GOAL]
case tail.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
[PROOFSTEP]
rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
[GOAL]
case tail.inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ d✝ : α
U : Relator.RightUnique r
b d : α
a✝ : ReflTransGen r a b
bd : r b d
ac : ReflTransGen r a b
IH : ReflTransGen r b b
⊢ ReflTransGen r d b ∨ ReflTransGen r b d
[PROOFSTEP]
exact Or.inr (single bd)
[GOAL]
case tail.inl.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
e : α
be : r b e
ec : ReflTransGen r e c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
[PROOFSTEP]
cases U bd be
[GOAL]
case tail.inl.inr.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
be : r b d
ec : ReflTransGen r d c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
[PROOFSTEP]
exact Or.inl ec
[GOAL]
case tail.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r c b
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
[PROOFSTEP]
exact Or.inr (IH.tail bd)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d a b : α
h : TransGen r a b
⊢ ReflTransGen r a b
[PROOFSTEP]
induction' h with b h b c _ bc ab
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c d a b✝ b : α
h : r a b
⊢ ReflTransGen r a b
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝¹ c✝ d a b✝ b c : α
a✝ : TransGen r a b
bc : r b c
ab : ReflTransGen r a b
⊢ ReflTransGen r a c
[PROOFSTEP]
exact ReflTransGen.single h
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝¹ c✝ d a b✝ b c : α
a✝ : TransGen r a b
bc : r b c
ab : ReflTransGen r a b
⊢ ReflTransGen r a c
[PROOFSTEP]
exact ReflTransGen.tail ab bc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : TransGen r a b
hbc : ReflTransGen r b c
⊢ TransGen r a c
[PROOFSTEP]
induction hbc
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : TransGen r a b
⊢ TransGen r a b
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : TransGen r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen r a b✝
⊢ TransGen r a c✝
[PROOFSTEP]
case refl => assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : TransGen r a b
⊢ TransGen r a b
[PROOFSTEP]
case refl => assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : TransGen r a b
⊢ TransGen r a b
[PROOFSTEP]
assumption
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : TransGen r a b
b✝ c✝ : α
a✝¹ : ReflTransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen r a b✝
⊢ TransGen r a c✝
[PROOFSTEP]
case tail c d _ hcd hac => exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d✝ : α
hab : TransGen r a b
c d : α
a✝ : ReflTransGen r b c
hcd : r c d
hac : TransGen r a c
⊢ TransGen r a d
[PROOFSTEP]
case tail c d _ hcd hac => exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d✝ : α
hab : TransGen r a b
c d : α
a✝ : ReflTransGen r b c
hcd : r c d
hac : TransGen r a c
⊢ TransGen r a d
[PROOFSTEP]
exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
hbc : r b c
⊢ TransGen r a c
[PROOFSTEP]
induction hab generalizing c
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b d c : α
hbc : r a c
⊢ TransGen r a c
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b d b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
[PROOFSTEP]
case refl => exact single hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b d c : α
hbc : r a c
⊢ TransGen r a c
[PROOFSTEP]
case refl => exact single hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b d c : α
hbc : r a c
⊢ TransGen r a c
[PROOFSTEP]
exact single hbc
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b d b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
[PROOFSTEP]
case tail _ _ _ hdb IH => exact tail (IH hdb) hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b d b✝ c✝ : α
a✝ : ReflTransGen r a b✝
hdb : r b✝ c✝
IH : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
[PROOFSTEP]
case tail _ _ _ hdb IH => exact tail (IH hdb) hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b d b✝ c✝ : α
a✝ : ReflTransGen r a b✝
hdb : r b✝ c✝
IH : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c
[PROOFSTEP]
exact tail (IH hdb) hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b c d : α
P : (a : α) → TransGen r a b → Prop
a : α
h : TransGen r a b
base : ∀ {a : α} (h : r a b), P a (_ : TransGen r a b)
ih : ∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a (_ : TransGen r a b)
⊢ P a h
[PROOFSTEP]
induction h
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b c d a b✝ : α
a✝ : r a b✝
P : (a : α) → TransGen r a b✝ → Prop
base : ∀ {a : α} (h : r a b✝), P a (_ : TransGen r a b✝)
ih : ∀ {a c : α} (h' : r a c) (h : TransGen r c b✝), P c h → P a (_ : TransGen r a b✝)
⊢ P a (_ : TransGen r a b✝)
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b c d a b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ :
  ∀ {P : (a : α) → TransGen r a b✝ → Prop},
    (∀ {a : α} (h : r a b✝), P a (_ : TransGen r a b✝)) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b✝), P c h → P a (_ : TransGen r a b✝)) → P a a✝¹
P : (a : α) → TransGen r a c✝ → Prop
base : ∀ {a : α} (h : r a c✝), P a (_ : TransGen r a c✝)
ih : ∀ {a c : α} (h' : r a c) (h : TransGen r c c✝), P c h → P a (_ : TransGen r a c✝)
⊢ P a (_ : TransGen r a c✝)
[PROOFSTEP]
case single a h => exact base h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b c d a✝ a : α
h : r a✝ a
P : (a_1 : α) → TransGen r a_1 a → Prop
base : ∀ {a_1 : α} (h : r a_1 a), P a_1 (_ : TransGen r a_1 a)
ih : ∀ {a_1 c : α} (h' : r a_1 c) (h : TransGen r c a), P c h → P a_1 (_ : TransGen r a_1 a)
⊢ P a✝ (_ : TransGen r a✝ a)
[PROOFSTEP]
case single a h => exact base h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b c d a✝ a : α
h : r a✝ a
P : (a_1 : α) → TransGen r a_1 a → Prop
base : ∀ {a_1 : α} (h : r a_1 a), P a_1 (_ : TransGen r a_1 a)
ih : ∀ {a_1 c : α} (h' : r a_1 c) (h : TransGen r c a), P c h → P a_1 (_ : TransGen r a_1 a)
⊢ P a✝ (_ : TransGen r a✝ a)
[PROOFSTEP]
exact base h
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b c d a b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ :
  ∀ {P : (a : α) → TransGen r a b✝ → Prop},
    (∀ {a : α} (h : r a b✝), P a (_ : TransGen r a b✝)) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b✝), P c h → P a (_ : TransGen r a b✝)) → P a a✝¹
P : (a : α) → TransGen r a c✝ → Prop
base : ∀ {a : α} (h : r a c✝), P a (_ : TransGen r a c✝)
ih : ∀ {a c : α} (h' : r a c) (h : TransGen r c c✝), P c h → P a (_ : TransGen r a c✝)
⊢ P a (_ : TransGen r a c✝)
[PROOFSTEP]
case tail b c _ hbc h_ih =>
  -- Lean 3 could figure out the motive and `apply h_ih` worked
  refine @h_ih (λ {a : α} (hab : @TransGen α r a b) => P a (TransGen.tail hab hbc)) ?_ ?_;
  exact fun h ↦ ih h (single hbc) (base hbc)
  exact fun hab hbc ↦ ih hab _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a (_ : TransGen r a b)) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a (_ : TransGen r a b)) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a (_ : TransGen r a c)
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a (_ : TransGen r a c)
⊢ P a (_ : TransGen r a c)
[PROOFSTEP]
case tail b c _ hbc h_ih =>
  -- Lean 3 could figure out the motive and `apply h_ih` worked
  refine @h_ih (λ {a : α} (hab : @TransGen α r a b) => P a (TransGen.tail hab hbc)) ?_ ?_;
  exact fun h ↦ ih h (single hbc) (base hbc)
  exact fun hab hbc ↦ ih hab _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a (_ : TransGen r a b)) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a (_ : TransGen r a b)) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a (_ : TransGen r a c)
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a (_ : TransGen r a c)
⊢ P a (_ : TransGen r a c)
[PROOFSTEP]
refine @h_ih (λ {a : α} (hab : @TransGen α r a b) => P a (TransGen.tail hab hbc)) ?_ ?_
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a (_ : TransGen r a b)) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a (_ : TransGen r a b)) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a (_ : TransGen r a c)
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a (_ : TransGen r a c)
⊢ ∀ {a : α} (h : r a b), (fun {a} hab => P a (_ : TransGen r a c)) (_ : TransGen r a b)
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a (_ : TransGen r a b)) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a (_ : TransGen r a b)) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a (_ : TransGen r a c)
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a (_ : TransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b),
    (fun {a} hab => P a (_ : TransGen r a c)) h → (fun {a} hab => P a (_ : TransGen r a c)) (_ : TransGen r a b)
[PROOFSTEP]
exact fun h ↦ ih h (single hbc) (base hbc)
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d a b c : α
a✝ : TransGen r a b
hbc : r b c
h_ih :
  ∀ {P : (a : α) → TransGen r a b → Prop},
    (∀ {a : α} (h : r a b), P a (_ : TransGen r a b)) →
      (∀ {a c : α} (h' : r a c) (h : TransGen r c b), P c h → P a (_ : TransGen r a b)) → P a a✝
P : (a : α) → TransGen r a c → Prop
base : ∀ {a : α} (h : r a c), P a (_ : TransGen r a c)
ih : ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 c), P c_1 h → P a (_ : TransGen r a c)
⊢ ∀ {a c_1 : α} (h' : r a c_1) (h : TransGen r c_1 b),
    (fun {a} hab => P a (_ : TransGen r a c)) h → (fun {a} hab => P a (_ : TransGen r a c)) (_ : TransGen r a b)
[PROOFSTEP]
exact fun hab hbc ↦ ih hab _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
⊢ P h
[PROOFSTEP]
induction h with
| single h => exact base h
| tail hab hbc h_ih => exact ih hab (single hbc) h_ih (base hbc)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
h : TransGen r a b
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
⊢ P h
[PROOFSTEP]
induction h with
| single h => exact base h
| tail hab hbc h_ih => exact ih hab (single hbc) h_ih (base hbc)
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
b✝ : α
h : r a b✝
⊢ P (_ : TransGen r a b✝)
[PROOFSTEP]

| single h => exact base h
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
b✝ : α
h : r a b✝
⊢ P (_ : TransGen r a b✝)
[PROOFSTEP]
exact base h
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
b✝ c✝ : α
hab : TransGen r a b✝
hbc : r b✝ c✝
h_ih : P hab
⊢ P (_ : TransGen r a c✝)
[PROOFSTEP]

| tail hab hbc h_ih => exact ih hab (single hbc) h_ih (base hbc)
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c d : α
P : {a b : α} → TransGen r a b → Prop
a b : α
base : ∀ {a b : α} (h : r a b), P (_ : TransGen r a b)
ih : ∀ {a b c : α} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (_ : TransGen r a c)
b✝ c✝ : α
hab : TransGen r a b✝
hbc : r b✝ c✝
h_ih : P hab
⊢ P (_ : TransGen r a c✝)
[PROOFSTEP]
exact ih hab (single hbc) h_ih (base hbc)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
hbc : TransGen r b c
⊢ TransGen r a c
[PROOFSTEP]
induction hbc
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
b✝ : α
a✝ : r b b✝
⊢ TransGen r a b✝
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
b✝ c✝ : α
a✝¹ : TransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen r a b✝
⊢ TransGen r a c✝
[PROOFSTEP]
case single c hbc => exact tail' hab hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d : α
hab : ReflTransGen r a b
c : α
hbc : r b c
⊢ TransGen r a c
[PROOFSTEP]
case single c hbc => exact tail' hab hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d : α
hab : ReflTransGen r a b
c : α
hbc : r b c
⊢ TransGen r a c
[PROOFSTEP]
exact tail' hab hbc
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hab : ReflTransGen r a b
b✝ c✝ : α
a✝¹ : TransGen r b b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen r a b✝
⊢ TransGen r a c✝
[PROOFSTEP]
case tail c d _ hcd hac => exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d✝ : α
hab : ReflTransGen r a b
c d : α
a✝ : TransGen r b c
hcd : r c d
hac : TransGen r a c
⊢ TransGen r a d
[PROOFSTEP]
case tail c d _ hcd hac => exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d✝ : α
hab : ReflTransGen r a b
c d : α
a✝ : TransGen r b c
hcd : r c d
hac : TransGen r a c
⊢ TransGen r a d
[PROOFSTEP]
exact hac.tail hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
⊢ TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : TransGen r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
[PROOFSTEP]
cases' h with _ hac b _ hab hbc
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hac : r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
[PROOFSTEP]
exact ⟨_, by rfl, hac⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
hac : r a c
⊢ ReflTransGen r a a
[PROOFSTEP]
rfl
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d b : α
hab : TransGen r a b
hbc : r b c
⊢ ∃ b, ReflTransGen r a b ∧ r b c
[PROOFSTEP]
exact ⟨_, hab.to_reflTransGen, hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
⊢ TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : TransGen r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c
[PROOFSTEP]
induction h
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d b✝ : α
a✝ : r a b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b b✝
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ b, r a b ∧ ReflTransGen r b b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝
[PROOFSTEP]
case single c hac => exact ⟨_, hac, by rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d c : α
hac : r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c
[PROOFSTEP]
case single c hac => exact ⟨_, hac, by rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d c : α
hac : r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c
[PROOFSTEP]
exact ⟨_, hac, by rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d c : α
hac : r a c
⊢ ReflTransGen r c c
[PROOFSTEP]
rfl
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ b, r a b ∧ ReflTransGen r b b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝
[PROOFSTEP]
case tail b c _ hbc IH =>
  rcases IH with ⟨d, had, hdb⟩
  exact ⟨_, had, hdb.tail hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : 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
[PROOFSTEP]
case tail b c _ hbc IH =>
  rcases IH with ⟨d, had, hdb⟩
  exact ⟨_, had, hdb.tail hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : 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
[PROOFSTEP]
rcases IH with ⟨d, had, hdb⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c✝ d✝ b c : α
a✝ : TransGen r a b
hbc : r b c
d : α
had : r a d
hdb : ReflTransGen r d b
⊢ ∃ b, r a b ∧ ReflTransGen r b c
[PROOFSTEP]
exact ⟨_, had, hdb.tail hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : Acc r a
⊢ Acc (Relation.TransGen r) a
[PROOFSTEP]
induction' h with x _ H
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
⊢ Acc (Relation.TransGen r) x
[PROOFSTEP]
refine' Acc.intro x fun y hy ↦ _
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y : α
hy : Relation.TransGen r y x
⊢ Acc (Relation.TransGen r) y
[PROOFSTEP]
cases' hy with _ hyx z _ hyz hzx
[GOAL]
case intro.single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y : α
hyx : r y x
⊢ Acc (Relation.TransGen r) y
case intro.tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d x : α
h✝ : ∀ (y : α), r y x → Acc r y
H : ∀ (y : α), r y x → Acc (Relation.TransGen r) y
y z : α
hyz : Relation.TransGen r y z
hzx : r z x
⊢ Acc (Relation.TransGen r) y
[PROOFSTEP]
exacts [H y hyx, (H z hzx).inv hyz]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
trans : Transitive r
a b : α
h : TransGen r a b
⊢ r a b
[PROOFSTEP]
induction h
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝¹ c d : α
trans : Transitive r
a b b✝ : α
a✝ : r a b✝
⊢ r a b✝
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c d : α
trans : Transitive r
a b b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : r a b✝
⊢ r a c✝
[PROOFSTEP]
case single _ hc => exact hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c d : α
trans : Transitive r
a b b✝ : α
hc : r a b✝
⊢ r a b✝
[PROOFSTEP]
case single _ hc => exact hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝¹ c d : α
trans : Transitive r
a b b✝ : α
hc : r a b✝
⊢ r a b✝
[PROOFSTEP]
exact hc
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c d : α
trans : Transitive r
a b b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : r a b✝
⊢ r a c✝
[PROOFSTEP]
case tail c d _ hcd hac => exact trans hac hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d✝ : α
trans : Transitive r
a b c d : α
a✝ : TransGen r a c
hcd : r c d
hac : r a c
⊢ r a d
[PROOFSTEP]
case tail c d _ hcd hac => exact trans hac hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d✝ : α
trans : Transitive r
a b c d : α
a✝ : TransGen r a c
hcd : r c d
hac : r a c
⊢ r a d
[PROOFSTEP]
exact trans hac hcd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
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)
[PROOFSTEP]
induction hab
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ : α
a✝ : r a b✝
⊢ TransGen p (f a) (f b✝)
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen p (f a) (f b✝)
⊢ TransGen p (f a) (f c✝)
[PROOFSTEP]
case single c hac => exact TransGen.single (h a c hac)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c✝ d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
c : α
hac : r a c
⊢ TransGen p (f a) (f c)
[PROOFSTEP]
case single c hac => exact TransGen.single (h a c hac)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c✝ d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
c : α
hac : r a c
⊢ TransGen p (f a) (f c)
[PROOFSTEP]
exact TransGen.single (h a c hac)
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c d : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
b✝ c✝ : α
a✝¹ : TransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : TransGen p (f a) (f b✝)
⊢ TransGen p (f a) (f c✝)
[PROOFSTEP]
case tail c d _ hcd hac => exact TransGen.tail hac (h c d hcd)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d✝ : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
c d : α
a✝ : TransGen r a c
hcd : r c d
hac : TransGen p (f a) (f c)
⊢ TransGen p (f a) (f d)
[PROOFSTEP]
case tail c d _ hcd hac => exact TransGen.tail hac (h c d hcd)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c✝ d✝ : α
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → p (f a) (f b)
c d : α
a✝ : TransGen r a c
hcd : r c d
hac : TransGen p (f a) (f c)
⊢ TransGen p (f a) (f d)
[PROOFSTEP]
exact TransGen.tail hac (h c d hcd)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
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)
[PROOFSTEP]
simpa [transGen_idem] using hab.lift f h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : TransGen r b a
⊢ TransGen (Function.swap r) a b
[PROOFSTEP]
induction' h with b h b c _ hbc ih
[GOAL]
case single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d b : α
h : r b✝ b
⊢ TransGen (Function.swap r) b b✝
[PROOFSTEP]
exact TransGen.single h
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : TransGen r b✝ b
hbc : r b c
ih : TransGen (Function.swap r) b b✝
⊢ TransGen (Function.swap r) c b✝
[PROOFSTEP]
exact ih.head hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : ∀ (b : α), ¬r a b
⊢ ReflTransGen r a b ↔ b = a
[PROOFSTEP]
rw [cases_head_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a
[PROOFSTEP]
simp [h, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
⊢ ReflTransGen r a b ↔ b = a ∨ TransGen r a b
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : ReflTransGen r a b
⊢ b = a ∨ TransGen r a b
[PROOFSTEP]
cases' h with c _ hac hcb
[GOAL]
case refine'_1.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a c d : α
⊢ a = a ∨ TransGen r a a
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case refine'_1.tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c✝ d c : α
hac : ReflTransGen r a c
hcb : r c b
⊢ b = a ∨ TransGen r a b
[PROOFSTEP]
exact Or.inr (TransGen.tail' hac hcb)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : b = a ∨ TransGen r a b
⊢ ReflTransGen r a b
[PROOFSTEP]
rcases h with (rfl | h)
[GOAL]
case refine'_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
b c d : α
⊢ ReflTransGen r b b
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : TransGen r a b
⊢ ReflTransGen r a b
[PROOFSTEP]
exact h.to_reflTransGen
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
refl : Reflexive r
trans : Transitive r
a b : α
h : ReflTransGen r a b
⊢ r a b
[PROOFSTEP]
induction' h with b c _ h₂ IH
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
refl : Reflexive r
trans : Transitive r
a b : α
⊢ r a a
[PROOFSTEP]
apply refl
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝¹ c✝ d : α
refl : Reflexive r
trans : Transitive r
a b✝ b c : α
a✝ : ReflTransGen r a b
h₂ : r b c
IH : r a b
⊢ r a c
[PROOFSTEP]
exact trans IH h₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝ b✝ c d : α
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)
[PROOFSTEP]
simpa [refl_trans_gen_idem] using hab.lift f h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : ReflTransGen r b a
⊢ ReflTransGen (Function.swap r) a b
[PROOFSTEP]
induction' h with b c _ hbc ih
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
⊢ ReflTransGen (Function.swap r) b b
[PROOFSTEP]
rfl
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c✝ d b c : α
a✝ : ReflTransGen r b✝ b
hbc : r b c
ih : ReflTransGen (Function.swap r) b b✝
⊢ ReflTransGen (Function.swap r) c b✝
[PROOFSTEP]
exact ih.head hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
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
[PROOFSTEP]
induction hab
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
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
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : Join (ReflTransGen r) b✝ c
⊢ Join (ReflTransGen r) c✝ c
[PROOFSTEP]
case refl => exact ⟨c, hac, refl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
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
[PROOFSTEP]
case refl => exact ⟨c, hac, refl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
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
[PROOFSTEP]
exact ⟨c, hac, refl⟩
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a c
b✝ c✝ : α
a✝¹ : ReflTransGen r a b✝
a✝ : r b✝ c✝
a_ih✝ : Join (ReflTransGen r) b✝ c
⊢ Join (ReflTransGen r) c✝ c
[PROOFSTEP]
case 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
    case refl => exact ⟨e, refl, ReflGen.single hde⟩
    case tail f b _ hfb ih =>
      rcases ih with ⟨a, hea, hfa⟩
      cases' hfa with _ hfa
      · exact ⟨b, hea.tail hfb, ReflGen.refl⟩
      · rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
        exact ⟨c, hea.trans hac, hbc⟩
  rcases this with ⟨a, hea, hba⟩
  cases' hba with _ hba
  · exact ⟨b, hea, hcb⟩
  · exact ⟨a, hea, hcb.tail hba⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d✝ : α
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
[PROOFSTEP]
case 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
    case refl => exact ⟨e, refl, ReflGen.single hde⟩
    case tail f b _ hfb ih =>
      rcases ih with ⟨a, hea, hfa⟩
      cases' hfa with _ hfa
      · exact ⟨b, hea.tail hfb, ReflGen.refl⟩
      · rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
        exact ⟨c, hea.trans hac, hbc⟩
  rcases this with ⟨a, hea, hba⟩
  cases' hba with _ hba
  · exact ⟨b, hea, hcb⟩
  · exact ⟨a, hea, hcb.tail hba⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d✝ : α
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
[PROOFSTEP]
rcases ih with ⟨b, hdb, hcb⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
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
[PROOFSTEP]
have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
  clear hcb
  induction hdb
  case refl => exact ⟨e, refl, ReflGen.single hde⟩
  case tail f b _ hfb ih =>
    rcases ih with ⟨a, hea, hfa⟩
    cases' hfa with _ hfa
    · exact ⟨b, hea.tail hfb, ReflGen.refl⟩
    · rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
      exact ⟨c, hea.trans hac, hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
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
[PROOFSTEP]
clear hcb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
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
[PROOFSTEP]
induction hdb
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
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
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝¹ c d✝ : α
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 b✝ c✝ : α
a✝¹ : ReflTransGen r d b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ a, ReflTransGen r e a ∧ ReflGen r b✝ a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r c✝ a
[PROOFSTEP]
case refl => exact ⟨e, refl, ReflGen.single hde⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
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
[PROOFSTEP]
case refl => exact ⟨e, refl, ReflGen.single hde⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
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
[PROOFSTEP]
exact ⟨e, refl, ReflGen.single hde⟩
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝¹ c d✝ : α
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 b✝ c✝ : α
a✝¹ : ReflTransGen r d b✝
a✝ : r b✝ c✝
a_ih✝ : ∃ a, ReflTransGen r e a ∧ ReflGen r b✝ a
⊢ ∃ a, ReflTransGen r e a ∧ ReflGen r c✝ a
[PROOFSTEP]
case tail f b _ hfb ih =>
  rcases ih with ⟨a, hea, hfa⟩
  cases' hfa with _ hfa
  · exact ⟨b, hea.tail hfb, ReflGen.refl⟩
  · rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
    exact ⟨c, hea.trans hac, hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝¹ c d✝ : α
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
[PROOFSTEP]
case tail f b _ hfb ih =>
  rcases ih with ⟨a, hea, hfa⟩
  cases' hfa with _ hfa
  · exact ⟨b, hea.tail hfb, ReflGen.refl⟩
  · rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
    exact ⟨c, hea.trans hac, hbc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝¹ c d✝ : α
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
[PROOFSTEP]
rcases ih with ⟨a, hea, hfa⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c d✝ : α
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
[PROOFSTEP]
cases' hfa with _ hfa
[GOAL]
case intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝¹ c d✝ : α
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
[PROOFSTEP]
exact ⟨b, hea.tail hfb, ReflGen.refl⟩
[GOAL]
case intro.intro.single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c d✝ : α
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
[PROOFSTEP]
rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
[GOAL]
case intro.intro.single.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝² b✝¹ c✝ d✝ : α
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
[PROOFSTEP]
exact ⟨c, hea.trans hac, hbc⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
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
[PROOFSTEP]
rcases this with ⟨a, hea, hba⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c d✝ : α
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 : α
hea : ReflTransGen r e a
hba : ReflGen r b a
⊢ Join (ReflTransGen r) e c
[PROOFSTEP]
cases' hba with _ hba
[GOAL]
case intro.intro.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c d✝ : α
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
[PROOFSTEP]
exact ⟨b, hea, hcb⟩
[GOAL]
case intro.intro.intro.intro.single
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a✝¹ b✝ c d✝ : α
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 : α
hea : ReflTransGen r e a
hba : r b a
⊢ Join (ReflTransGen r) e c
[PROOFSTEP]
exact ⟨a, hea, hcb.tail hba⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
h' : ReflTransGen r' a b
⊢ r a b
[PROOFSTEP]
induction' h' with b c _ hbc ih
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b c d : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
⊢ r a a
[PROOFSTEP]
exact hr _
[GOAL]
case tail
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b✝ c✝ d : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
b c : α
a✝ : ReflTransGen r' a b
hbc : r' b c
ih : r a b
⊢ r a c
[PROOFSTEP]
exact ht ih (h _ _ hbc)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
⊢ EqvGen r a b → r a b
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h✝ : Equivalence r
h : EqvGen r a b
⊢ r a b
[PROOFSTEP]
induction h with
| rel => assumption
| refl => exact h.1 _
| symm => apply h.symm; assumption
| trans _ _ _ _ _ hab hbc => exact h.trans hab hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h✝ : Equivalence r
h : EqvGen r a b
⊢ r a b
[PROOFSTEP]
induction h with
| rel => assumption
| refl => exact h.1 _
| symm => apply h.symm; assumption
| trans _ _ _ _ _ hab hbc => exact h.trans hab hbc
[GOAL]
case rel
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : r x✝ y✝
⊢ r x✝ y✝
[PROOFSTEP]

| rel => assumption
[GOAL]
case rel
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : r x✝ y✝
⊢ r x✝ y✝
[PROOFSTEP]
assumption
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ : α
⊢ r x✝ x✝
[PROOFSTEP]

| refl => exact h.1 _
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ : α
⊢ r x✝ x✝
[PROOFSTEP]
exact h.1 _
[GOAL]
case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r y✝ x✝
[PROOFSTEP]

| symm => apply h.symm; assumption
[GOAL]
case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r y✝ x✝
[PROOFSTEP]
apply h.symm
[GOAL]
case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ : α
a✝ : EqvGen r x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝
[PROOFSTEP]
assumption
[GOAL]
case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ z✝ : α
a✝¹ : EqvGen r x✝ y✝
a✝ : EqvGen r y✝ z✝
hab : r x✝ y✝
hbc : r y✝ z✝
⊢ r x✝ z✝
[PROOFSTEP]

| trans _ _ _ _ _ hab hbc => exact h.trans hab hbc
[GOAL]
case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
a b : α
h : Equivalence r
x✝ y✝ z✝ : α
a✝¹ : EqvGen r x✝ y✝
a✝ : EqvGen r y✝ z✝
hab : r x✝ y✝
hbc : r y✝ z✝
⊢ r x✝ z✝
[PROOFSTEP]
exact h.trans hab hbc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
h : EqvGen r a b
⊢ EqvGen p a b
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
h : EqvGen r a b
⊢ EqvGen p a b
[PROOFSTEP]
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
[GOAL]
case rel
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a✝ b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
h : r a b
⊢ EqvGen p a b
[PROOFSTEP]

| rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
[GOAL]
case rel
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a✝ b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
h : r a b
⊢ EqvGen p a b
[PROOFSTEP]
exact EqvGen.rel _ _ (hrp _ _ h)
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
x✝ : α
⊢ EqvGen p x✝ x✝
[PROOFSTEP]

| refl => exact EqvGen.refl _
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a b : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
x✝ : α
⊢ EqvGen p x✝ x✝
[PROOFSTEP]
exact EqvGen.refl _
[GOAL]
case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a✝¹ b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
a✝ : EqvGen r a b
ih : EqvGen p a b
⊢ EqvGen p b a
[PROOFSTEP]

| symm a b _ ih => exact EqvGen.symm _ _ ih
[GOAL]
case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a✝¹ b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b : α
a✝ : EqvGen r a b
ih : EqvGen p a b
⊢ EqvGen p b a
[PROOFSTEP]
exact EqvGen.symm _ _ ih
[GOAL]
case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a✝² b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b c : α
a✝¹ : EqvGen r a b
a✝ : EqvGen r b c
hab : EqvGen p a b
hbc : EqvGen p b c
⊢ EqvGen p a c
[PROOFSTEP]

| trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
[GOAL]
case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
a✝² b✝ : α
r p : α → α → Prop
hrp : ∀ (a b : α), r a b → p a b
a b c : α
a✝¹ : EqvGen r a b
a✝ : EqvGen r b c
hab : EqvGen p a b
hbc : EqvGen p b c
⊢ EqvGen p a c
[PROOFSTEP]
exact EqvGen.trans _ _ _ hab hbc


[GOAL]
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
⊢ CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) ↑toFinsupp
[PROOFSTEP]
rintro s t ⟨u, a, hr, he⟩
[GOAL]
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ u → r a' a
he : s + {a} = t + u
⊢ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) (↑toFinsupp) s t
[PROOFSTEP]
replace hr := fun a' ↦ mt (hr a')
[GOAL]
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
⊢ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) (↑toFinsupp) s t
[PROOFSTEP]
classical
refine ⟨a, fun b h ↦ ?_, ?_⟩ <;> simp_rw [toFinsupp_apply]
· apply_fun count b at he
  simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)] using he
· apply_fun count a at he
  simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)), add_zero] at he
  exact he ▸ Nat.lt_succ_self _
[GOAL]
case intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
⊢ InvImage (Finsupp.Lex (rᶜ ⊓ fun x x_1 => x ≠ x_1) fun x x_1 => x < x_1) (↑toFinsupp) s t
[PROOFSTEP]
refine ⟨a, fun b h ↦ ?_, ?_⟩
[GOAL]
case intro.intro.intro.refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
b : α
h : (rᶜ ⊓ fun x x_1 => x ≠ x_1) b a
⊢ ↑(↑toFinsupp s) b = ↑(↑toFinsupp t) b
[PROOFSTEP]
simp_rw [toFinsupp_apply]
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
⊢ (fun {i} x x_1 => x < x_1) (↑(↑toFinsupp s) a) (↑(↑toFinsupp t) a)
[PROOFSTEP]
simp_rw [toFinsupp_apply]
[GOAL]
case intro.intro.intro.refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
b : α
h : (rᶜ ⊓ fun x x_1 => x ≠ x_1) b a
⊢ count b s = count b t
[PROOFSTEP]
apply_fun count b at he
[GOAL]
case intro.intro.intro.refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
b : α
h : (rᶜ ⊓ fun x x_1 => x ≠ x_1) b a
he : count b (s + {a}) = count b (t + u)
⊢ count b s = count b t
[PROOFSTEP]
simpa only [count_add, count_singleton, if_neg h.2, add_zero, count_eq_zero.2 (hr b h.1)] using he
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
⊢ count a s < count a t
[PROOFSTEP]
apply_fun count a at he
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
he : count a (s + {a}) = count a (t + u)
⊢ count a s < count a t
[PROOFSTEP]
simp only [count_add, count_singleton_self, count_eq_zero.2 (hr _ (irrefl_of r a)), add_zero] at he
[GOAL]
case intro.intro.intro.refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t u : Multiset α
a : α
hr : ∀ (a' : α), ¬r a' a → ¬a' ∈ u
he : count a s + 1 = count a t
⊢ count a s < count a t
[PROOFSTEP]
exact he ▸ Nat.lt_succ_self _
[GOAL]
α : Type u_1
r : α → α → Prop
x' x : α
h✝ : r x' x
a : α
h : a ∈ {x'}
⊢ r a x
[PROOFSTEP]
rwa [mem_singleton.1 h]
[GOAL]
α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ s + t + {x✝} = s + u + x✝¹ ↔ t + {x✝} = u + x✝¹
[PROOFSTEP]
rw [add_assoc, add_assoc, add_left_cancel_iff]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s : Multiset α
⊢ CutExpand r s' s ↔ ∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t
[PROOFSTEP]
simp_rw [CutExpand, add_singleton_eq_iff]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s : Multiset α
⊢ (∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a) ↔
    ∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t
[PROOFSTEP]
refine' exists₂_congr fun t a ↦ ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s t : Multiset α
a : α
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a →
    (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t
[PROOFSTEP]
rintro ⟨ht, ha, rfl⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t
[PROOFSTEP]
obtain h | h := mem_add.1 ha
[GOAL]
case refine'_1.intro.intro.inl
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
h : a ∈ s
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t
case refine'_1.intro.intro.inr
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
ha : a ∈ s + t
h : a ∈ t
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ erase (s + t) a = erase s a + t
[PROOFSTEP]
exacts [⟨ht, h, erase_add_left_pos t h⟩, (@irrefl α r _ a (ht a h)).elim]
[GOAL]
case refine'_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s' s t : Multiset α
a : α
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s ∧ s' = erase s a + t →
    (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ s' = erase (s + t) a
[PROOFSTEP]
rintro ⟨ht, h, rfl⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : IsIrrefl α r
s t : Multiset α
a : α
ht : ∀ (a' : α), a' ∈ t → r a' a
h : a ∈ s
⊢ (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ s + t ∧ erase s a + t = erase (s + t) a
[PROOFSTEP]
exact ⟨ht, mem_add.2 (Or.inl h), (erase_add_left_pos t h).symm⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬CutExpand r s 0
[PROOFSTEP]
classical
rw [cutExpand_iff]
rintro ⟨_, _, _, ⟨⟩, _⟩
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬CutExpand r s 0
[PROOFSTEP]
rw [cutExpand_iff]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
⊢ ¬∃ t a, (∀ (a' : α), a' ∈ t → r a' a) ∧ a ∈ 0 ∧ s = erase 0 a + t
[PROOFSTEP]
rintro ⟨_, _, _, ⟨⟩, _⟩
[GOAL]
α : Type u_1
r✝ r : α → α → Prop
⊢ Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s => s.fst + s.snd
[PROOFSTEP]
rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩
[GOAL]
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = (fun s => s.fst + s.snd) (s₁, s₂) + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ (fun s => s.fst + s.snd) a' = s
[PROOFSTEP]
dsimp at he ⊢
[GOAL]
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
[PROOFSTEP]
classical
  -- Porting note: Originally `obtain ⟨ha, rfl⟩`
    -- This is https://github.com/leanprover/std4/issues/62
obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he
rw [hb]
rw [add_assoc, mem_add] at ha
obtain h | h := ha
· refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩
  · rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
  · rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
· refine' ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, _⟩, _⟩
  · rw [add_comm, singleton_add, cons_erase h]
  · rw [add_assoc, erase_add_right_pos _ h]
[GOAL]
case mk.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
[PROOFSTEP]
obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = s
[PROOFSTEP]
rw [hb]
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
rw [add_assoc, mem_add] at ha
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
ha : a ∈ s₁ ∨ a ∈ s₂ + t
hb : s = erase (s₁ + s₂ + t) a
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
obtain h | h := ha
[GOAL]
case mk.intro.intro.intro.intro.inl
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩
[GOAL]
case mk.intro.intro.intro.intro.inl.refine'_1
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ erase s₁ a + t + {a} = s₁ + t
[PROOFSTEP]
rw [add_comm, ← add_assoc, singleton_add, cons_erase h]
[GOAL]
case mk.intro.intro.intro.intro.inl.refine'_2
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₁
⊢ (erase s₁ a + t, s₂).fst + (erase s₁ a + t, s₂).snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]
[GOAL]
case mk.intro.intro.intro.intro.inr
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.fst + a'.snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
refine' ⟨(s₁, (s₂ + t).erase a), GameAdd.snd ⟨t, a, hr, _⟩, _⟩
[GOAL]
case mk.intro.intro.intro.intro.inr.refine'_1
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ erase (s₂ + t) a + {a} = s₂ + t
[PROOFSTEP]
rw [add_comm, singleton_add, cons_erase h]
[GOAL]
case mk.intro.intro.intro.intro.inr.refine'_2
α : Type u_1
r✝ r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
he : s + {a} = s₁ + s₂ + t
hb : s = erase (s₁ + s₂ + t) a
h : a ∈ s₂ + t
⊢ (s₁, erase (s₂ + t) a).fst + (s₁, erase (s₂ + t) a).snd = erase (s₁ + s₂ + t) a
[PROOFSTEP]
rw [add_assoc, erase_add_right_pos _ h]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
s : Multiset α
hs : ∀ (a : α), a ∈ s → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) s
[PROOFSTEP]
induction s using Multiset.induction
[GOAL]
case empty
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ (a : α), a ∈ 0 → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝¹ : α
s✝ : Multiset α
a✝ : (∀ (a : α), a ∈ s✝ → Acc (CutExpand r) {a}) → Acc (CutExpand r) s✝
hs : ∀ (a : α), a ∈ a✝¹ ::ₘ s✝ → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) (a✝¹ ::ₘ s✝)
[PROOFSTEP]
case empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ (a : α), a ∈ 0 → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0
[PROOFSTEP]
case empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
hs : ∀ (a : α), a ∈ 0 → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0
[PROOFSTEP]
exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
[GOAL]
case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝¹ : α
s✝ : Multiset α
a✝ : (∀ (a : α), a ∈ s✝ → Acc (CutExpand r) {a}) → Acc (CutExpand r) s✝
hs : ∀ (a : α), a ∈ a✝¹ ::ₘ s✝ → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) (a✝¹ ::ₘ s✝)
[PROOFSTEP]
case cons a s ihs =>
  rw [← s.singleton_add a]
  rw [forall_mem_cons] at hs
  exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) (a ::ₘ s)
[PROOFSTEP]
case cons a s ihs =>
  rw [← s.singleton_add a]
  rw [forall_mem_cons] at hs
  exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) (a ::ₘ s)
[PROOFSTEP]
rw [← s.singleton_add a]
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) ({a} + s)
[PROOFSTEP]
rw [forall_mem_cons] at hs
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
s : Multiset α
ihs : (∀ (a : α), a ∈ s → Acc (CutExpand r) {a}) → Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ (x : α), x ∈ s → Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)
[PROOFSTEP]
exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
[GOAL]
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
hacc : Acc r a
⊢ Acc (CutExpand r) {a}
[PROOFSTEP]
induction' hacc with a h ih
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) {a}
[PROOFSTEP]
refine' Acc.intro _ fun s ↦ _
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
⊢ CutExpand r s {a} → Acc (CutExpand r) s
[PROOFSTEP]
classical
simp only [cutExpand_iff, mem_singleton]
rintro ⟨t, a, hr, rfl, rfl⟩
refine' acc_of_singleton fun a' ↦ _
rw [erase_singleton, zero_add]
exact ih a' ∘ hr a'
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
⊢ CutExpand r s {a} → Acc (CutExpand r) s
[PROOFSTEP]
simp only [cutExpand_iff, mem_singleton]
[GOAL]
case intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
⊢ (∃ t a_1, (∀ (a' : α), a' ∈ t → r a' a_1) ∧ a_1 = a ∧ s = erase {a} a_1 + t) → Acc (CutExpand r) s
[PROOFSTEP]
rintro ⟨t, a, hr, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) (erase {a} a + t)
[PROOFSTEP]
refine' acc_of_singleton fun a' ↦ _
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ erase {a} a + t → Acc (CutExpand r) {a'}
[PROOFSTEP]
rw [erase_singleton, zero_add]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
a✝ : α
t : Multiset α
a : α
hr : ∀ (a' : α), a' ∈ t → r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ t → Acc (CutExpand r) {a'}
[PROOFSTEP]
exact ih a' ∘ hr a'


[GOAL]
⊢ ¬UnivLE.{u + 1, u}
[PROOFSTEP]
simp only [Small_iff, not_forall, not_exists, not_nonempty_iff]
[GOAL]
⊢ ∃ x, ∀ (x_1 : Type u), IsEmpty (x ≃ x_1)
[PROOFSTEP]
exact ⟨Type u, fun α => ⟨fun f => Function.not_surjective_Type.{u, u} f.symm f.symm.surjective⟩⟩