case refine_1
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ β → α

case refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ ∀ {a b : β}, s a b → r (?refine_1 a) (?refine_1 b)
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ WellFounded r → WellFounded s
refine RelHomClass.wellFounded (RelHom.mk ?_ ?_ : s →r r)
case refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ r (Classical.choose (_ : HasRightInverse f) a) (Classical.choose (_ : HasRightInverse f) b)
case refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ ∀ {a b : β}, s a b → r (Classical.choose (_ : HasRightInverse f) a) (Classical.choose (_ : HasRightInverse f) b)
intro a b h
case refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ s (f (Classical.choose (_ : HasRightInverse f) a)) (f (Classical.choose (_ : HasRightInverse f) b))
case refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ r (Classical.choose (_ : HasRightInverse f) a) (Classical.choose (_ : HasRightInverse f) b)
apply o.2
case h.e'_1
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) a) = a

case h.e'_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
case refine_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ s (f (Classical.choose (_ : HasRightInverse f) a)) (f (Classical.choose (_ : HasRightInverse f) b))
convert h
no goals
case h.e'_1
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) a) = a

case h.e'_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
iterate 2 apply Classical.choose_spec hf.hasRightInverse
no goals
case refine_1
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
⊢ β → α
exact Classical.choose hf.hasRightInverse
no goals
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type ?u.15958
δ : Type ?u.15961
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
f : α → β
hf : Surjective f
o : ∀ {a b : α}, r a b ↔ s (f a) (f b)
a b : β
h : s a b
⊢ f (Classical.choose (_ : HasRightInverse f) b) = b
apply Classical.choose_spec hf.hasRightInverse