case mp
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a) → Acc r a

case mpr
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ a)
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a) ↔ Acc r a
constructor
no goals
case mp
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a) → Acc r a
exact RelHomClass.acc (Quotient.mkRelHom H) a
case mpr
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ a)
case mpr
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ a)
intro ac
case mpr.intro
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ y)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ x✝)
case mpr
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ a)
induction' ac with _ _ IH
case mpr.intro
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ y)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ x✝)
case mpr.intro
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ y)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ x✝)
dsimp at IH
case mpr.intro
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ y)
q : Quotient inst✝
h : Quotient.lift₂ r H q (Quotient.mk inst✝ x✝)
⊢ Acc (Quotient.lift₂ r H) q
case mpr.intro
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ y)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ x✝)
refine' ⟨_, fun q h => _⟩
case mpr.intro.intro
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ y)
a' : α
h : Quotient.lift₂ r H (Quotient.mk inst✝ a') (Quotient.mk inst✝ x✝)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a')
case mpr.intro
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ y)
q : Quotient inst✝
h : Quotient.lift₂ r H q (Quotient.mk inst✝ x✝)
⊢ Acc (Quotient.lift₂ r H) q
obtain ⟨a', rfl⟩ := q.exists_rep
no goals
case mpr.intro.intro
α : Type u_1
β : Type ?u.44894
γ : Type ?u.44897
δ : Type ?u.44900
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝ : 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) (Quotient.mk inst✝ y)
a' : α
h : Quotient.lift₂ r H (Quotient.mk inst✝ a') (Quotient.mk inst✝ x✝)
⊢ Acc (Quotient.lift₂ r H) (Quotient.mk inst✝ a')
exact IH a' h