mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
this : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f
⊢ L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ 0 = 0

Tactic:
comp_zero,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝ : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
this : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f
⊢ L.map φ.s ≫ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ L.map f ≫ L.map (cokernel.π f) = L.map f ≫ 0

Tactic:
comp_zero,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ L.map f ≫ L.map (cokernel.π f) = 0
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
a b : N ⋊[φ] G
⊢ fn (a * b).left * fg (a * b).right = fn a.left * fg a.right * (fn b.left * fg b.right)

Tactic:
have := fun n g ↦ DFunLike.ext_iff.1 (h n) g
    simp only [MulAut.conj_apply, MonoidHom.comp_apply, MulEquiv.coe_toMonoidHom] at this
    simp only [mul_left, mul_right, map_mul, this, mul_assoc, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.f
⊢ L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ 0 = 0

Tactic:
comp_zero,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesMonomorphisms
this✝ : L.EssSurj
W : D
w : W ⟶ L.obj X
hw : w ≫ L.map f = 0
this :
  ∀ (W : D) (w : W ⟶ L.obj X),
    w ≫ L.map f = 0 → (∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z) → ∃ l, l ≫ L.map (kernel.ι f) = w
hw' : ¬∃ Z, ∃ (hZ : W = L.obj Z), ∃ z, w = eqToHom hZ ≫ L.map z
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ w = L.map φ.f
⊢ L.map φ.s ≫ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
⊢ L.map f ≫ L.map φ.f = 0

Tactic:
by rw [← hφ, reassoc_of% hw, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Nonempty (NormalEpi f)

Tactic:
rw [epi_iff L P] at hf
    obtain ⟨X', Y', f', _, ⟨e⟩⟩ := hf
    let hf' := normalEpiOfEpi f'
    have := preservesCokernel L P hf'.g
    refine ⟨NormalEpi.ofArrowIso ?_ e⟩
    exact {
      W := L.obj hf'.W
      g := L.map hf'.g
      w := by rw [← L.map_comp]; simp [hf'.w]
      isColimit :=
        (CokernelCofork.isColimitMapCoconeEquiv _ L).1
          (isColimitOfPreserves L hf'.isColimit) }

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ Z✝ : Action V G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, comm := ⋯ }.hom =
    ({ hom := F.map f.hom, comm := ⋯ } ≫ { hom := F.map g.hom, comm := ⋯ }).hom

Tactic:
simp only [Action.comp_hom, F.map_comp]

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
W : Type u_2
inst✝² : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝¹ : Monoid G
inst✝ : F.Faithful
X✝ Y✝ : Action V G
a₁✝ a₂✝ : X✝ ⟶ Y✝
eq : (F.mapAction G).map a₁✝ = (F.mapAction G).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext
    apply_fun (fun f ↦ f.hom) at eq
    exact F.map_injective eq

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

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
h : F.FullyFaithful
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : (F.mapAction G).obj X✝ ⟶ (F.mapAction G).obj Y✝
⊢ X✝ ⟶ Y✝

Tactic:
refine ⟨h.preimage f.hom, fun _ ↦ h.map_injective ?_⟩
    simp only [map_comp, map_preimage]
    exact f.comm _

Goal state after:
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
this : Continuous v
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
let u : H × (forget₂ _ TopCat).obj X → (forget₂ _ TopCat).obj X :=
      fun p ↦ (forget₂ _ TopCat).map (X.obj.ρ p.1) p.2

Goal state after:
V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
X : ContAction V H
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
this : Continuous v
u : H × ↑((forget₂ (ContAction V H) TopCat).obj X) → ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (ConcreteCategory.hom ((forget₂ V TopCat).map (X.obj.ρ p.1))) p.2
⊢ Continuous fun p ↦ p.1 • p.2
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
⊢ { f // f ≫ U'.map (F.map (adj₁.unit.app X)) = f ≫ otherMap L U' adj₁ adj₂ X } ≃
    { g // F.map (adj₁.unit.app (L.obj Y) ≫ U.map g) = g ≫ F.map (adj₁.unit.app X) }

Tactic:
apply (adj₂.homEquiv _ _).symm.subtypeEquiv _

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
⊢ ∀ (a : Y ⟶ U'.obj (F.obj X)),
    a ≫ U'.map (F.map (adj₁.unit.app X)) = a ≫ otherMap L U' adj₁ adj₂ X ↔
      F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm a)) =
        (adj₂.homEquiv Y (F.obj X)).symm a ≫ F.map (adj₁.unit.app X)
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ (𝟭 (a ⟶ b)).map η ≫ ((λ_ g).symm ≪≫ normalizeIso nil g).hom =
    ((λ_ f).symm ≪≫ normalizeIso nil f).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map η

Tactic:
erw [leftUnitor_inv_naturality_assoc, assoc]

Goal state after:
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η : f ⟶ g
⊢ (λ_ ((𝟭 (a ⟶ b)).obj f)).inv ≫ 𝟙 a ◁ (𝟭 (a ⟶ b)).map η ≫ (normalizeIso nil g).hom =
    (λ_ f).symm.hom ≫ (normalizeIso nil f).hom ≫ ((normalize B).mapFunctor a b ⋙ inclusionPath a b).map η
Module: Mathlib.CategoryTheory.Bicategory.Modification.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : B ⥤ᴸ C
η θ : F ⟶ G
app : (a : B) → η.app a ≅ θ.app a
naturality : ∀ {a b : B} (f : a ⟶ b), F.map f ◁ (app b).hom ≫ θ.naturality f = η.naturality f ≫ (app a).hom ▷ G.map f
a b : B
f : a ⟶ b
⊢ F.map f ◁ (app b).inv ≫ η.naturality f = θ.naturality f ≫ (app a).inv ▷ G.map f

Tactic:
by
    simpa using F.map f ◁ (app b).inv ≫= (naturality f).symm =≫ (app a).inv ▷ G.map f

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ ((α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
        η.naturality (f ≫ g) ▷ θ.app c ≫
          (α_ (η.app a) (G.map (f ≫ g)) (θ.app c)).hom ≫
            η.app a ◁ θ.naturality (f ≫ g) ≫ (α_ (η.app a) (θ.app a) (H.map (f ≫ g))).inv) ≫
      (η.app a ≫ θ.app a) ◁ H.mapComp f g =
    (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      F.mapComp f g ▷ η.app c ▷ θ.app c ≫
        (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
          (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                  (F.map f ≫ η.app b) ◁ θ.naturality g ≫
                    η.naturality f ▷ (θ.app b ≫ H.map g) ≫
                      (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                        η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                          η.app a ◁ θ.naturality f ▷ H.map g ≫
                            η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                              (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv

Tactic:
by
        rw [whisker_exchange_assoc]; simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
⊢ ∀ (τ : (LeftExtension.mk u adj.unit).whisker h ⟶ s),
    τ = homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯

Tactic:
τ₀

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
⊢ τ₀ = homMk (𝟙 (u ≫ h) ⊗≫ u ◁ s.unit ⊗≫ adj.counit ▷ s.extension ⊗≫ 𝟙 s.extension) ⋯
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ ∀ (τ : (LeftLift.mk f adj.unit).whisker h ⟶ s),
    τ = homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯

Tactic:
τ₀

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
τ₀ : (LeftLift.mk f adj.unit).whisker h ⟶ s
⊢ τ₀ = homMk (𝟙 (h ≫ f) ⊗≫ s.unit ▷ f ⊗≫ s.lift ◁ adj.counit ⊗≫ 𝟙 s.lift) ⋯
Module: Mathlib.Data.PFun

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a✝ : α
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf✝ : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a
a : α
ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun x y ↦ Sum.inr x ∈ f y) y
IH :
  (y : α) →
    (a : Sum.inr y ∈ f a) →
      b ∈
          WellFounded.fixF
            (fun a IH ↦
              Part.assert (f a).Dom fun hf ↦
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            y ⋯ →
        C y
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯
⊢ C a

Tactic:
have h : b ∈ f.fix a := Part.mem_assert_iff.2 ⟨⟨a, ha⟩, h₂⟩

Goal state after:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ι : Type u_6
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a✝ : α
H : (a' : α) → b ∈ f.fix a' → ((a'' : α) → Sum.inr a'' ∈ f a' → C a'') → C a'
pf✝ : ∀ (a : α) (hf : (f a).Dom) (a' : α), (f a).get hf = Sum.inr a' → Sum.inr a' ∈ f a
a : α
ha : ∀ (y : α), Sum.inr y ∈ f a → Acc (fun x y ↦ Sum.inr x ∈ f y) y
IH :
  (y : α) →
    (a : Sum.inr y ∈ f a) →
      b ∈
          WellFounded.fixF
            (fun a IH ↦
              Part.assert (f a).Dom fun hf ↦
                match e : (f a).get hf with
                | Sum.inl b => Part.some b
                | Sum.inr a' => IH a' ⋯)
            y ⋯ →
        C y
h₂ :
  b ∈
    WellFounded.fixF
      (fun a IH ↦
        Part.assert (f a).Dom fun hf ↦
          match e : (f a).get hf with
          | Sum.inl b => Part.some b
          | Sum.inr a' => IH a' ⋯)
      a ⋯
h : b ∈ f.fix a
⊢ C a
Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ (fun f ↦ { hom := { toFun := fun o ↦ Option.elim o Y.toTwoPointing.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ } })
      ((fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ }) f) =
    f

Tactic:
by
            ext (_ | _) : 4
            · exact f.hom.map_snd.symm
            · rfl

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X✝ : Type w
φ✝ : X✝ → X✝ → Prop
X : Type w
φ : X → X → Prop
hφ : IsTrans X φ
x✝ : (Types.pullbackCone (p₂OfRel φ) (p₁OfRel φ)).pt
x₁ snd✝ : X
h : Function.uncurry φ (x₁, snd✝)
fst✝ x₂' : X
h' : Function.uncurry φ (fst✝, x₂')
h₁₂ :
  (ConcreteCategory.hom (p₂OfRel φ)) (⟨(x₁, snd✝), h⟩, ⟨(fst✝, x₂'), h'⟩).1 =
    (ConcreteCategory.hom (p₁OfRel φ)) (⟨(x₁, snd✝), h⟩, ⟨(fst✝, x₂'), h'⟩).2
⊢ ROfRel φ

Tactic:
dsimp at h₁₂
    rw [← h₁₂] at h'
    refine ⟨⟨x₁, x₂'⟩, hφ.trans _ _ _ h h'⟩

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X✝ : Type w
φ✝ : X✝ → X✝ → Prop
X : Type w
φ : X → X → Prop
hφ : IsTrans X φ
x✝ : (Types.pullbackCone (p₂OfRel φ) (p₁OfRel φ)).pt
x₁ snd✝ : X
h : Function.uncurry φ (x₁, snd✝)
fst✝ x₂' : X
h' : Function.uncurry φ (fst✝, x₂')
h₁₂ :
  (ConcreteCategory.hom (p₂OfRel φ)) (⟨(x₁, snd✝), h⟩, ⟨(fst✝, x₂'), h'⟩).1 =
    (ConcreteCategory.hom (p₁OfRel φ)) (⟨(x₁, snd✝), h⟩, ⟨(fst✝, x₂'), h'⟩).2
⊢ ROfRel φ

Tactic:
by
    dsimp at h₁₂
    rw [← h₁₂] at h'
    refine ⟨⟨x₁, x₂'⟩, hφ.trans _ _ _ h h'⟩

Goal state after:
Module: Mathlib.CategoryTheory.EquivalenceRelation

Goal state before:
pp: X R : Type w
p₁ p₂ : R ⟶ X
e : TransitiveRelation p₁ p₂
x₁ x₂ x₃ : X
⊢ Rel.ofPair p₁ p₂ x₁ x₂ → Rel.ofPair p₁ p₂ x₂ x₃ → Rel.ofPair p₁ p₂ x₁ x₃

Tactic:
refine fun ⟨r, ⟨hr₁, hr₂⟩⟩ ⟨r', ⟨hr₁', hr₂'⟩⟩ =>
      ⟨e.t ((PullbackCone.IsLimit.equivPullbackObj e.isLimit).symm ⟨(r, r'), hr₂.trans hr₁'.symm⟩),
        ⟨?_, ?_⟩⟩
    all_goals simpa

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

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.IsHomLift f φ.hom
⊢ f ≫ eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯ = 𝟙 R

Tactic:
by subst_hom_lift p f φ.hom; simp [← p.map_comp]

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

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.IsHomLift f φ.hom
⊢ (eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯) ≫ f = 𝟙 S

Tactic:
by subst_hom_lift p f φ.hom; simp [← p.map_comp]

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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = α.app X₁

Tactic:
reassoc_of% eq₂,

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₁ : G'.map (F'.map (α.app X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = ε.app (G'.obj (L₁.obj X₁)) ≫ α.app X₁
eq₃ : G'.map (L₁.map (adj.unit.app X₁)) ≫ α.app (F.obj (G.obj X₁)) = α.app X₁ ≫ L₂.map (G.map (adj.unit.app X₁))
eq₂ :
  G'.map (η.app (L₁.obj X₁)) ≫ G'.map (F'.map (α.app X₁)) =
    G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁))
⊢ G'.map (L₁.map (adj.unit.app X₁)) ≫ G'.map (β.app (G.obj X₁)) ≫ ε.app (L₂.obj (G.obj X₁)) = α.app X₁
Module: Mathlib.CategoryTheory.Galois.EssSurj

Goal state before:
pp: G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝ : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this : ∀ (i : ι), DiscreteTopology (f i).V.obj
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)

Tactic:
have (i : ι) : ContinuousSMul G (f i).V := ContinuousSMul.mk <| by
    let r : f i ⟶ X := Sigma.ι f i ≫ u.hom
    let r'' (p : G × (f i).V) : G × X.V := (p.1, r.hom p.2)
    let q (p : G × X.V) : X.V := (X.ρ p.1).hom p.2
    let q' (p : G × (f i).V) : (f i).V := ((f i).ρ p.1).hom p.2
    have heq : q ∘ r'' = r.hom ∘ q' := by
      ext (p : G × (f i).V)
      exact (ConcreteCategory.congr_hom (r.comm p.1) p.2).symm
    have hrinj : Function.Injective r.hom :=
      (ConcreteCategory.mono_iff_injective_of_preservesPullback r).mp <| mono_comp _ _
    let t₁ : TopologicalSpace (G × (f i).V) := inferInstance
    change @Continuous _ _ _ ⊥ q'
    have : TopologicalSpace.induced r.hom inferInstance = ⊥ := by
      rw [← le_bot_iff]
      exact fun s _ ↦ ⟨r.hom '' s, ⟨isOpen_discrete (r.hom '' s), Set.preimage_image_eq s hrinj⟩⟩
    rw [← this, continuous_induced_rng, ← heq]
    exact Continuous.comp continuous_smul (by fun_prop)

Goal state after:
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : CompactSpace G
X : Action FintypeCat G
inst✝² : TopologicalSpace X.V.obj
inst✝¹ : DiscreteTopology X.V.obj
inst✝ : ContinuousSMul G X.V.obj
ι : Type
hf : Finite ι
f : ι → Action FintypeCat G
u : ∐ f ≅ X
hc : ∀ (i : ι), IsConnected (f i)
this✝¹ : (i : ι) → TopologicalSpace (f i).V.obj := fun i ↦ ⊥
this✝ : ∀ (i : ι), DiscreteTopology (f i).V.obj
this : ∀ (i : ι), ContinuousSMul G (f i).V.obj
⊢ ∃ ι, ∃ (x : Finite ι), ∃ f, Nonempty ((∐ fun i ↦ Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ ↑(f i)))) ≅ X)
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u₁
inst✝ : Groupoid G
φ : C ⥤ G
x✝¹ x✝ : Quiver.FreeGroupoid C
f g : x✝¹ ⟶ x✝
r : homRel C f g
this :
  ∀ {X Y : C} (f : X ⟶ Y),
    Quiver.homOfEq ((Quiver.FreeGroupoid.of C ⋙q (Quiver.FreeGroupoid.lift φ.toPrefunctor).toPrefunctor).map f) ⋯ ⋯ =
      φ.toPrefunctor.map f
⊢ (Quiver.FreeGroupoid.lift φ.toPrefunctor).map f = (Quiver.FreeGroupoid.lift φ.toPrefunctor).map g

Tactic:
induction r <;> cat_disch

Goal state after: