Theorem: equiv_reflects_mono (CategoryTheoryExercises/Exercises/Exercise3.lean)

State before:
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
⊢ Mono f
Tactic:
have h := e.functor.map_injective (X := X) (Y := Y)
State after:
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
h : Function.Injective e.functor.map
⊢ Mono f

State before:
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
hef : Mono (e.functor.map f)
h : Function.Injective e.functor.map
⊢ Mono f
Tactic:
cases' hef with hef
State after:
case mk
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
⊢ Mono f

State before:
case mk
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
⊢ Mono f
Tactic:
constructor
State after:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h

State before:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Tactic:
intros W φ ψ h
State after:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h✝ : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ φ = ψ

State before:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h✝ : Function.Injective e.functor.map
hef : ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map f → g = h
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ φ = ψ
Tactic:
specialize @hef (e.functor.obj W) (e.functor.map φ) (e.functor.map ψ)
State after:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h✝ : Function.Injective e.functor.map
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
hef : e.functor.map φ ≫ e.functor.map f = e.functor.map ψ ≫ e.functor.map f → e.functor.map φ = e.functor.map ψ
⊢ φ = ψ

State before:
case mk.right_cancellation
C : Type u
inst✝¹ : Category C
D : Type v
inst✝ : Category D
X Y : C
f : X ⟶ Y
e : C ≌ D
h✝ : Function.Injective e.functor.map
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
hef : e.functor.map φ ≫ e.functor.map f = e.functor.map ψ ≫ e.functor.map f → e.functor.map φ = e.functor.map ψ
⊢ φ = ψ
Tactic:
sorry
State after:
no goals