-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
/-- For a morphism from a connected object `A` to a Galois object `B` and an automorphism
of `A`, there exists a unique automorphism of `B` making the canonical diagram commute. -/
lemma exists_autMap {A B : C} (f : A ⟶ B) [IsConnected A] [IsGalois B] (σ : Aut A) :
    ∃! (τ : Aut B), f ≫ τ.hom = σ.hom ≫ f

Proof state:
case intro.refine_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ (fun τ => f ≫ τ.hom = σ.hom ≫ f) ((evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a))

Tactic:
apply evaluation_injective_of_isConnected F A B a

Result:
case intro.refine_2.a
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ (fun f => F.map f a) (f ≫ ((evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)).hom) =
    (fun f => F.map f a) (σ.hom ≫ f)

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

Tactic:
simpa using congr_fun (F.congr_map hτ) a

Result:
no goals

Proof state:
case intro.refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ ∀ (y : Aut B),
    (fun τ => f ≫ τ.hom = σ.hom ≫ f) y → y = (evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)

Tactic:
intro τ hτ

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

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

Tactic:
let F := GaloisCategory.getFiberFunctor C

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

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

Tactic:
exact (evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)

Result:
no goals

Proof state:
case intro.refine_2.a
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ (fun f => F.map f a) (f ≫ ((evaluationEquivOfIsGalois F B (F.map f a)).symm (F.map (σ.hom ≫ f) a)).hom) =
    (fun f => F.map f a) (σ.hom ≫ f)

Tactic:
simp

Result:
no goals

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

Tactic:
refine ⟨?_, ?_, ?_⟩

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

case intro.refine_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ (fun τ => f ≫ τ.hom = σ.hom ≫ f) ?intro.refine_1

case intro.refine_3
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ ∀ (y : Aut B), (fun τ => f ≫ τ.hom = σ.hom ≫ f) y → y = ?intro.refine_1

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

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

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

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

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
f : A ⟶ B
inst✝¹ : IsConnected A
inst✝ : IsGalois B
σ : Aut A
F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C
a : (F.obj A).carrier
⊢ ∃! τ, f ≫ τ.hom = σ.hom ≫ f