-- 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⟩
hn : IsInitial Y → False
this✝ : IsIso u
this : IsIso v
⊢ G.map u y = a

Tactic:
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]

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
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

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
hu : G.map u y = a
⊢ G.map v y = b

Tactic:
simp only [v, G, y, e, ← PreservesPullback.iso_hom_snd G, fiberPullbackEquiv,
  Iso.toEquiv_comp, Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply,
  inv_hom_id_apply]

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
this✝ : IsIso u
this : IsIso v
hu : G.map u y = a
⊢ pullback.snd ((F ⋙ FintypeCat.incl).map i) ((F ⋙ FintypeCat.incl).map j)
      ((Types.pullbackIsoPullback (F.map i) (F.map j)).inv ⟨(a, b), h⟩) =
    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
⊢ ∃ f, F.map f.hom a = b

Tactic:
let v : Y ⟶ B := pullback.snd i j

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
⊢ ∃ 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
⊢ ∃ f, F.map f.hom a = b

Tactic:
let u : Y ⟶ A := pullback.fst i j

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
⊢ ∃ f, F.map f.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 ((asIso u).symm ≪≫ asIso v).hom a = b

Tactic:
rw [← hu, ← hv]

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 ((asIso u).symm ≪≫ asIso v).hom (G.map u y) = G.map v y

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
⊢ ∃ f, F.map f.hom a = b

Tactic:
let y : F.obj Y := e.symm ⟨(a, b), h⟩

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⟩
⊢ ∃ f, F.map f.hom a = b