a b c d : Prop
α✝ : Type u
r : α✝ → α✝ → Prop
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
⊢ f = g
a b c d : Prop
α✝ : Type u
r : α✝ → α✝ → Prop
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
⊢ f = g
let eqv (f g : (x : α) → β x) := ∀ x, f x = g x
a b c d : Prop
α✝ : Type u
r : α✝ → α✝ → Prop
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
extfunApp : Quot eqv → (x : α) → β x :=
  fun f x => Quot.liftOn f (fun f => f x) (_ : ∀ (x_1 x_2 : (x : α) → β x), eqv x_1 x_2 → x_1 x = x_2 x)
⊢ f = g
a b c d : Prop
α✝ : Type u
r : α✝ → α✝ → Prop
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
⊢ f = g
let extfunApp (f : Quot eqv) (x : α) : β x :=
  Quot.liftOn f
    (fun (f : ∀ (x : α), β x) => f x)
    (fun _ _ h => h x)
a b c d : Prop
α✝ : Type u
r : α✝ → α✝ → Prop
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
extfunApp : Quot eqv → (x : α) → β x :=
  fun f x => Quot.liftOn f (fun f => f x) (_ : ∀ (x_1 x_2 : (x : α) → β x), eqv x_1 x_2 → x_1 x = x_2 x)
⊢ extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
a b c d : Prop
α✝ : Type u
r : α✝ → α✝ → Prop
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
extfunApp : Quot eqv → (x : α) → β x :=
  fun f x => Quot.liftOn f (fun f => f x) (_ : ∀ (x_1 x_2 : (x : α) → β x), eqv x_1 x_2 → x_1 x = x_2 x)
⊢ f = g
show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
no goals
a b c d : Prop
α✝ : Type u
r : α✝ → α✝ → Prop
α : Sort u
β : α → Sort v
f g : (x : α) → β x
h : ∀ (x : α), f x = g x
eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
extfunApp : Quot eqv → (x : α) → β x :=
  fun f x => Quot.liftOn f (fun f => f x) (_ : ∀ (x_1 x_2 : (x : α) → β x), eqv x_1 x_2 → x_1 x = x_2 x)
⊢ extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
exact congrArg extfunApp (Quot.sound h)