mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse :=
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
⊢ IsCoverDense.restrictHomEquivHom
      ((adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)) Q)
          ((sheafifyOfIsEquivalence J K G A).map f ≫ g))) =
    IsCoverDense.restrictHomEquivHom
      (G.op.whiskerLeft f ≫
        (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
            ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
          ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g))

Tactic:
congr 2

Goal state after:
case e_6
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)) Q)
        ((sheafifyOfIsEquivalence J K G A).map f ≫ g)) =
    G.op.whiskerLeft f ≫
      (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
t : IsLimit c
s : Cone F
⊢ K.map (t.lift ((proj K B).mapCone s)) ≫ (raiseCone c).pt.hom = s.pt.hom

Tactic:
simp [← Functor.map_comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
c : WalkingMulticospan E.multicospanShape
⊢ (Hom.mapMulticospan f.hom).map ((eqToIso ⋯).hom.app c) ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj c) =
    𝟙 ((Hom.mapMulticospan f.hom).obj c)

Tactic:
cases c

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
a✝ : E.multicospanShape.L
⊢ (Hom.mapMulticospan f.hom).map ((eqToIso ⋯).hom.app (WalkingMulticospan.left a✝)) ≫
      (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝))

case right
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
a✝ : E.multicospanShape.R
⊢ (Hom.mapMulticospan f.hom).map ((eqToIso ⋯).hom.app (WalkingMulticospan.right a✝)) ≫
      (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝))
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F✝ : J × K ⥤ Type v
inst✝ : IsFiltered K
F : J ⥤ K ⥤ Type v
this : IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫ lim.map (whiskerRight (currying.unitIso.app F).inv colim))
⊢ IsIso (colimitLimitToLimitColimitCone F).hom

Tactic:
apply IsIso.comp_isIso

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
hS : S ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left
R : Sieve Y
Z : C
f : Z ⟶ Y.left
hR : Sieve.pullback (Over.homMk f ⋯) R ∈ ⇑(Sieve.overEquiv (Over.mk (f ≫ Y.hom))) ⁻¹' J (Over.mk (f ≫ Y.hom)).left
hf : ((Sieve.overEquiv Y) S).arrows f
⊢ Sieve.pullback f ((Sieve.overEquiv Y) R) ∈ J Z

Tactic:
rwa [Set.mem_preimage, Sieve.overEquiv_pullback] at hR

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
J✝ : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J✝ RingCat
R : Sheaf K RingCat
inst✝⁶ : F.IsContinuous J✝ K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J✝ K).obj R
inst✝⁵ : (pushforward φ).IsRightAdjoint
inst✝⁴ : HasWeakSheafify J✝ AddCommGrpCat
inst✝³ : HasWeakSheafify K AddCommGrpCat
inst✝² : J✝.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : K.WEqualsLocallyBijective AddCommGrpCat
inst✝ : F.Final
I J : Type u
f : I → J
i : I
⊢ (Cofan.mk ((pullback φ).obj (free I)) fun j ↦ (pullback φ).map (ιFree j)).inj i ≫
      (pullback φ).map (freeMap f) ≫ (pullbackObjFreeIso φ J).hom =
    (Cofan.mk ((pullback φ).obj (free I)) fun j ↦ (pullback φ).map (ιFree j)).inj i ≫
      (pullbackObjFreeIso φ I).hom ≫ freeMap f

Tactic:
simp [← Functor.map_comp_assoc]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
⊢ PreservesLimitsOfShape (Discrete ι) hf.functor

Tactic:
apply +allowSynthFailures preservesLimitsOfShape_of_discrete

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
ι : Type u_1
inst✝¹ : Nonempty ι
inst✝ : Finite ι
⊢ ∀ (f_1 : ι → Opens ↑X), PreservesLimit (Discrete.functor f_1) hf.functor
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj
i : ι
⊢ ((restrictHomEquivHom F F' h) α).app (op (B i)) = α.app (op i)

Tactic:
nth_rw 2 [← (restrictHomEquivHom F F' h).left_inv α]
  rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
| ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t

Tactic:
enter [t]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))),
    ∀ x ∈ U,
      ∃ V,
        ∃ (_ : x ∈ V),
          ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
| ∀ x ∈ U,
    ∃ V,
      ∃ (_ : x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ (ConcreteCategory.hom (M.map (𝟙 (IsFiltered.max ⋯.some V))))
      ((ConcreteCategory.hom (R.map (leftToMax ⋯.some V))) 0 • (ConcreteCategory.hom (M.map (rightToMax ⋯.some V))) b) =
    (ConcreteCategory.hom (M.map (leftToMax ⋯.some V))) 0

Tactic:
simp only [map_zero, zero_smul]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this : ContinuousAdd M
⊢ instTopologicalSpaceProd = moduleTopology R (M × N)

Tactic:
have : ContinuousAdd N := toContinuousAdd R N

Goal state after:
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝ : ContinuousAdd M
this : ContinuousAdd N
⊢ instTopologicalSpaceProd = moduleTopology R (M × N)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hfc : ⇑f ∈ {f | Continuous[inst✝⁵, inst✝³] f}
⊢ ⇑f ∈ Set.range DFunLike.coe

Tactic:
exact ⟨⟨f, hfc⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_9
E : Type u_10
F : Type u_11
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Module R E
inst✝² : TopologicalSpace F
inst✝¹ : AddCommMonoid F
inst✝ : Module R F
f : E →L[R] F
g : F →L[R] E
hinv : g ∘SL f = ContinuousLinearMap.id R E
⊢ Function.LeftInverse ⇑g ⇑f

Tactic:
simpa [coe_comp, ← Function.leftInverse_iff_comp] using congr(⇑$hinv)

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Preserves

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
⊢ F.map f ≫
      F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι (F.obj X))) f) ≫
        adj.counit.app (Injective.under (F.obj X)) =
    Injective.ι (F.obj X)

Tactic:
simp [← Functor.map_comp_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Limits.PreservesLimitsOfSize.{v, v, v, max v v', max u (v + 1), (max v v') + 1}
    (uliftFunctor.{v', v, u} R ⋙ forget (ModuleCat R))

Tactic:
change Limits.PreservesLimitsOfSize.{v, v} (forget (ModuleCat R) ⋙
      CategoryTheory.uliftFunctor.{v'})
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ IsIso F

Tactic:
have hF' : Topology.IsEmbedding F := by
    refine .of_comp F.1.2 D₂.ι.1.2 ?_
    -- `isEmbedding_of_isOpenQuotientMap_of_isInducing` is the key lemma that shows the two
    -- definitions of homology give the same topology.
    refine isEmbedding_of_isOpenQuotientMap_of_isInducing
      D₁.i (F ≫ D₂.ι) D₁.π D₂.p ?_ .subtypeVal
      (Submodule.isOpenQuotientMap_mkQ _).isQuotientMap
      (Submodule.isOpenQuotientMap_mkQ _)
      (Subtype.val_injective.comp hF.1) ?_
    · rw [← ContinuousLinearMap.coe_comp, ← ContinuousLinearMap.coe_comp,
        ← hom_comp, ← hom_comp, ShortComplex.π_leftRightHomologyComparison'_ι]
    · suffices ∀ x y, S.g y = 0 → D₂.p y = D₂.p x → S.g x = 0 by
        simpa [Set.subset_def, D₁, kerι_apply S.g] using this
      intro x y hy e
      obtain ⟨z, hz⟩ := (Submodule.Quotient.eq _).mp e
      obtain rfl := eq_sub_iff_add_eq.mp hz
      simpa [show S.g (S.f z) = 0 from ConcreteCategory.congr_hom S.zero z] using hy

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ IsIso F
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ Topology.IsEmbedding ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F)) ∧
    Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F))

Tactic:
exact ⟨hF', hF.2⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0

Tactic:
· rintro ⟨hM, hM₂⟩
    let e : M ≃L[R] M₂ :=
    { toFun := 0
      invFun := 0
      left_inv x := Subsingleton.elim _ _
      right_inv x := Subsingleton.elim _ _
      map_add' x y := Subsingleton.elim _ _
      map_smul' c x := Subsingleton.elim _ _ }
    refine ⟨e, ?_⟩
    ext x
    exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.Algebra.Category.Ring.EqualizerPushout

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
⊢ IsLimit (Fork.ofι f ⋯)

Tactic:
let fork : Fork (pushoutCocone R S S).inl (pushoutCocone R S S).inr :=
    Fork.ofι (ofHom (algebraMap R S)) (by rw [(PushoutCocone.condition _)])

Goal state after:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
fork : Fork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr := Fork.ofι (ofHom (algebraMap ↑R ↑S)) ⋯
⊢ IsLimit (Fork.ofι f ⋯)
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : IsCardinalPresentable X κ
⊢ IsCardinalPresentable X κ'

Tactic:
exact isCardinalPresentable_of_le _ h

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
J₂ : Type u'
inst✝⁵ : Category.{v, u} J₁
inst✝⁴ : Category.{v', u'} J₂
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J₁ κ
inst✝¹ : IsCardinalFiltered J₂ κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ J₁ × J₂
hC : HasCardinalLT (Arrow A✝) κ
⊢ Cocone F

Tactic:
by
    let c₁ := cocone (F ⋙ Prod.fst _ _) hC
    let c₂ := cocone (F ⋙ Prod.snd _ _) hC
    exact
      { pt := (c₁.pt, c₂.pt)
        ι.app i := (c₁.ι.app i, c₂.ι.app i)
        ι.naturality {i j} f := by
          ext
          · simpa using c₁.w f
          · simpa using c₂.w f }

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type u_6
C : Type u_7
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra R B
inst✝ : Algebra R C
a : A
b : B
c : C
⊢ (prodRight R S A B C).symm (a ⊗ₜ[R] b, a ⊗ₜ[R] c) = a ⊗ₜ[R] (b, c)

Tactic:
apply (prodRight R S A B C).injective
  simp [prodRight_tmul]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
r : ↥s
this :
  (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) ((ConcreteCategory.hom g') ↑r) =
      (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) 0 ↔
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map f)) ((ConcreteCategory.hom g') ↑r) =
        (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map g)) 0
⊢ (ConcreteCategory.hom (g' ≫ c.ι.app i)) ↑r = 0

Tactic:
rw [← hg']

Goal state after:
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
r : ↥s
this :
  (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) ((ConcreteCategory.hom g') ↑r) =
      (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app i)) 0 ↔
    ∃ k f g,
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map f)) ((ConcreteCategory.hom g') ↑r) =
        (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map g)) 0
⊢ (ConcreteCategory.hom (π ≫ g)) ↑r = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ p > 0, MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P

Tactic:
constructor
  · intro h q q_prime q_mixedChar
    exact h q (Nat.Prime.pos q_prime) q_mixedChar
  · intro h q q_pos q_mixedChar
    rcases q_mixedChar.charP_quotient with ⟨I, hI_ne_top, _⟩
    -- Krull's Thm: There exists a prime ideal `P` such that `I ≤ P`
    rcases Ideal.exists_le_maximal I hI_ne_top with ⟨M, hM_max, h_IM⟩
    let r := ringChar (R ⧸ M)
    have r_pos : r ≠ 0 := by
      have q_zero :=
        congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)
      simp only [map_natCast, map_zero] at q_zero
      apply ne_zero_of_dvd_ne_zero (ne_of_gt q_pos)
      exact (CharP.cast_eq_zero_iff (R ⧸ M) r q).mp q_zero
    have r_prime : Nat.Prime r :=
      or_iff_not_imp_right.1 (CharP.char_is_prime_or_zero (R ⧸ M) r) r_pos
    apply h r r_prime
    have : CharZero R := q_mixedChar.toCharZero
    exact ⟨⟨M, hM_max.ne_top, ringChar.of_eq rfl⟩⟩

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a : α
s : Seq α
⊢ (cons a s).head = some a

Tactic:
head_eq_destruct,

Goal state after:
α : Type u
a : α
s : Seq α
⊢ Prod.fst <$> (cons a s).destruct = some a