case tfae_1_to_2
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
⊢ Acc r a → WellFoundedOn {b | ReflTransGen r b a} r

ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
tfae_have 1 → 2
case tfae_2_to_3
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
⊢ WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r

ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
tfae_have 2 → 3
case tfae_3_to_1
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
⊢ WellFoundedOn {b | TransGen r b a} r → Acc r a

ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
tfae_3_to_1 : WellFoundedOn {b | TransGen r b a} r → Acc r a
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
tfae_have 3 → 1
no goals
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
tfae_3_to_1 : WellFoundedOn {b | TransGen r b a} r → Acc r a
⊢ TFAE [Acc r a, WellFoundedOn {b | ReflTransGen r b a} r, WellFoundedOn {b | TransGen r b a} r]
tfae_finish
case tfae_1_to_2
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
h : Acc r a
b : ↑{b | ReflTransGen r b a}
⊢ Acc r ↑b
case tfae_1_to_2
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
⊢ Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
refine fun h => ⟨fun b => InvImage.accessible _ ?_⟩
case tfae_1_to_2
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
⊢ Acc (TransGen r) ↑b
case tfae_1_to_2
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
h : Acc r a
b : ↑{b | ReflTransGen r b a}
⊢ Acc r ↑b
rw [← acc_transGen_iff] at h ⊢
case tfae_1_to_2.inl
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : a = ↑b
⊢ Acc (TransGen r) ↑b

case tfae_1_to_2.inr
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : TransGen r (↑b) a
⊢ Acc (TransGen r) ↑b
case tfae_1_to_2
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
⊢ Acc (TransGen r) ↑b
obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2
no goals
case tfae_1_to_2.inl
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : a = ↑b
⊢ Acc (TransGen r) ↑b
rwa [h'] at h
no goals
case tfae_1_to_2.inr
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : TransGen r (↑b) a
⊢ Acc (TransGen r) ↑b
exact h.inv h'
no goals
case tfae_2_to_3
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
⊢ WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
exact fun h => h.subset fun _ => TransGen.to_reflTransGen
case tfae_3_to_1
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
h : WellFoundedOn {b | TransGen r b a} r
b : α
hb : r b a
⊢ Fibration (fun a_1 b => r ↑a_1 ↑b) r Subtype.val
case tfae_3_to_1
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
⊢ WellFoundedOn {b | TransGen r b a} r → Acc r a
refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
no goals
case tfae_3_to_1
ι : Type ?u.5635
α✝ : Type ?u.5638
β : Type ?u.5641
r✝ r' : α✝ → α✝ → Prop
s t : Set α✝
x y : α✝
α : Type u_1
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → WellFoundedOn {b | ReflTransGen r b a} r
tfae_2_to_3 : WellFoundedOn {b | ReflTransGen r b a} r → WellFoundedOn {b | TransGen r b a} r
h : WellFoundedOn {b | TransGen r b a} r
b : α
hb : r b a
⊢ Fibration (fun a_1 b => r ↑a_1 ↑b) r Subtype.val
exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩