-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- Key technical lemma: the twisted inclusion `selfProdPermIncl h b` maps `a` to `F.map u b`. -/
private lemma selfProdTermIncl_fib_eq (b : F.obj A) :
    F.map u b = F.map (selfProdPermIncl h b) a

Proof state:
case h.convert_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).carrier
t : (F.obj X).carrier
⊢ F.map (CategoryTheory.PreGaloisCategory.selfProdProj u t) b =
    (ConcreteCategory.hom (F.map (Pi.π (fun x => X) t)))
      (F.map (Pi.map' ⇑(CategoryTheory.PreGaloisCategory.fiberPerm h b) fun j => (Iso.refl X).hom)
        (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X))

Tactic:
convert_to F.map (selfProdProj u t) b =
  (F.map (Pi.map' (fiberPerm h b) fun _ ↦ 𝟙 X) ≫
  F.map (Pi.π (fun _ ↦ X) t)) (mkSelfProdFib F X)

Result:
case h.convert_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).carrier
t : (F.obj X).carrier
⊢ F.map (CategoryTheory.PreGaloisCategory.selfProdProj u t) b =
    (F.map (Pi.map' ⇑(CategoryTheory.PreGaloisCategory.fiberPerm h b) fun x => 𝟙 X) ≫ F.map (Pi.π (fun x => X) t))
      (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).carrier
⊢ F.map u b = F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a

Tactic:
apply Concrete.Pi.map_ext _ F

Result:
case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).carrier
⊢ ∀ (i : (F.obj X).carrier),
    (ConcreteCategory.hom (F.map (Pi.π (fun x => X) i))) (F.map u b) =
      (ConcreteCategory.hom (F.map (Pi.π (fun x => X) i)))
        (F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a)

Proof state:
case h.e'_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).carrier
t : (F.obj X).carrier
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x => X) t))) (F.map u b) =
    F.map (CategoryTheory.PreGaloisCategory.selfProdProj u t) b

Tactic:
simp only [selfProdProj, map_comp, FintypeCat.comp_apply]

Result:
case h.e'_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X
a : (F.obj A).carrier
h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).carrier
t : (F.obj X).carrier
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x => X) t))) (F.map u b) = F.map (Pi.π (fun x => X) t) (F.map u b)