-- 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 (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a)

Tactic:
dsimp only [selfProdPermIncl, Pi.whiskerEquiv]

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 =
    (ConcreteCategory.hom (F.map (Pi.π (fun x => X) t)))
      (F.map (u ≫ Pi.map' ⇑(CategoryTheory.PreGaloisCategory.fiberPerm h b) fun j => (Iso.refl X).hom) 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 =
    (F.map (Pi.map' ⇑(CategoryTheory.PreGaloisCategory.fiberPerm h b) fun x => 𝟙 X) ≫ F.map (Pi.π (fun x => X) t))
      (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X)

Tactic:
rw [← map_comp, Pi.map'_comp_π, Category.comp_id, mkSelfProdFib_map_π F X (fiberPerm h b t)]

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 = (CategoryTheory.PreGaloisCategory.fiberPerm h b) t

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 (u ≫ Pi.map' ⇑(CategoryTheory.PreGaloisCategory.fiberPerm h b) fun j => (Iso.refl X).hom) a)

Tactic:
rw [map_comp, FintypeCat.comp_apply, h]

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 =
    (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))

Proof state:
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)

Tactic:
intro (t : F.obj X)

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
t : (F.obj X).carrier
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x => X) t))) (F.map u b) =
    (ConcreteCategory.hom (F.map (Pi.π (fun x => X) t)))
      (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 (Pi.π (fun x => X) t) (F.map u b)

Tactic:
rfl

Result:
no goals

Proof state:
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
t : (F.obj X).carrier
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun x => X) t))) (F.map u b) =
    (ConcreteCategory.hom (F.map (Pi.π (fun x => X) t)))
      (F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a)

Tactic:
convert_to F.map (selfProdProj u t) b = _

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 (CategoryTheory.PreGaloisCategory.selfProdProj u t) b

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 (CategoryTheory.PreGaloisCategory.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 = (CategoryTheory.PreGaloisCategory.fiberPerm h b) t

Tactic:
rfl

Result:
no goals