awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
rw : is2.inv ≫ (functorToAction F).map (Sigma.desc gf) = u'.inv ≫ t.hom ≫ i
⊢ (functorToAction F).map (Sigma.desc gf) = is2.hom ≫ u'.inv ≫ t.hom ≫ i

Tactic:
rw [← Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
⊢ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) = u'.inv ≫ t.hom ≫ i

Tactic:
Sigma.hom_ext _ _ (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.Sigma.hom_ext
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
refine :
  ∀ (j : ι),
    Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫
        is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
      Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i
⊢ is2.inv ≫ (functorToAction F).map (Sigma.desc gf) = u'.inv ≫ t.hom ≫ i

Tactic:
refine Sigma.hom_ext _ _ (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.Sigma.hom_ext
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
j : ι
this : (functorToAction F).map (gf j) = (gu j).inv ≫ i' j
⊢ Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫
      is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
    Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i

Tactic:
simpa [is2, u']
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
j : ι
suffices : (functorToAction F).map (gf j) = (gu j).inv ≫ i' j
⊢ Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫
      is2.inv ≫ (functorToAction F).map (Sigma.desc gf) =
    Sigma.ι (C := Action FintypeCat (Aut F)) (fun (i : ι) ↦ (functorToAction F).obj (gZ i)) j ≫ u'.inv ≫ t.hom ≫ i

Tactic:
suffices (functorToAction F).map (gf j) = (gu j).inv ≫ i' j by
      simpa [is2, u']
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
j : ι
⊢ (functorToAction F).map (gf j) = (gu j).inv ≫ i' j

Tactic:
simp only [h, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
⊢ (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i

Tactic:
have heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i := by
    simp only [Iso.trans_inv, Iso.symm_inv, Category.assoc]
    rw [← Iso.inv_comp_eq]
    refine Sigma.hom_ext _ _ (fun j ↦ ?_)
    suffices (functorToAction F).map (gf j) = (gu j).inv ≫ i' j by
      simpa [is2, u']
    simp only [h, Iso.inv_hom_id_assoc]
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ (t.symm ≪≫ u' ≪≫ is2.symm).hom ≫ (functorToAction F).map (Sigma.desc gf) = i

Tactic:
simp [heq]
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
refine : Mono (X := sigmaObj.{0, v_1, u_1} gZ) (Sigma.desc gf)
⊢ ∃ (Z : C) (f : Z ⟶ X) (u : Y ≅ (functorToAction F).obj Z), Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
refine ⟨∐ gZ, Sigma.desc gf, t.symm ≪≫ u' ≪≫ is2.symm, ?_, by simp [heq]⟩
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ Mono (X := sigmaObj.{0, v_1, u_1} gZ) (Sigma.desc gf)

Tactic:
mono_of_mono_map (functorToAction F) (heq ▸ mono_comp _ _)

Premises used: Eq.rec, CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.mono_comp, CategoryTheory.Functor.mono_of_mono_map, Eq.symm
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst_3 : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun (j : ι) ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : (i : ι) → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h_1 : ∀ (i : ι), IsConnected.{u_1, v_1} (gZ i)
h_2 : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (sigmaObj.{0, v_1, u_1} gZ) ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
u' : ∐ f ≅ ∐ fun (i : ι) ↦ (functorToAction F).obj (gZ i) := Sigma.mapIso gu
heq : (functorToAction F).map (Sigma.desc gf) = (t.symm ≪≫ u' ≪≫ is2.symm).inv ≫ i
⊢ Mono (X := sigmaObj.{0, v_1, u_1} gZ) (Sigma.desc gf)

Tactic:
exact mono_of_mono_map (functorToAction F) (heq ▸ mono_comp _ _)

Premises used: CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
⊢ Mono (u ≫ prod.fst)

Tactic:
have : Mono (u ≫ prod.fst) := prod.lift_fst (𝟙 _) f ▸ inferInstance
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono (u ≫ prod.fst)
⊢ Mono u

Tactic:
have : Mono u := mono_of_mono u prod.fst
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this_1 : Mono (u ≫ prod.fst)
this : Mono u
⊢ Mono i

Tactic:
apply mono_comp u _

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
⊢ Mono i

Tactic:
have : Mono i := by
      have : Mono (u ≫ prod.fst) := prod.lift_fst (𝟙 _) f ▸ inferInstance
      have : Mono u := mono_of_mono u prod.fst
      apply mono_comp u _
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
obtain :
  ∀ (Z : C) (g : Z ⟶ Limits.prod.{v_1, u_1} X Y) (v : (functorToAction F).obj X ≅ (functorToAction F).obj Z),
    Mono g → ∀ (hvgi : v.hom ≫ (functorToAction F).map g = i), ∃ (a : X ⟶ Y), (functorToAction F).map a = f
⊢ ∃ (a : X ⟶ Y), (functorToAction F).map a = f

Tactic:
obtain ⟨Z, g, v, _, hvgi⟩ := exists_lift_of_mono F (Limits.prod X Y)
      ((functorToAction F).obj X) i

Premises used: CategoryTheory.PreGaloisCategory.functorToAction, CategoryTheory.PreGaloisCategory.exists_lift_of_mono, CategoryTheory.Functor.obj, CategoryTheory.Limits.prod
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
⊢ (functorToAction F).map g = v.inv ≫ i

Tactic:
simp [← hvgi]
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
⊢ (functorToAction F).map g = v.inv ≫ i

Tactic:
have hgvi : (functorToAction F).map g = v.inv ≫ i := by simp [← hvgi]
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
simp : IsIso (v.inv ≫ i ≫ (functorToAction F).map prod.fst)
⊢ IsIso ((functorToAction F).map ψ)

Tactic:
simp only [map_comp, hgvi, Category.assoc, ψ]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
h : IsIso (𝟙 ((functorToAction F).obj X))
⊢ IsIso (i ≫ (functorToAction F).map prod.fst)

Tactic:
simpa [i, u]
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
suffices : IsIso (𝟙 ((functorToAction F).obj X))
⊢ IsIso (i ≫ (functorToAction F).map prod.fst)

Tactic:
suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso (𝟙 ((functorToAction F).obj X))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Galois.Full
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F : Functor.{v_1, u, u_1, u + 1} C FintypeCat
inst_1 : GaloisCategory.{u_1, v_1} C
inst_2 : FiberFunctor F
X Y : C
f : (functorToAction F).obj X ⟶ (functorToAction F).obj Y
u : (functorToAction F).obj X ⟶ (functorToAction F).obj X ⨯ (functorToAction F).obj Y :=
  prod.lift (𝟙 ((functorToAction F).obj X)) f
i : (functorToAction F).obj X ⟶ (functorToAction F).obj (Limits.prod.{v_1, u_1} X Y) :=
  u ≫ Iso.inv (PreservesLimitPair.iso (functorToAction F) X Y)
this : Mono i
Z : C
g : Z ⟶ Limits.prod.{v_1, u_1} X Y
v : (functorToAction F).obj X ≅ (functorToAction F).obj Z
left : Mono g
hvgi : v.hom ≫ (functorToAction F).map g = i
ψ : Z ⟶ X := g ≫ prod.fst
hgvi : (functorToAction F).map g = v.inv ≫ i
⊢ IsIso (i ≫ (functorToAction F).map prod.fst)

Tactic:
have : IsIso (i ≫ (functorToAction F).map prod.fst) := by
        suffices h : IsIso (𝟙 ((functorToAction F).obj X)) by simpa [i, u]
        infer_instance