mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x ↦ (f a).get ⋯ = x → C a) ((f a).get ⋯)
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction h' fun a' h ih ↦
        Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → (fun x ↦ C x) a') ((f a').get ⋯)
          (fun b' e ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun a'' e ↦
            have e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)

Tactic:
refine Eq.rec (motive := fun x e =>
      Sum.casesOn (motive := fun y => (f a).get (dom_of_mem_fix h) = y → C a) x ?_ ?_
      (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = _) ?_
    (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm

Goal state after:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun y ↦ (f a).get ⋯ = y → C a) (Sum.inr a')
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction h' fun a' h ih ↦
        Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → (fun x ↦ C x) a') ((f a').get ⋯)
          (fun b' e ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun a'' e ↦
            have e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a b : α
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a =
    ((pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a)) ≫ g₂) ≫
      Sigma.desc e

Tactic:
(Category.assoc _ _ g₂),

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π
a b : α
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a =
    (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a) ≫ g₂) ≫
      Sigma.desc e
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
a b : α
hg :
  (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    ((pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a)) ≫ g₂) ≫
      Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b

Tactic:
(Category.assoc _ _ g₂),

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝³ : HasCoproduct X
inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)
inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a ↦ pullback g (Sigma.ι X a)
inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a ↦ pullback.fst g (Sigma.ι X a))
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
g₁ g₂ : Z ⟶ ∐ fun b ↦ X b
a b : α
hg :
  (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a) ≫ g₂) ≫
      Sigma.desc π
⊢ (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a =
    pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
hab : a = b
R : 𝒮
hR : p.obj a = R
⊢ p.IsHomLift (𝟙 R) (eqToHom hab)

Tactic:
subst hR hab

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsCocartesian f φ
⊢ IsCocartesian.map p f φ φ = 𝟙 b

Tactic:
subst_hom_lift p f φ; symm
  apply map_uniq
  simp only [comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsStronglyCocartesian f φ
⊢ map p f φ ⋯ φ = 𝟙 b

Tactic:
subst_hom_lift p f φ; symm
  apply map_uniq
  simp only [comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : (𝟭 D₁).map (β.app X₂) ≫ η.app ((L₂ ⋙ F').obj X₂) = η.app ((F ⋙ L₁).obj X₂) ≫ (G' ⋙ F').map (β.app X₂)
eq₂ : F'.map (G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂)) = F'.map (α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂))
⊢ (β ≫
          L₂.whiskerLeft
            (F'.leftUnitor.inv ≫
              F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom)).app
      X₂ =
    (β ≫ L₂.whiskerLeft (𝟙 F')).app X₂

Tactic:
have eq₃ := β.naturality (adj.counit.app X₂)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : (𝟭 D₁).map (β.app X₂) ≫ η.app ((L₂ ⋙ F').obj X₂) = η.app ((F ⋙ L₁).obj X₂) ≫ (G' ⋙ F').map (β.app X₂)
eq₂ : F'.map (G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂)) = F'.map (α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂))
eq₃ :
  (F ⋙ L₁).map (adj.counit.app X₂) ≫ β.app ((𝟭 C₂).obj X₂) = β.app ((F ⋙ G).obj X₂) ≫ (L₂ ⋙ F').map (adj.counit.app X₂)
⊢ (β ≫
          L₂.whiskerLeft
            (F'.leftUnitor.inv ≫
              F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom)).app
      X₂ =
    (β ≫ L₂.whiskerLeft (𝟙 F')).app X₂
Module: Mathlib.CategoryTheory.Galois.Examples

Goal state before:
pp: case h
G : Type u
inst✝¹ : Group G
X : Action FintypeCat G
inst✝ : IsConnected X
x y : X.V.obj
T : Set X.V.obj := ⋯
this✝² : Fintype ↑T
this✝¹ : MulAction G (FintypeCat.of ↑T).obj := ⋯
T' : Action FintypeCat G := ⋯
i : T' ⟶ X := ⋯
this✝ : Mono i
this : IsIso i
hb : Function.Bijective ⇑(ConcreteCategory.hom i.hom)
y' : X.V.obj
g : G
hg : g • x = y'
hy' : y' = y
⊢ g • x = y

Tactic:
exact hg.trans hy'

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
⊢ Nat.card (F.obj (X ⨿ Y)).obj = Nat.card (F.obj X).obj + Nat.card (F.obj Y).obj

Tactic:
let e : F.obj (X ⨿ Y) ≃ F.obj X ⊕ F.obj Y := Iso.toEquiv
    <| (PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm.trans
    <| Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
e : (F.obj (X ⨿ Y)).obj ≃ (F.obj X).obj ⊕ (F.obj Y).obj :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).obj = Nat.card (F.obj X).obj + Nat.card (F.obj Y).obj
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case pos
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
h : IsConnected X
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
exact has_decomp_connected_components_aux_conn X

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Decomposition

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

Tactic:
← map_comp,

Goal state after:
case convert_2
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
inst✝ : IsConnected A
b : (F.obj A).obj
t : (F.obj X).obj
⊢ (ConcreteCategory.hom (F.map (selfProdProj u t))) b =
    (ConcreteCategory.hom (F.map ((Pi.map' ⇑(fiberPerm h b) fun x ↦ 𝟙 X) ≫ Pi.π (fun x ↦ X) t))) (mkSelfProdFib F X)
Module: Mathlib.CategoryTheory.Galois.Equivalence

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
⊢ (functorToContAction F).EssSurj

Tactic:
have : (functorToContAction F').EssSurj := inferInstance

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
F' : C ⥤ FintypeCat := F ⋙ FintypeCat.uSwitch
this✝ : FiberFunctor F' := FiberFunctor.comp_right FintypeCat.uSwitch
this : (functorToContAction F').EssSurj
⊢ (functorToContAction F).EssSurj
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S : Set (Aut F)
⊢ (∃ t ⊆ S, IsOpen t ∧ 1 ∈ t) → ∃ i, True ∧ ↑(MulAction.stabilizer (Aut F) i.pt) ⊆ S

Tactic:
intro ⟨U, hU, hUopen, hUone⟩
      obtain ⟨I, _, hc, hmem⟩ := exists_set_ker_evaluation_subset_of_isOpen F hUone hUopen
      let P : C := ∏ᶜ fun X : I ↦ X.val
      obtain ⟨A, a, hgal, hbij⟩ := exists_galois_representative F P
      refine ⟨⟨A, a, hgal⟩, trivial, ?_⟩
      intro t (ht : t.hom.app A a = a)
      apply hU
      apply hmem
      have (X : I) : IsConnected X.val := hc X.val X.property
      have (X : I) : Nonempty (F.obj X.val) := nonempty_fiber_of_isConnected F X
      intro X
      ext x
      simp only [FintypeCat.id_apply]
      obtain ⟨z, rfl⟩ :=
        surjective_of_nonempty_fiber_of_isConnected F (Pi.π (fun X : I ↦ X.val) X) x
      obtain ⟨f, rfl⟩ := hbij.surjective z
      rw [NatTrans.naturality_apply, NatTrans.naturality_apply, ht]

Goal state after:
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
m : ↥V ⧸ (↑U).subgroupOf ↑V
x : Aut F ⧸ ↑U
⊢ (ConcreteCategory.hom
        (u.inv ≫
            (functorToAction F).map ((quotientDiag V h u).map m) ≫ u.hom ≫ quotientToQuotientOfLE (↑V) (↑U) hUinV).hom)
      x =
    (ConcreteCategory.hom (quotientToQuotientOfLE (↑V) (↑U) hUinV).hom) x

Tactic:
induction m, x using Quotient.inductionOn₂ with

Goal state after:
case h
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : CompactSpace G
V U : OpenSubgroup (Aut F)
h : (↑U).Normal
A : C
u : (functorToAction F).obj A ≅ ofMulAction (Aut F) (FintypeCat.of (Aut F ⧸ ↑U))
hUinV : U ≤ V
σ : ↥↑V
μ : Aut F
⊢ (ConcreteCategory.hom
        (u.inv ≫
            (functorToAction F).map ((quotientDiag V h u).map ⟦σ⟧) ≫
              u.hom ≫ quotientToQuotientOfLE (↑V) (↑U) hUinV).hom)
      ⟦μ⟧ =
    (ConcreteCategory.hom (quotientToQuotientOfLE (↑V) (↑U) hUinV).hom) ⟦μ⟧
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := fun X ↦ gi X • ↑(MulAction.stabilizer G X.pt)
c : Set G := ⋂ i, cl i
⊢ (Set.univ ∩ c).Nonempty

Tactic:
apply CompactSpace.isCompact_univ.inter_iInter_nonempty

Goal state after:
case htc
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := ⋯
c : Set G := ⋯
⊢ ∀ (i : PointedGaloisObject F), IsClosed (cl i)

case hst
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := ⋯
c : Set G := ⋯
⊢ ∀ (u : Finset (PointedGaloisObject F)), (Set.univ ∩ ⋂ i ∈ u, cl i).Nonempty
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this : HomRel.CompClosure redStep (q ≫ q.reverse) (q ≫ f.toPath ≫ (reverse f).toPath ≫ q.reverse)
⊢ HomRel.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath.comp q.reverse)

Tactic:
change HomRel.CompClosure redStep (q ≫ Quiver.Path.reverse q)
        (Quiver.Path.cons q f ≫ (Quiver.Hom.toPath (Quiver.reverse f)) ≫ (Quiver.Path.reverse q))

Goal state after:
case cons.a
V : Type u
inst✝ : Quiver V
X Y b✝ c✝ : Paths (Symmetrify V)
q : Path X b✝
f : b✝ ⟶ c✝
ih : EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)
this : HomRel.CompClosure redStep (q ≫ q.reverse) (q ≫ f.toPath ≫ (reverse f).toPath ≫ q.reverse)
⊢ HomRel.CompClosure redStep (q ≫ q.reverse) (q.cons f ≫ (reverse f).toPath ≫ q.reverse)
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ (s : Set (Subgroupoid C)), IsGLB s (sInf s)

Tactic:
refine fun s => ⟨fun S Ss F => ?_, fun T Tl F fT => ?_⟩ <;> simp only [mem_sInf]
      exacts [fun hp => hp S Ss, fun S Ss => Tl Ss fT]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: case mp
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
S : Subgroupoid C
Sn : S.IsNormal
⊢ generatedNormal X ≤ S → ∀ (c d : C), X c d ⊆ S.arrows c d

Tactic:
rintro h c d
    have h' := generated_le_generatedNormal X
    rw [le_iff] at h h'
    exact ((subset_generated X c d).trans (@h' c d)).trans (@h c d)

Goal state after:
Module: Mathlib.CategoryTheory.IsoCat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ f.inverse ⋙ e.inverse ⋙ e.functor ⋙ f.functor = 𝟭 E

Tactic:
← Functor.assoc e.inverse,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
e : IsoCat C D
f : IsoCat D E
⊢ f.inverse ⋙ (e.inverse ⋙ e.functor) ⋙ f.functor = 𝟭 E
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.disconnect ≤ S

Tactic:
rw [le_iff]; rintro _ _ _ ⟨⟩; assumption

Goal state after:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ E
G : D ⥤ E
α : Prod.fst C D ⋙ F ⟶ Prod.snd C D ⋙ G
x : C ⋆ D
⊢ homInduction (fun x x_1 f ↦ F.map f) (fun x x_1 g ↦ G.map g) (fun c d ↦ α.app (c, d)) (𝟙 x) =
    𝟙
      (match x with
      | left x => F.obj x
      | right x => G.obj x)

Tactic:
by
    cases x
    · dsimp only [id_left, homInduction_left]
      simp
    · dsimp only [id_right, homInduction_right]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f =
    ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i))).hom ≫
      prod.map (map fun i ↦ f ↑i) (map fun i ↦ f ↑i) ≫
        ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i ↦ Y ↑i) (∏ᶜ fun i ↦ Y ↑i))).inv

Tactic:
by
  rw [← Category.assoc, Iso.eq_comp_inv]
  dsimp only [IsLimit.conePointUniqueUpToIso, binaryFanOfProp, prodIsProd]
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ ≫ h₁₂.p₁ = h.p₁

Tactic:
by simp [p₁₂, hp₁]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
x✝² : C
x✝¹ x✝ : x✝² ⟶ h.pullback
h₁ : x✝¹ ≫ h.p₁₂ = x✝ ≫ h.p₁₂
h₂ : x✝¹ ≫ h.p₁₃ = x✝ ≫ h.p₁₃
⊢ x✝¹ ≫ h.p₁ = x✝ ≫ h.p₁

Tactic:
by simpa using h₁ =≫ h₁₂.p₁

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout b.inr 0 b.fst 0

Tactic:
refine of_top ?_ (by simp) (of_isBilimit h)
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
⊢ Function.RightInverse (fun f k ↦ f ≫ Pi.π (fun x ↦ Y) k) Pi.lift

Tactic:
intro f
        ext ⟨j⟩
        simp [yp]

Goal state after: