mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced

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
F : C ⥤ D
inst✝³ : F.ReflectsIsomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : F.PreservesMonomorphisms
inst✝ : Balanced D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso f

Tactic:
← isIso_iff_of_reflects_iso (F := F)

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝³ : F.ReflectsIsomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : F.PreservesMonomorphisms
inst✝ : Balanced D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso (F.map f)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
⊢ Nonempty (IsColimit d)

Tactic:
by
  let iso : d ≅ (Cofan.mk _ fun i : ι ↦ PullbackCone.IsLimit.lift ht
      ((s i).fst ≫ a.inj i) ((s i).snd) (by simp [hu, (s i).condition])) :=
    Cofan.ext e <| fun p ↦ PullbackCone.IsLimit.hom_ext ht (by simp [he₁]) (by simp [he₂])
  rw [(IsColimit.equivIsoColimit iso).nonempty_congr]
  refine hau _ (Discrete.natTrans fun i ↦ (s i.as).fst) t.fst ?_ (.of_discrete _) fun j ↦ ?_
  · ext; simp [Cofan.inj]
  · simp only [Discrete.functor_obj_eq_as, Cofan.mk_pt, Functor.const_obj_obj, Cofan.mk_ι_app,
      Discrete.natTrans_app]
    rw [← Cofan.inj]
    refine IsPullback.of_right ?_ (by simp) (IsPullback.of_isLimit ht).flip
    simpa [hu] using (IsPullback.of_isLimit (hs j.1)).flip

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
⊢ HasProjectiveDimensionLT X m

Tactic:
by
  let := HasExt.standard C
  rw [hasProjectiveDimensionLT_iff]
  intro i hi Y e
  exact e.eq_zero_of_hasProjectiveDimensionLT n (by lia)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext S.X₁ Y i
⊢ hS.extClass.comp x₁ ⋯ = 0

Tactic:
rw [x₁.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
m : ↑(A.obj.obj X)
⊢ smul α φ 0 m = 0

Tactic:
apply A.isSeparated _ _ (Presheaf.imageSieve_mem J φ m)
  rintro Y f ⟨m₀, hm₀⟩
  rw [map_smul_eq α φ 0 m f.op 0 (by simp) m₀ hm₀, zero_smul, map_zero,
    (A.obj.map f.op).hom.map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f =
    StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g

Tactic:
ext
      exact congr($(IsCofiltered.eq_condition f' g').right)

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

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
J : GrothendieckTopology C
⊢ J ∈ {J | K ≤ J.toCoverage} → K.toGrothendieck ≤ J

Tactic:
hJ

Goal state after:
case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ J.toCoverage}
⊢ K.toGrothendieck ≤ J
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R) ↔
    ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀

Tactic:
refine ⟨fun h X E ↦ h _ E.mem₀, fun h X R hR ↦ ?_⟩

Goal state after:
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
R : Presieve X
hR : R ∈ J.coverings X
⊢ Presieve.IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
σ : ι → Type (max u_3 u_2)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.toPrecoverage.coverings (X i)
⊢ Sieve.generate (Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst) ∈ J S

Tactic:
← Presieve.bindOfArrows_ofArrows

Goal state after:
C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
σ : ι → Type (max u_3 u_2)
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.toPrecoverage.coverings (X i)
⊢ Sieve.generate (Presieve.bindOfArrows X f fun i ↦ Presieve.ofArrows (Y i) (g i)) ∈ J S
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ Sieve.pullback (𝟙 (pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂) =
    E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))

Tactic:
sieve₁_eq_pullback_sieve₁' _ _ _ pullback.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ Sieve.pullback (𝟙 (pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂) =
    Sieve.pullback (pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ⋯) (E.sieve₁' i₁ i₂)
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
G : C ⥤ D
A : Type w
inst✝² : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : G.IsCocontinuous J K
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
⊢ Presheaf.IsSheaf K (G.op.ran.obj ℱ.obj)

Tactic:
by
  rw [Presheaf.isSheaf_iff_multifork]
  intro X S
  exact ⟨RanIsSheafOfIsCocontinuous.isLimitMultifork ℱ.2
    (G.op.isPointwiseRightKanExtensionRanCounit ℱ.obj) S⟩

Goal state after:
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : Sheaf K (Type v)
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : D
⊢ appHom i.hom X ≫ appHom i.inv X = 𝟙 (ℱ.obj.obj (op X))

Tactic:
by
    ext x
    apply Functor.IsCoverDense.ext G
    intro Y f
    simp

Goal state after:
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : Sheaf K (Type v)
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : D
⊢ appHom i.inv X ≫ appHom i.hom X = 𝟙 (ℱ'.obj.obj (op X))

Tactic:
by
    ext x
    apply Functor.IsCoverDense.ext G
    intro Y f
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

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
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝³ : Category.{u, v} A
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve (G.obj U✝)
hS : S✝ ∈ K (G.obj U✝)
⊢ Sieve.functorPullback G S✝ ∈ (G.restrictedTopology K) U✝

Tactic:
by
    apply G.mem_restrictedTopology_of_functorPushforward_mem
    exact LocallyCoverDense.functorPushforward_functorPullback_mem ⟨_, hS⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : Cᵒᵖ ⥤ D
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.rightOp

Tactic:
by
    apply +allowSynthFailures createsColimitsOfShapeRightOp
    exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

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✝ : F.Final
M : SheafOfModules R
⊢ Function.Bijective (⇑((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) ∘ fun x ↦ pullbackObjUnitToUnit φ ≫ x)

Tactic:
← (unitHomEquiv _).bijective.of_comp_iff'

Goal state after:
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✝ : F.Final
M : SheafOfModules R
⊢ Function.Bijective
    (⇑((pushforward φ).obj M).unitHomEquiv ∘
      ⇑((pullbackPushforwardAdjunction φ).homEquiv (unit S) M) ∘ fun x ↦ pullbackObjUnitToUnit φ ≫ x)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬IsZero Y
⊢ IsZero Z

Tactic:
IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬biprod.inl = 0
⊢ IsZero Z
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.fst

Tactic:
intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.snd

Tactic:
intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y) (m : s.pt ⟶ X ⊓ Y), m ≫ homOfLE ⋯ = s.fst → m ≫ homOfLE ⋯ = s.snd → m = homOfLE ⋯

Tactic:
intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.inl

Tactic:
intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.inr

Tactic:
intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y) (m : X ⊔ Y ⟶ s.pt), homOfLE ⋯ ≫ m = s.inl → homOfLE ⋯ ≫ m = s.inr → m = homOfLE ⋯

Tactic:
intros; rfl

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ {R | ∀ x ∈ X, ∃ U f, R f ∧ x ∈ U}
x : T
hx : x ∈ Y
⊢ ∃ U f_1, Presieve.pullbackArrows f S f_1 ∧ x ∈ U

Tactic:
rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩

Goal state after:
T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
f : Y ⟶ X
S : Presieve X
hS : S ∈ {R | ∀ x ∈ X, ∃ U f, R f ∧ x ∈ U}
x : T
hx : x ∈ Y
U : Opens T
g : U ⟶ X
hg : S g
hU : x ∈ U
⊢ ∃ U f_1, Presieve.pullbackArrows f S f_1 ∧ x ∈ U
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
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
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ≅ G
⊢ (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) ≫
      (sheafPushforwardContinuousNatTrans α.inv RingCat J K).app S =
    φ

Tactic:
ext : 3; simp [← Functor.map_comp, ← op_comp]

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C X
𝒢 : Presheaf C Y
H₂ : (pushforward C H₁.hom).obj ℱ ⟶ 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ U = (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U)))

Tactic:
simp [Opens.map_def, Set.preimage_preimage]

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U))) = U

Tactic:
simp [Opens.map_def, Set.preimage_preimage]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
α : Type u
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
j : ι
⊢ U j ≤ s.pt

Tactic:
exact (s.ι.app (single j)).le

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
⊢ IsSeparable ↑(Submodule.span R s)

Tactic:
Submodule.span_eq_iUnion_nat

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
⊢ IsSeparable (⋃ n, (fun f ↦ ∑ i, (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s})
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_2
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)
⊢ ⇑(ConcreteCategory.hom D₂.p) ⁻¹' ⇑(ConcreteCategory.hom D₂.p) '' Set.range ⇑(ConcreteCategory.hom D₁.i) ⊆
    Set.range ⇑(ConcreteCategory.hom D₁.i)

Tactic:
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:
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝ : Module.Finite ↑R ↑S
this : Algebra.IsEpi ↑R ↑S
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
Algebra.isEpi_iff_surjective_algebraMap_of_finite

Goal state after:
R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝ : Module.Finite ↑R ↑S
this : Function.Surjective ⇑(algebraMap ↑R ↑S)
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: 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₂
x : M✝
y : M₂
M : M✝ ≃L[R] M₂
⊢ (↑M).inverse y = x ↔ y = ↑M x

Tactic:
simp only [inverse_equiv, ContinuousLinearEquiv.coe_coe]

Goal state after:
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₂
x : M✝
y : M₂
M : M✝ ≃L[R] M₂
⊢ M.symm y = x ↔ y = M x
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i : J
s' : Cone F :=
  { pt := Over.mk (s.π.app i ≫ (F.obj i).hom), π := { app := fun j ↦ Over.homMk (s.π.app j) ⋯, naturality := ⋯ } }
⊢ ∃! l, ∀ (j : J), l ≫ ((Over.forget X).mapCone c).π.app j = s.π.app j

Tactic:
refine ⟨(hc.lift s').left, fun j ↦ congr($(hc.fac s' j).left), fun f hf ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i : J
s' : Cone F :=
  { pt := Over.mk (s.π.app i ≫ (F.obj i).hom), π := { app := fun j ↦ Over.homMk (s.π.app j) ⋯, naturality := ⋯ } }
f : s.pt ⟶ ((Over.forget X).mapCone c).pt
hf : (fun l ↦ ∀ (j : J), l ≫ ((Over.forget X).mapCone c).π.app j = s.π.app j) f
⊢ f = Over.Hom.left (hc.lift s')
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ (ofCocone c).ι.app i ≫
      ofHom
        { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)),
          cont := ⋯ } =
    s.ι.app i

Tactic:
by ext x; exact congr($(hc.fac ((forget₂ _ _).mapCocone s) i).hom x)

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

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ ⊤ ≤ (ConcreteCategory.hom fBC).range

Tactic:
← closure_range_union_range_eq_top_of_isPushout (.of_hasPushout _ _),

Goal state after:
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ Subring.closure
      (Set.range ⇑(ConcreteCategory.hom (pushout.inl φ ψ)) ∪ Set.range ⇑(ConcreteCategory.hom (pushout.inr φ ψ))) ≤
    (ConcreteCategory.hom fBC).range