-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- Up to isomorphism an element of the fiber of `X` only lies in one connected component. -/
lemma connected_component_unique {X A B : C} [IsConnected A] [IsConnected B] (a : F.obj A)
    (b : F.obj B) (i : A ⟶ X) (j : B ⟶ X) (h : F.map i a = F.map j b) [Mono i] [Mono j] :
    ∃ (f : A ≅ B), F.map f.hom a = b

Proof state:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
⊢ ∃ f, F.map f.hom a = b

Tactic:
have hn : IsInitial Y → False := not_initial_of_inhabited F y

Result:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
⊢ ∃ f, F.map f.hom a = b

Proof state:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
⊢ pullback.fst ((F ⋙ FintypeCat.incl).map i) ((F ⋙ FintypeCat.incl).map j)
      ((Types.pullbackIsoPullback (F.map i) (F.map j)).inv ⟨(a, b), h⟩) =
    a

Tactic:
erw [Types.pullbackIsoPullback_inv_fst_apply (F.map i) (F.map j)]

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 B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
⊢ F.map ((asIso u).symm ≪≫ asIso v).hom a = b

Tactic:
have hu : G.map u y = a := by
  simp only [u, G, y, e, ← PreservesPullback.iso_hom_fst G, fiberPullbackEquiv,
    Iso.toEquiv_comp, Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply,
    inv_hom_id_apply]
  erw [Types.pullbackIsoPullback_inv_fst_apply (F.map i) (F.map j)]

Result:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
hu : G.map u y = a
⊢ F.map ((asIso u).symm ≪≫ asIso v).hom a = b

Proof state:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
hu : G.map u y = a
hv : G.map v y = b
⊢ (F.map u ≫ F.map ((asIso u).symm ≪≫ asIso v).hom) y = F.map v y

Tactic:
simp only [← F.map_comp, Iso.trans_hom, Iso.symm_hom, asIso_inv, asIso_hom,
  IsIso.hom_inv_id_assoc]

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 B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
hu : G.map u y = a
hv : G.map v y = b
⊢ F.map ((asIso u).symm ≪≫ asIso v).hom (G.map u y) = G.map v y

Tactic:
show (F.toPrefunctor.map u ≫ F.toPrefunctor.map _) y = F.toPrefunctor.map v y

Result:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
inst✝⁵ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝⁴ : FiberFunctor F
X A B : C
inst✝³ : IsConnected A
inst✝² : IsConnected B
a : (F.obj A).carrier
b : (F.obj B).carrier
i : A ⟶ X
j : B ⟶ X
h : F.map i a = F.map j b
inst✝¹ : Mono i
inst✝ : Mono j
Y : C := pullback i j
u : Y ⟶ A := pullback.fst i j
v : Y ⟶ B := pullback.snd i j
G : C ⥤ Type w := F ⋙ FintypeCat.incl
e : (F.obj Y).carrier ≃ { p // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
y : (F.obj Y).carrier := e.symm ⟨(a, b), h⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
hu : G.map u y = a
hv : G.map v y = b
⊢ (F.map u ≫ F.map ((asIso u).symm ≪≫ asIso v).hom) y = F.map v y