mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z✝) (injectiveResolution X✝)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
        (InjectiveResolution.desc f (injectiveResolution Y✝) (injectiveResolution X✝)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
        (InjectiveResolution.desc g (injectiveResolution Z✝) (injectiveResolution Y✝))

Tactic:
← (HomotopyCategory.quotient _ _).map_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z✝) (injectiveResolution X✝)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc f (injectiveResolution Y✝) (injectiveResolution X✝) ≫
        InjectiveResolution.desc g (injectiveResolution Z✝) (injectiveResolution Y✝))
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n✝ n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
Y' : C
R' : InjectiveResolution Y'
g : Y ⟶ Y'
φ : R.Hom R' g
⊢ (f ≫ φ.hom.f n) ≫ R'.cocomplex.d n m = 0

Tactic:
by simp [reassoc_of% hf]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ (pullback.snd (Abelian.factorThruImage S.f) c ≫ c) ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom

Tactic:
rw [Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.Exact
b' : Pseudoelement S.X₂
b : Over S.X₂
hb : pseudoApply S.g ⟦b⟧ = 0
hb' : b.hom ≫ S.g = 0
c : b.left ⟶ (KernelFork.ofι (image.ι S.f) ⋯).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι S.f) ⋯) = b.hom
⊢ pullback.snd (Abelian.factorThruImage S.f) c ≫ c ≫ kernel.ι (cokernel.π S.f) =
    pullback.snd (Abelian.factorThruImage S.f) c ≫ b.hom
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
a : Over S.X₁
ha' : ⟦a⟧ = a'
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
← ha'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f) ≫
      (F.mapHomotopyCategory (ComplexShape.up ℕ)).map J.iso.hom ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)

Tactic:
rw [← Functor.map_comp_assoc, iso_hom_naturality f I J φ comm, Functor.map_comp,
    assoc, assoc]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) ≫
        (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : (isomorphisms C).inverseImage G f
⊢ G.kernel.isoModSerre f

Tactic:
simp only [inverseImage_iff, isomorphisms.iff] at hf

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Abelian C
inst✝² : Abelian D
G : D ⥤ C
inst✝¹ : PreservesFiniteLimits G
inst✝ : PreservesFiniteColimits G
X Y : D
f : X ⟶ Y
hf : IsIso (G.map f)
⊢ G.kernel.isoModSerre f
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n✝ n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
⊢ R.complex.d m n ≫ f ≫ g = 0

Tactic:
by simp [reassoc_of% hf]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ Functor.whiskerRight (rightDerivedToHomotopyCategory (𝟙 F))
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (F.rightDerived n)

Tactic:
simp only [rightDerivedToHomotopyCategory_id, Functor.whiskerRight_id']

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ 𝟙 (F.rightDerivedToHomotopyCategory ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) = 𝟙 (F.rightDerived n)
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
⊢ Mono (L.map f)

Tactic:
rw [Preadditive.mono_iff_cancel_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
⊢ ∀ (P : D) (g : P ⟶ L.obj X), g ≫ L.map f = 0 → g = 0
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x✝ : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (F g).right = g
x : ActionCategory G X
⊢ (F 1).left x.back = 𝟙 ()

Tactic:
rw [F.map_one]

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x✝ : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (F g).right = g
x : ActionCategory G X
⊢ left 1 x.back = 𝟙 ()
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
σ τ x : G
⊢ ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧

Tactic:
rw [mul_inv_rev, mul_assoc]

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

Goal state before:
pp: case refine_2
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
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f

Tactic:
· rintro ⟨X', Y', f', _, ⟨e⟩⟩
    exact ((MorphismProperty.monomorphisms D).arrow_mk_iso_iff e).1
      (by simpa using inferInstanceAs (Mono (L.map f')))

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ T.map (T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f) ≫ s.pt.a =
    (beckAlgebraCofork X).pt.a ≫ T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f

Tactic:
dsimp
      rw [Functor.map_comp, Category.assoc, h₂, Monad.right_unit_assoc,
        show X.a ≫ _ ≫ _ = _ from T.η.naturality_assoc _ _, h₁, Monad.left_unit_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C), Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.leftToRight.app X)

Tactic:
simp_rw [mono_leftToRight_app_iff_mono_adj₂_unit_app, rightToLeft_eq_counits]
  dsimp
  simp only [NatIso.isIso_inv_app, Functor.comp_obj, Functor.id_obj,
    whiskerLeft_app, Category.comp_id, Category.id_comp]
  simp_rw [epi_comp_iff_of_epi, epi_iff_forall_injective, mono_iff_forall_injective]
  rw [forall_comm]
  refine forall_congr' fun X ↦ forall_congr' fun Y ↦ ?_
  rw [← (q.adj₁.homEquiv _ _).comp_injective _]
  simp_rw [Function.comp_def, q.adj₁.homEquiv_naturality_left]
  refine ((q.adj₁.homEquiv _ _).injective_comp fun f ↦ _).trans ?_
  rw [← ((q.adj₂.homEquiv _ _).trans (q.adj₃.homEquiv _ _)).comp_injective _]
  simp [Function.comp_def, ← q.adj₂.homEquiv_symm_id, ← q.adj₂.homEquiv_naturality_right_symm,
    ← q.adj₃.homEquiv_id, ← q.adj₃.homEquiv_naturality_left]

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
η : LaxTrans F G
θ : LaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ η.vCompNaturality θ (f ≫ g) ≫ F.mapComp f g ▷ η.vCompApp θ c =
    η.vCompApp θ a ◁ H.mapComp f g ≫
      (α_ (η.vCompApp θ a) (H.map f) (H.map g)).inv ≫
        η.vCompNaturality θ f ▷ H.map g ≫
          (α_ (F.map f) (η.vCompApp θ b) (H.map g)).hom ≫
            F.map f ◁ η.vCompNaturality θ g ≫ (α_ (F.map f) (F.map g) (η.vCompApp θ c)).inv

Tactic:
by
  calc
    _ = 𝟙 _ ⊗≫ η.app a ◁ θ.naturality (f ≫ g) ⊗≫
          (η.naturality (f ≫ g) ≫ F.mapComp f g ▷ η.app c) ▷ θ.app c ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.naturality (f ≫ g) ≫ G.mapComp f g ▷ θ.app c) ⊗≫
          (η.naturality f ▷ G.map g ⊗≫ F.map f ◁ η.naturality g) ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [η.naturality_comp]
      bicategory
    _ = 𝟙 _ ⊗≫ η.app a ◁ (θ.app a ◁ H.mapComp f g ⊗≫ θ.naturality f ▷ H.map g) ⊗≫
          ((η.app a ≫ G.map f) ◁ θ.naturality g ≫ η.naturality f ▷ (G.map g ≫ θ.app c)) ⊗≫
            F.map f ◁ η.naturality g ▷ θ.app c ⊗≫ 𝟙 _ := by
      rw [θ.naturality_comp]
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} D₁
inst✝³ : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
hF : (W₁.prod W₂).IsInvertedBy F
inst✝¹ : W₁.ContainsIdentities
inst✝ : W₂.ContainsIdentities
⊢ W₁.Localization × W₂.Localization ⥤ E

Tactic:
by
  refine uncurry.obj (Construction.lift (prodLift₁ F hF).flip ?_).flip
  intro _ _ f₂ hf₂
  have : ∀ (X₁ : W₁.Localization),
      IsIso (((Functor.flip (prodLift₁ F hF)).map f₂).app X₁) := fun X₁ => by
    obtain ⟨X₁, rfl⟩ := (Construction.objEquiv W₁).surjective X₁
    exact ((MorphismProperty.isomorphisms E).arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso
        (eqToIso (Functor.congr_obj (prod_fac₁ F hF) X₁))).app (Arrow.mk f₂))).2
          (hF _ ⟨MorphismProperty.id_mem _ _, hf₂⟩)
  apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
i : X₂ ≅ Y₂
⊢ (X₁ ◁ i.hom) ▷ X₃ ≫ (α_ X₁ Y₂ X₃).hom ≫ X₁ ◁ i.inv ▷ X₃ = (α_ X₁ X₂ X₃).hom

Tactic:
simp only [associator_naturality₂_assoc, ← whiskerLeft_comp, ← whiskerRight_comp,
    Iso.hom_inv_id, whiskerRight_id, whiskerLeft_id, comp_id]

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

Goal state after:
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₁₂ : snd✝ = fst✝
⊢ ROfRel φ
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
ha : p.obj a = R
hb : p.obj b = S
h : f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom hb
⊢ p.IsHomLift f φ

Tactic:
subst ha hb h; simp

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

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.IsCartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst✝ : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : c ⟶ b'
hψ : p.IsHomLift f ψ
⊢ IsCartesian.map p f φ (ψ ≫ φ'.inv) ≫ φ ≫ φ'.hom = ψ

Tactic:
simp only [fac_assoc, assoc, Iso.inv_hom_id, comp_id]

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

Goal state before:
pp: case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a'✝ ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a'✝ ⟶ a
⊢ (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') π → π = τ ≫ ψ

Tactic:
⟨hπ, hπ_comp⟩

Goal state after:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝¹ : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst✝ : p.IsCartesian f φ
a'✝ : 𝒳
g : p.obj a'✝ ⟶ R
φ' : a'✝ ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a'✝ ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a'✝ ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π = τ ≫ ψ
Module: Mathlib.CategoryTheory.FiberedCategory.Fibered

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
⊢ (fun χ ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') π → π = τ' ≫ Φ.hom

Tactic:
⟨hπ, hπ_comp⟩

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π = τ' ≫ Φ.hom
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₂)
⊢ F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom = 𝟙 F'

Tactic:
apply F'.rightDerived_ext β W₂

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₂)
⊢ β ≫
      L₂.whiskerLeft
        (F'.leftUnitor.inv ≫ F'.whiskerLeft η ≫ (F'.associator G' F').inv ≫ whiskerRight ε F' ≫ F'.rightUnitor.hom) =
    β ≫ L₂.whiskerLeft (𝟙 F')
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 A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (F.map (pullback.fst f g))) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = a

Tactic:
simp only [fiberPullbackEquiv, Functor.comp_map, Iso.toEquiv_symm_fun]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (F.map (pullback.fst f g)))
      ((ConcreteCategory.hom
            (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g ≪≫
                Types.pullbackIsoPullback (F.map f).hom (F.map g).hom).inv).toFun
        ⟨(a, b), h⟩) =
    a
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 A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (F.map (pullback.snd f g))) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b

Tactic:
simp only [fiberPullbackEquiv, Functor.comp_map, Iso.toEquiv_symm_fun]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X A B : C
f : A ⟶ X
g : B ⟶ X
a : (F.obj A).obj
b : (F.obj B).obj
h : (ConcreteCategory.hom (F.map f)) a = (ConcreteCategory.hom (F.map g)) b
⊢ (ConcreteCategory.hom (F.map (pullback.snd f g)))
      ((ConcreteCategory.hom
            (PreservesPullback.iso (F ⋙ FintypeCat.incl) f g ≪≫
                Types.pullbackIsoPullback (F.map f).hom (F.map g).hom).inv).toFun
        ⟨(a, b), h⟩) =
    b
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsGalois A
a b : (F.obj A).obj
⊢ (ConcreteCategory.hom (F.map ((evaluationEquivOfIsGalois F A a).symm b).hom)) a = b

Tactic:
by
  change (evaluationEquivOfIsGalois F A a) _ = _
  simp

Goal state after: