[GOAL]
α β : Type u
f g : α ⟶ β
h : ∀ (a : α), f a = g a
⊢ f = g
[PROOFSTEP]
funext x
[GOAL]
case h
α β : Type u
f g : α ⟶ β
h : ∀ (a : α), f a = g a
x : α
⊢ f x = g x
[PROOFSTEP]
exact h x
[GOAL]
α β γ : Type u
f : α → β
g : β → γ
inst✝ : IsIso (↾f)
⊢ Mono (↾f)
[PROOFSTEP]
infer_instance
[GOAL]
α β γ : Type u
f : α → β
g : β → γ
inst✝ : IsIso (↾f)
⊢ ↾f ≫ inv (↾f) = 𝟙 α
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Type w
X Y Z : C
σ : F ⟶ G
τ : G ⟶ H
f : X ⟶ Y
g : Y ⟶ Z
a : F.obj X
⊢ F.map (f ≫ g) a = F.map g (F.map f a)
[PROOFSTEP]
simp [types_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Type w
X Y Z : C
σ : F ⟶ G
τ : G ⟶ H
a : F.obj X
⊢ F.map (𝟙 X) a = a
[PROOFSTEP]
simp [types_id]
[GOAL]
X : Type u
x y : X
⊢ x = y → homOfElement x = homOfElement y
[PROOFSTEP]
aesop
[GOAL]
X Y : Type u
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective f
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
⊢ Mono f → Function.Injective f
[PROOFSTEP]
intro H x x' h
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : f x = f x'
⊢ x = x'
[PROOFSTEP]
skip
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : f x = f x'
⊢ x = x'
[PROOFSTEP]
rw [← homOfElement_eq_iff] at h ⊢
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
H : Mono f
x x' : X
h : homOfElement (f x) = homOfElement (f x')
⊢ homOfElement x = homOfElement x'
[PROOFSTEP]
exact (cancel_mono f).mp h
[GOAL]
case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Injective f → Mono f
[PROOFSTEP]
exact fun H => ⟨fun g g' h => H.comp_left h⟩
[GOAL]
X Y : Type u
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective f
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : Type u
f : X ⟶ Y
⊢ Epi f → Function.Surjective f
[PROOFSTEP]
rintro ⟨H⟩
[GOAL]
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
⊢ Function.Surjective f
[PROOFSTEP]
refine' Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => _
[GOAL]
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ g₁ = g₂
[PROOFSTEP]
rw [← Equiv.ulift.symm.injective.comp_left.eq_iff]
[GOAL]
case mp.mk
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ (fun x x_1 => x ∘ x_1) (↑Equiv.ulift.symm) g₁ = (fun x x_1 => x ∘ x_1) (↑Equiv.ulift.symm) g₂
[PROOFSTEP]
apply H
[GOAL]
case mp.mk.a
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ f ≫ (fun x x_1 => x ∘ x_1) (↑Equiv.ulift.symm) g₁ = f ≫ (fun x x_1 => x ∘ x_1) (↑Equiv.ulift.symm) g₂
[PROOFSTEP]
change ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f
[GOAL]
case mp.mk.a
X Y : Type u
f : X ⟶ Y
H : ∀ {Z : Type u} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
g₁ g₂ : Y → Prop
hg : g₁ ∘ f = g₂ ∘ f
⊢ ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f
[PROOFSTEP]
rw [hg]
[GOAL]
case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Surjective f → Epi f
[PROOFSTEP]
exact fun H => ⟨fun g g' h => H.injective_comp_right h⟩
[GOAL]
m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
⊢ { obj := m, map := fun {X Y} f => Functor.map f }.map (𝟙 α) =
    𝟙 ({ obj := m, map := fun {X Y} f => Functor.map f }.obj α)
[PROOFSTEP]
funext X
[GOAL]
case h
m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
X : { obj := m, map := fun {X Y} f => Functor.map f }.obj α
⊢ { obj := m, map := fun {X Y} f => Functor.map f }.map (𝟙 α) X =
    𝟙 ({ obj := m, map := fun {X Y} f => Functor.map f }.obj α) X
[PROOFSTEP]
apply id_map
