-- Mathlib/Order/WellFoundedSet.lean
theorem acc_iff_wellFoundedOn {α} {r : α → α → Prop} {a : α} :
    TFAE [Acc r a,
      WellFoundedOn { b | ReflTransGen r b a } r,
      WellFoundedOn { b | TransGen r b a } r]

Proof state:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
h : {b | TransGen r b a}.WellFoundedOn r
b : α
hb : r b a
⊢ Fibration (fun a_1 b => r ↑a_1 ↑b) r Subtype.val

Tactic:
exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩

Result:
no goals

Proof state:
case inl
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : a = ↑b
⊢ Acc (TransGen r) ↑b

Tactic:
rwa [h'] at h

Result:
no goals

Proof state:
α : Type u_6
r : α → α → Prop
a : α
⊢ Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r

Tactic:
refine fun h => ⟨fun b => InvImage.accessible _ ?_⟩

Result:
α : Type u_6
r : α → α → Prop
a : α
h : Acc r a
b : ↑{b | ReflTransGen r b a}
⊢ Acc r ↑b

Proof state:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE

Tactic:
tfae_have 2 → 3 := fun h => h.subset fun _ => TransGen.to_reflTransGen

Result:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE

Proof state:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
⊢ {b | TransGen r b a}.WellFoundedOn r → Acc r a

Tactic:
refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)

Result:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
h : {b | TransGen r b a}.WellFoundedOn r
b : α
hb : r b a
⊢ Fibration (fun a_1 b => r ↑a_1 ↑b) r Subtype.val

Proof state:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
tfae_3_to_1 : {b | TransGen r b a}.WellFoundedOn r → Acc r a
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
α : Type u_6
r : α → α → Prop
a : α
h : Acc r a
b : ↑{b | ReflTransGen r b a}
⊢ Acc r ↑b

Tactic:
rw [← acc_transGen_iff] at h ⊢

Result:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
⊢ Acc (TransGen r) ↑b

Proof state:
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
⊢ Acc (TransGen r) ↑b

Tactic:
obtain h' | h' := reflTransGen_iff_eq_or_transGen.1 b.2

Result:
case inl
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : a = ↑b
⊢ Acc (TransGen r) ↑b

case inr
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : TransGen r (↑b) a
⊢ Acc (TransGen r) ↑b

Proof state:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE

Tactic:
tfae_have 3 → 1 := by
  refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
  exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩

Result:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : Acc r a → {b | ReflTransGen r b a}.WellFoundedOn r
tfae_2_to_3 : {b | ReflTransGen r b a}.WellFoundedOn r → {b | TransGen r b a}.WellFoundedOn r
tfae_3_to_1 : {b | TransGen r b a}.WellFoundedOn r → Acc r a
⊢ [Acc r a, {b | ReflTransGen r b a}.WellFoundedOn r, {b | TransGen r b a}.WellFoundedOn r].TFAE

Proof state:
case inr
α : Type u_6
r : α → α → Prop
a : α
h : Acc (TransGen r) a
b : ↑{b | ReflTransGen r b a}
h' : TransGen r (↑b) a
⊢ Acc (TransGen r) ↑b

Tactic:
exact h.inv h'

Result:
no goals