Theorem: equiv_preserves_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
inst✝ : Mono f
e : C ≌ D
⊢ Mono (e.functor.map 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
inst✝ : Mono f
e : C ≌ D
⊢ ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map 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
inst✝ : Mono f
e : C ≌ D
⊢ ∀ {Z : D} (g h : Z ⟶ e.functor.obj X), g ≫ e.functor.map f = h ≫ e.functor.map 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
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ φ = ψ

State before:
case right_cancellation
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ φ = ψ
Tactic:
apply Functor.map_injective e.inverse
State after:
case right_cancellation.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.inverse.map φ = e.inverse.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
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.inverse.map φ = e.inverse.map ψ
Tactic:
apply Mono.right_cancellation (f := (Equivalence.unitInv e).app X)
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
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.inverse.map φ ≫ (Equivalence.unitInv e).app X = e.inverse.map ψ ≫ (Equivalence.unitInv e).app X

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
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.inverse.map φ ≫ (Equivalence.unitInv e).app X = e.inverse.map ψ ≫ (Equivalence.unitInv e).app X
Tactic:
apply Mono.right_cancellation (f := f)
State after:
case right_cancellation.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ (e.inverse.map φ ≫ (Equivalence.unitInv e).app X) ≫ f = (e.inverse.map ψ ≫ (Equivalence.unitInv e).app X) ≫ f

State before:
case right_cancellation.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ (e.inverse.map φ ≫ (Equivalence.unitInv e).app X) ≫ f = (e.inverse.map ψ ≫ (Equivalence.unitInv e).app X) ≫ f
Tactic:
apply e.functor.map_injective
State after:
case right_cancellation.a.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.functor.map ((e.inverse.map φ ≫ (Equivalence.unitInv e).app X) ≫ f) =
    e.functor.map ((e.inverse.map ψ ≫ (Equivalence.unitInv e).app X) ≫ f)

State before:
case right_cancellation.a.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ e.functor.map ((e.inverse.map φ ≫ (Equivalence.unitInv e).app X) ≫ f) =
    e.functor.map ((e.inverse.map ψ ≫ (Equivalence.unitInv e).app X) ≫ f)
Tactic:
simp only [Functor.map_comp]
State after:
case right_cancellation.a.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ (e.functor.map (e.inverse.map φ) ≫ e.functor.map ((Equivalence.unitInv e).app X)) ≫ e.functor.map f =
    (e.functor.map (e.inverse.map ψ) ≫ e.functor.map ((Equivalence.unitInv e).app X)) ≫ e.functor.map f

State before:
case right_cancellation.a.a.a.a
C : Type u
inst✝² : Category C
D : Type v
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
e : C ≌ D
W : D
φ ψ : W ⟶ e.functor.obj X
h : φ ≫ e.functor.map f = ψ ≫ e.functor.map f
⊢ (e.functor.map (e.inverse.map φ) ≫ e.functor.map ((Equivalence.unitInv e).app X)) ≫ e.functor.map f =
    (e.functor.map (e.inverse.map ψ) ≫ e.functor.map ((Equivalence.unitInv e).app X)) ≫ e.functor.map f
Tactic:
simpa
State after:
no goals