case intro
α : Type u_1
β : Type u_2
γ : Type ?u.13156
δ : Type ?u.13159
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)
α : Type u_1
β : Type u_2
γ : Type ?u.13156
δ : Type ?u.13159
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a : α
ha : Acc rα a
⊢ Acc rβ (f a)
induction' ha with a _ ih
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.13156
δ : Type ?u.13159
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
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.13156
δ : Type ?u.13159
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)
refine' Acc.intro (f a) fun b hr ↦ _
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.13156
δ : Type ?u.13159
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')
case intro
α : Type u_1
β : Type u_2
γ : Type ?u.13156
δ : Type ?u.13159
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
obtain ⟨a', hr', rfl⟩ := fib hr
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.13156
δ : Type ?u.13159
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')
exact ih a' hr'