mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ ∀ b ∈ (Opposite.unop S).attach, b ≠ v → Pi.π f (↑b).as ≫ Pi.ι (fun a ↦ f (↑a).as) b ≫ Pi.π (fun x ↦ f (↑x).as) v = 0

pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ v ∉ (Opposite.unop S).attach → Pi.π f (↑v).as ≫ Pi.ι (fun a ↦ f (↑a).as) v ≫ Pi.π (fun x ↦ f (↑x).as) v = 0

Tactic:
· intro b hb hb₁
    rw [Pi.ι_π_of_ne _ hb₁, comp_zero]

Goal state after:
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ v ∉ (Opposite.unop S).attach → Pi.π f (↑v).as ≫ Pi.ι (fun a ↦ f (↑a).as) v ≫ Pi.π (fun x ↦ f (↑x).as) v = 0
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:
rw [← (HomotopyCategory.quotient _ _).map_comp]
    apply HomotopyCategory.eq_of_homotopy
    apply InjectiveResolution.descCompHomotopy

Goal state after:
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 : ℕ
f g : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
hg : g ≫ R.cocomplex.d n m = 0
⊢ R.extMk f m hm hf - R.extMk g m hm hg = R.extMk (f - g) m hm ⋯

Tactic:
by
  dsimp [extMk]
  simp only [Preadditive.sub_comp]
  rw [Cocycle.fromSingleMk_sub _ _ _ _ _
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hf])
    (by simp [cochainComplex_d _ _ _ n m rfl rfl, reassoc_of% hg])]
  simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = 0
⊢ a = 0

Tactic:
rw [← apply_zero f] at ha

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = pseudoApply f 0
⊢ a = 0
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 : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
p : ℕ
hp : p + 1 = n
⊢ R.extMk f m hm hf = 0 ↔ ∃ g, R.complex.d n p ≫ g = f

Tactic:
simp only [← R.extEquivCohomologyClass.apply_eq_iff_eq,
    extEquivCohomologyClass_extMk, extEquivCohomologyClass_zero,
    CohomologyClass.mk_eq_zero_iff]
  rw [Cocycle.toSingleMk_mem_coboundaries_iff _ _ _ _ _ (-p) (by lia),
    R.cochainComplex_d _ _ _ _ rfl rfl]
  refine ⟨fun ⟨g, hg⟩ ↦ ⟨(R.cochainComplexXIso (-p) p rfl).inv ≫ g, ?_⟩,
    fun ⟨g, hg⟩ ↦ ⟨(R.cochainComplexXIso (-p) p rfl).hom ≫ g, by simpa⟩⟩
  rw [← cancel_epi (R.cochainComplexXIso (-n) n rfl).hom]
  simpa [Category.assoc] using hg

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✝
⊢ (MorphismProperty.epimorphisms D).inverseImage L f✝ ↔ P.epiModSerre f✝

Tactic:
simp [epi_map_iff L P]

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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝ : Abelian D := abelian L P
this : PreservesFiniteColimits L
x✝ : PreservesFiniteColimits (L ⋙ G)
⊢ (L ⋙ G).Additive

Tactic:
have := preservesBinaryBiproducts_of_preservesBinaryCoproducts (L ⋙ G)

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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝¹ : Abelian D := abelian L P
this✝ : PreservesFiniteColimits L
x✝ : PreservesFiniteColimits (L ⋙ G)
this : PreservesBinaryBiproducts (L ⋙ G)
⊢ (L ⋙ G).Additive
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G✝ : D ⥤ E
G : D ⥤ₑ E
⊢ exactFunctor C E (((exactFunctor D E).ι ⋙ (Functor.whiskeringLeft C D E).obj L).obj G)

Tactic:
by
      dsimp
      simpa only [exactFunctor_comp_iff L P] using G.property

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

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
h : F.FullyFaithful
this✝ : F.Full
this : F.Faithful
⊢ IsIso t.adj₂.counit

Tactic:
by
      rw [← t.isIso_unit_iff_isIso_counit]
      infer_instance

Goal state after:
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)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (constructRightAdjointEquiv L U' adj₁ adj₂ h✝ X Y').symm (L.map g ≫ h) =
    g ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h✝ Y Y').symm h

Tactic:
constructRightAdjointEquiv_symm_apply,

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)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (Fork.IsLimit.homIso (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y')))
          X).symm
      ⟨(adj₂.homEquiv X (F.obj Y'))
          ((adj₁.homEquiv (L.obj X) (F.obj Y')).symm
            ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj X)) (L.map g ≫ h))),
        ⋯⟩ =
    g ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h✝ Y Y').symm h
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)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (Fork.IsLimit.homIso (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y')))
          X).symm
      ⟨(adj₂.homEquiv X (F.obj Y'))
          ((adj₁.homEquiv (L.obj X) (F.obj Y')).symm
            ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj X)) (L.map g ≫ h))),
        ⋯⟩ =
    g ≫ (constructRightAdjointEquiv L U' adj₁ adj₂ h✝ Y Y').symm h

Tactic:
constructRightAdjointEquiv_symm_apply,

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)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (Fork.IsLimit.homIso (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y')))
          X).symm
      ⟨(adj₂.homEquiv X (F.obj Y'))
          ((adj₁.homEquiv (L.obj X) (F.obj Y')).symm
            ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj X)) (L.map g ≫ h))),
        ⋯⟩ =
    g ≫
      (Fork.IsLimit.homIso
            (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y).symm
        ⟨(adj₂.homEquiv Y (F.obj Y'))
            ((adj₁.homEquiv (L.obj Y) (F.obj Y')).symm ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h)),
          ⋯⟩
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)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (adj₂.homEquiv X (F.obj Y'))
      (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj X)) (L.map g ≫ h)) ≫ adj₁.counit.app (F.obj Y')) =
    ↑((Fork.IsLimit.homIso
          (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) X)
        (g ≫
          (Fork.IsLimit.homIso
                (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y).symm
            ⟨(adj₂.homEquiv Y (F.obj Y'))
                (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h) ≫ adj₁.counit.app (F.obj Y')),
              ⋯⟩))

Tactic:
erw [Fork.IsLimit.homIso_natural, Fork.IsLimit.homIso_natural]

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)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ (adj₂.homEquiv X (F.obj Y'))
      (F.map (L.map g ≫ ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h)) ≫ adj₁.counit.app (F.obj Y')) =
    g ≫
      ↑((Fork.IsLimit.homIso
            (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y)
          ((Fork.IsLimit.homIso
                (limit.isLimit (parallelPair (U'.map (F.map (adj₁.unit.app Y'))) (otherMap L U' adj₁ adj₂ Y'))) Y).symm
            ⟨(adj₂.homEquiv Y (F.obj Y'))
                (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h) ≫ adj₁.counit.app (F.obj Y')),
              ⋯⟩))
Module: Mathlib.CategoryTheory.Core

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { iso := (EquivFunctor.mapEquiv m (f ≫ g).iso.toEquiv).toIso } =
    { iso := (EquivFunctor.mapEquiv m f.iso.toEquiv).toIso } ≫ { iso := (EquivFunctor.mapEquiv m g.iso.toEquiv).toIso }

Tactic:
ext
    simp [Equiv.toIso, EquivFunctor.map_trans']

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
⊢ (f a).Dom

Tactic:
let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
  rw [WellFounded.fixF_eq] at h₂; exact h₂.fst.fst

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : 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 : b ∈ f.fix 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₀
⊢ C a

Tactic:
refine fixInduction h fun a' h ih => ?_

Goal state after:
α : 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✝ : b ∈ f.fix 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₀
a' : α
h : b ∈ f.fix a'
ih : (a'' : α) → Sum.inr a'' ∈ f a' → C a''
⊢ C a'
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t

Tactic:
by_cases h : x ∈ s <;> simp [h]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s

Tactic:
by
  ext x
  simp only [Set.mem_preimage, PFun.asSubtype, PFun.mem_preimage]
  show f.fn x.val _ ∈ s ↔ ∃ y ∈ s, y ∈ f x.val
  exact
    Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
      have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
      Part.mem_unique fxy this ▸ ys

Goal state after:
Module: Mathlib.CategoryTheory.Endofunctor.Algebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
V V₀ V₁ V₂ : Coalgebra F
f : V₀ ⟶ V₁
g : V₁ ⟶ V₂
h : V₀.V ≅ V₁.V
w : V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str
⊢ V₁.str ≫ F.map h.inv = h.inv ≫ V₀.str

Tactic:
by
        rw [h.eq_inv_comp, ← Category.assoc, ← w, Category.assoc, ← F.map_comp]
        simp only [Iso.hom_inv_id, Functor.map_id, Category.comp_id]

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
hφ' : p.IsHomLift f (eqToHom ⋯ ≫ φ)
⊢ p.IsHomLift f φ

Tactic:
simpa using hφ'

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
hφ' : p.IsHomLift f (φ ≫ eqToHom ⋯)
⊢ p.IsHomLift f φ

Tactic:
simpa using hφ'

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 : 𝒳
φ : a ⟶ b
f : R' ⟶ S
hφ' : p.IsHomLift (eqToHom ⋯ ≫ f) φ
⊢ p.IsHomLift f φ

Tactic:
simpa using hφ'

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
hφ' : p.IsHomLift (f ≫ eqToHom ⋯) φ
⊢ p.IsHomLift f φ

Tactic:
simpa using hφ'

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
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
⊢ IsIso (F.map f)

Tactic:
apply (ConcreteCategory.isIso_iff_bijective (F.map f)).mpr

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj
⊢ Function.Bijective ⇑(ConcreteCategory.hom (F.map f))
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: 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
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
⊢ Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj

Tactic:
card_fiber_eq_of_iso F i

Goal state after:
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
nhi : ∀ (a : IsInitial X), False
Y : C
v : Y ⟶ X
hni : ∀ (a : IsInitial Y), False
hvmono : Mono v
hvnoiso : ¬IsIso v
Z : C
u : Z ⟶ X
c : IsColimit (BinaryCofan.mk v u)
t : ColimitCocone (pair Y Z) := { cocone := BinaryCofan.mk v u, isColimit := c }
hn1 : Nat.card (F.obj Y).obj < n
i : X ≅ Y ⨿ Z
⊢ Nat.card (F.obj (Y ⨿ Z)).obj = Nat.card (F.obj Y).obj + Nat.card (F.obj Z).obj
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).obj
left✝ : IsGalois A
⊢ (ConcreteCategory.hom (t.app X)) ((ConcreteCategory.hom (F.map f)) a) =
    (ConcreteCategory.hom (s.app X)) ((ConcreteCategory.hom (F.map f)) a)

Tactic:
NatTrans.naturality_apply,

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).obj
left✝ : IsGalois A
⊢ (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (t.app A)) a) =
    (ConcreteCategory.hom (s.app X)) ((ConcreteCategory.hom (F.map f)) a)
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).obj
left✝ : IsGalois A
⊢ (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (t.app A)) a) =
    (ConcreteCategory.hom (s.app X)) ((ConcreteCategory.hom (F.map f)) a)

Tactic:
NatTrans.naturality_apply,

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
G : C ⥤ FintypeCat
t s : F ⟶ G
h : ∀ (X : C) [IsGalois X], t.app X = s.app X
X A : C
f : A ⟶ X
a : (F.obj A).obj
left✝ : IsGalois A
⊢ (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (t.app A)) a) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (s.app A)) a)
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 U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
X : ↑I
f : A ⟶ P
⊢ (ConcreteCategory.hom (t.hom.app ↑X))
      ((ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)) =
    (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)

Tactic:
NatTrans.naturality_apply,

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
X : ↑I
f : A ⟶ P
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X)))
      ((ConcreteCategory.hom (t.hom.app (∏ᶜ fun X ↦ ↑X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)) =
    (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)
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 U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
X : ↑I
f : A ⟶ P
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X)))
      ((ConcreteCategory.hom (t.hom.app (∏ᶜ fun X ↦ ↑X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)) =
    (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)

Tactic:
NatTrans.naturality_apply,

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
X : ↑I
f : A ⟶ P
⊢ (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X)))
      ((ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (t.hom.app A)) a)) =
    (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)
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)
⊢ EqvGen (HomRel.CompClosure redStep) (q ≫ q.reverse) (𝟙 X)

Tactic:
exact ih

Goal state after: