case mp
X Y : Type u
f : X ⟶ Y
⊢ Epi f → Function.Surjective f

case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Surjective f → Epi f
X Y : Type u
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective f
constructor
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
case mp
X Y : Type u
f : X ⟶ Y
⊢ Epi f → Function.Surjective f
rintro ⟨H⟩
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₂
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
refine' Function.surjective_of_right_cancellable_Prop fun g₁ g₂ hg => _
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₂
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₂
rw [← Equiv.ulift.symm.injective.comp_left.eq_iff]
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₂
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₂
apply H
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
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₂
change ULift.up ∘ g₁ ∘ f = ULift.up ∘ g₂ ∘ f
no goals
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
rw [hg]
no goals
case mpr
X Y : Type u
f : X ⟶ Y
⊢ Function.Surjective f → Epi f
exact fun H => ⟨fun g g' h => H.injective_comp_right h⟩