Theorem: equiv_reflects_mono (CategoryTheoryExercises/Solutions/Solution3.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:
constructor
State after:
case right_cancellation
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)
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h

State before:
case right_cancellation
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)
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Tactic:
intros W φ ψ h
State after:
case right_cancellation
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)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ φ = ψ

State before:
case right_cancellation
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)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ φ = ψ
Tactic:
apply e.functor.map_injective
State after:
case right_cancellation.a
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)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ e.functor.map φ = e.functor.map ψ

State before:
case right_cancellation.a
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)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ e.functor.map φ = e.functor.map ψ
Tactic:
apply hef.1
State after:
case right_cancellation.a.a
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)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ e.functor.map φ ≫ e.functor.map f = e.functor.map ψ ≫ e.functor.map f

State before:
case right_cancellation.a.a
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)
W : C
φ ψ : W ⟶ X
h : φ ≫ f = ψ ≫ f
⊢ e.functor.map φ ≫ e.functor.map f = e.functor.map ψ ≫ e.functor.map f
Tactic:
rw [← Functor.map_comp, ← Functor.map_comp, h]
State after:
no goals