-- Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
/-- `toAut` is injective, if only the identity acts trivially on every fiber. -/
lemma toAut_injective_of_non_trivial (h : ∀ (g : G), (∀ (X : C) (x : F.obj X), g • x = x) → g = 1) :
    Function.Injective (toAut F G)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
⊢ (toAut F G).ker ≤ ⊥

Tactic:
intro g (hg : toAut F G g = 1)

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
⊢ g ∈ ⊥

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).carrier
⊢ g • x = x

Tactic:
have : (toAut F G g).hom.app X = 𝟙 (F.obj X) := by
  rw [hg]
  rfl

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).carrier
this : ((toAut F G) g).hom.app X = 𝟙 (F.obj X)
⊢ g • x = x

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).carrier
⊢ (Iso.hom 1).app X = 𝟙 (F.obj X)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
⊢ g ∈ ⊥

Tactic:
refine h g (fun X x ↦ ?_)

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).carrier
⊢ g • x = x

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).carrier
this : ((toAut F G) g).hom.app X = 𝟙 (F.obj X)
⊢ g • x = x

Tactic:
rw [← toAut_hom_app_apply, this, FintypeCat.id_apply]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).carrier
⊢ ((toAut F G) g).hom.app X = 𝟙 (F.obj X)

Tactic:
rw [hg]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
g : G
hg : (toAut F G) g = 1
X : C
x : (F.obj X).carrier
⊢ (Iso.hom 1).app X = 𝟙 (F.obj X)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
⊢ Function.Injective ⇑(toAut F G)

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, eq_bot_iff]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝² : Group G
inst✝¹ : (X : C) → MulAction G (F.obj X).carrier
inst✝ : IsNaturalSMul F G
h : ∀ (g : G), (∀ (X : C) (x : (F.obj X).carrier), g • x = x) → g = 1
⊢ (toAut F G).ker ≤ ⊥