-- Mathlib/Order/RelIso/Basic.lean
theorem acc_lift₂_iff {_ : Setoid α} {r : α → α → Prop}
    {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} {a} :
    Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a

Proof state:
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a

Tactic:
constructor

Result:
case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a

case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧

Proof state:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
intro ac

Result:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
ac : Acc r a
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Proof state:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x✝⟧

Tactic:
refine ⟨_, fun q h => ?_⟩

Result:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
q : Quotient x✝¹
h : Quotient.lift₂ r H q ⟦x✝⟧
⊢ Acc (Quotient.lift₂ r H) q

Proof state:
case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a

Tactic:
exact RelHomClass.acc (Quotient.mkRelHom H) a

Result:
no goals

Proof state:
case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
ac : Acc r a
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
induction ac with | intro _ _ IH => ?_

Result:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
⊢ Acc (Quotient.lift₂ r H) ⟦x✝⟧

Proof state:
case mpr.intro.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
a' : α
h : Quotient.lift₂ r H ⟦a'⟧ ⟦x✝⟧
⊢ Acc (Quotient.lift₂ r H) ⟦a'⟧

Tactic:
exact IH a' h

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
q : Quotient x✝¹
h : Quotient.lift₂ r H q ⟦x✝⟧
⊢ Acc (Quotient.lift₂ r H) q

Tactic:
obtain ⟨a', rfl⟩ := q.exists_rep

Result:
case mpr.intro.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
a' : α
h : Quotient.lift₂ r H ⟦a'⟧ ⟦x✝⟧
⊢ Acc (Quotient.lift₂ r H) ⟦a'⟧