-- Mathlib/CategoryTheory/Action/Basic.lean
/-- The functor from `Action V H` to `Action V G` induced by a morphism `f : G → H` is full
if `f` is surjective. -/
lemma full_res (f_surj : Function.Surjective f) : (res V f).Full where
  map_surjective {X} {Y} g

Proof state:
case w.intro
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
⊢ X.ρ (f a) ≫ g.hom = g.hom ≫ Y.ρ (f a)

Tactic:
have : X.ρ (f a) = ((res V f).obj X).ρ a := rfl

Result:
case w.intro
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
this : X.ρ (f a) = ((res V f).obj X).ρ a
⊢ X.ρ (f a) ≫ g.hom = g.hom ≫ Y.ρ (f a)

Proof state:
case w.intro
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
this : X.ρ (f a) = ((res V f).obj X).ρ a
⊢ X.ρ (f a) ≫ g.hom = g.hom ≫ Y.ρ (f a)

Tactic:
rw [this, g.comm a]

Result:
case w.intro
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
this : X.ρ (f a) = ((res V f).obj X).ρ a
⊢ g.hom ≫ ((res V f).obj Y).ρ a = g.hom ≫ Y.ρ (f a)

Proof state:
case w
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
h : H
⊢ X.ρ h ≫ g.hom = g.hom ≫ Y.ρ h

Tactic:
obtain ⟨a, rfl⟩ := f_surj h

Result:
case w.intro
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
⊢ X.ρ (f a) ≫ g.hom = g.hom ≫ Y.ρ (f a)

Proof state:
case w.intro
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
a : G
this : X.ρ (f a) = ((res V f).obj X).ρ a
⊢ g.hom ≫ ((res V f).obj Y).ρ a = g.hom ≫ Y.ρ (f a)

Tactic:
simp

Result:
no goals

Proof state:
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ (res V f).map { hom := g.hom, comm := ⋯ } = g

Tactic:
ext

Result:
case h.h
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ ((res V f).map { hom := g.hom, comm := ⋯ }).hom = g.hom

Proof state:
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ ∃ a, (res V f).map a = g

Tactic:
use ⟨g.hom, fun h ↦ ?_⟩

Result:
case h
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ (res V f).map { hom := g.hom, comm := ⋯ } = g

case w
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
h : H
⊢ X.ρ h ≫ g.hom = g.hom ≫ Y.ρ h

Proof state:
case h.h
V : Type (u + 1)
inst✝² : LargeCategory V
G H : Type u
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ ((res V f).map { hom := g.hom, comm := ⋯ }).hom = g.hom

Tactic:
simp

Result:
no goals