-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
/-- `autMap` is surjective, if the source is also Galois. -/
lemma autMap_surjective_of_isGalois {A B : C} [IsGalois A] [IsGalois B] (f : A ⟶ B) :
    Function.Surjective (autMap f)

Proof state:
case h.a
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).carrier
ha' : F.map f a' = F.map σ.hom (F.map f a)
τ : Aut A
hτ : F.map τ.hom a = a'
⊢ (fun f_1 => F.map f_1.hom (F.map f a)) (autMap f τ) = (fun f_1 => F.map f_1.hom (F.map f a)) σ

Tactic:
simp [hτ, ha']

Result:
no goals

Proof state:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ ∃ a, autMap f a = σ

Tactic:
obtain ⟨a', ha'⟩ := surjective_of_nonempty_fiber_of_isConnected F f (F.map σ.hom (F.map f a))

Result:
case intro.intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).carrier
ha' : F.map f a' = F.map σ.hom (F.map f a)
⊢ ∃ a, autMap f a = σ

Proof state:
case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).carrier
ha' : F.map f a' = F.map σ.hom (F.map f a)
τ : Aut A
hτ : F.map τ.hom a = a'
⊢ autMap f τ = σ

Tactic:
apply evaluation_aut_injective_of_isConnected F B (F.map f a)

Result:
case h.a
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).carrier
ha' : F.map f a' = F.map σ.hom (F.map f a)
τ : Aut A
hτ : F.map τ.hom a = a'
⊢ (fun f_1 => F.map f_1.hom (F.map f a)) (autMap f τ) = (fun f_1 => F.map f_1.hom (F.map f a)) σ

Proof state:
case intro.intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).carrier
ha' : F.map f a' = F.map σ.hom (F.map f a)
⊢ ∃ a, autMap f a = σ

Tactic:
obtain ⟨τ, (hτ : F.map τ.hom a = a')⟩ := MulAction.exists_smul_eq (Aut A) a a'

Result:
case intro.intro.intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).carrier
ha' : F.map f a' = F.map σ.hom (F.map f a)
τ : Aut A
hτ : F.map τ.hom a = a'
⊢ ∃ a, autMap f a = σ

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃ a, autMap f a = σ

Tactic:
obtain ⟨a⟩ := nonempty_fiber_of_isConnected F A

Result:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ ∃ a, autMap f a = σ

Proof state:
case intro.intro.intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).carrier
ha' : F.map f a' = F.map σ.hom (F.map f a)
τ : Aut A
hτ : F.map τ.hom a = a'
⊢ ∃ a, autMap f a = σ

Tactic:
use τ

Result:
case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a a' : (F.obj A).carrier
ha' : F.map f a' = F.map σ.hom (F.map f a)
τ : Aut A
hτ : F.map τ.hom a = a'
⊢ autMap f τ = σ

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
⊢ ∃ a, autMap f a = σ

Tactic:
let F := GaloisCategory.getFiberFunctor C

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
⊢ ∃ a, autMap f a = σ

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
⊢ Function.Surjective (autMap f)

Tactic:
intro σ

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
⊢ ∃ a, autMap f a = σ