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

Goal state before:
pp: case pullback
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
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
Z : D
U : C
iUY : U ⟶ Y
iZU : Z ⟶ G.obj U
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
⊢ Sieve.pullback (iZU ≫ G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S)) ∈ K Z

Tactic:
Sieve.pullback_comp

Goal state after:
case pullback
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
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
Z : D
U : C
iUY : U ⟶ Y
iZU : Z ⟶ G.obj U
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
⊢ Sieve.pullback iZU (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈ K Z
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case pullback
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
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback (iZU₁ ≫ G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S))) ∈
    K Z

Tactic:
Sieve.pullback_comp

Goal state after:
case pullback
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
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback iZU₁
      (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback f S)))) ∈
    K Z
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
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ G.map (iU₁U ≫ iUY ≫ f) = G.map (iU₁W ≫ iWX)

Tactic:
by simp [e₁, e₂]

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

Goal state before:
pp: case transitive
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
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S R : Sieve X
a✝¹ : (Precoverage.comap G K.toPrecoverage).Saturate X S
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → (Precoverage.comap G K.toPrecoverage).Saturate Y (Sieve.pullback f R)
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.functorPushforward G (Sieve.pullback f R) ∈ K (G.obj Y)
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback (i ≫ G.map g) (Sieve.functorPushforward G R) ∈ K Y

Tactic:
Sieve.pullback_comp

Goal state after:
case transitive
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
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S R : Sieve X
a✝¹ : (Precoverage.comap G K.toPrecoverage).Saturate X S
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → (Precoverage.comap G K.toPrecoverage).Saturate Y (Sieve.pullback f R)
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.functorPushforward G (Sieve.pullback f R) ∈ K (G.obj Y)
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G R)) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Sieve.pullback (lift ≫ m) (equalizerSieve a b) ∈ K Y

Tactic:
Sieve.pullback_comp

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Sieve.pullback lift (Sieve.pullback m (equalizerSieve a b)) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
⊢ Sieve.pullback (lift ≫ m) (imageSieve f a) ∈ K Y

Tactic:
Sieve.pullback_comp

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
⊢ Sieve.pullback lift (Sieve.pullback m (imageSieve f a)) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case refine_2.refine_1
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
R : Presieve (F.obj X)
hR : R ∈ K.coverings (F.obj X)
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ Sieve.functorPullback F (Sieve.generate (Sieve.functorPushforward F T).arrows) ≤ T

Tactic:
rw [Sieve.generate_sieve, Sieve.functorPullback_functorPushforward_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hunique
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
y₁ y₂ : ↑F.sections
hy₁ : ∀ (i : I), ↑y₁ (Opposite.op (Y i)) = x i
hy₂ : ∀ (i : I), ↑y₂ (Opposite.op (Y i)) = x i
⊢ y₁ = y₂

Tactic:
exact hY.sections_ext ⟨F, hF⟩ (fun i => by rw [hy₁, hy₂])

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
⊢ u ≫ Over.homMk (𝟙 Z) ⋯ = 𝟙 ((Over.map f).obj (Over.mk (g ≫ U.hom)))

Tactic:
ext; simp [u]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
⊢ Over.homMk (𝟙 Z) ⋯ ≫ u = 𝟙 (Over.mk (g ≫ U.hom ≫ f))

Tactic:
ext; simp [u]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : S ∈ (J.over X) U
⊢ Sieve.functorPushforward (Over.post F) S ∈ (K.over (F.obj X)) ((Over.post F).obj U)

Tactic:
rw [GrothendieckTopology.mem_over_iff] at hS ⊢
    rw [Sieve.overEquiv_functorPushforward_post]
    exact h.cover_preserve hS

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

Goal state before:
pp: X : TopCat
U V : Opens ↑X
⊢ ↑(⋯.functor.obj ((map U.inclusion').obj V)) = ↑(V ⊓ U)

Tactic:
simp only [IsOpenMap.coe_functor_obj, map_coe, coe_inf,
    Set.image_preimage_eq_inter_range, set_range_inclusion' U]

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

Goal state before:
pp: α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
J : Type
⊢ ∀ [𝒥 : SmallCategory J] [FinCategory J], HasLimitsOfShape J α

Tactic:
𝒥₁

Goal state after:
α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
J : Type
𝒥₁ : SmallCategory J
⊢ ∀ [FinCategory J], HasLimitsOfShape J α
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
J : Type
⊢ ∀ [𝒥 : SmallCategory J] [FinCategory J], HasColimitsOfShape J α

Tactic:
𝒥₁

Goal state after:
α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
J : Type
𝒥₁ : SmallCategory J
⊢ ∀ [FinCategory J], HasColimitsOfShape J α
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
X✝ Y✝ : SheafOfModules R
e : X✝ ≅ Y✝
⊢ isQuasicoherent R X✝ → isQuasicoherent R Y✝

Tactic:
by
    intro ⟨⟨q⟩⟩
    exact ⟨⟨q.ofIsIso e.hom⟩⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) →
    ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj X_1 ⟶
      ((Pairwise.diagram ι).op ⋙ F.presheaf).obj X_1

pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ ∀ ⦃X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ⦄ (f : X_1 ⟶ Y),
    ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map f ≫ ?refine_1 Y =
      ?refine_1 X_1 ≫ ((Pairwise.diagram ι).op ⋙ F.presheaf).map f

Tactic:
· rintro ((_ | _) | (_ | _))
    exacts [s.fst, s.snd, s.fst ≫ F.1.map (homOfLE inf_le_left).op,
      s.snd ≫ F.1.map (homOfLE inf_le_left).op]

Goal state after:
case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ ∀ ⦃X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ⦄ (f : X_1 ⟶ Y),
    (((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).map f ≫
        Opposite.casesOn Y fun unop ↦
          Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
            ULift.casesOn a fun down ↦
              WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) =
      (Opposite.casesOn X_1 fun unop ↦
          Pairwise.casesOn unop (fun a ↦ ULift.casesOn a fun down ↦ WalkingPair.casesOn down s.fst s.snd) fun a a_1 ↦
            ULift.casesOn a fun down ↦
              WalkingPair.casesOn down (s.fst ≫ F.obj.map (homOfLE ⋯).op) (s.snd ≫ F.obj.map (homOfLE ⋯).op)) ≫
        ((Pairwise.diagram ι).op ⋙ F.presheaf).map f
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ m ≫ F.obj.map (eqToHom ⋯).op = F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op

Tactic:
apply (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.hom_ext

Goal state after:
case property.refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
⊢ ∀ (j : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ),
    (m ≫ F.obj.map (eqToHom ⋯).op) ≫ (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app j =
      (F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op) ≫
        (Functor.mapCone F.presheaf (Pairwise.cocone ι).op).π.app j
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
⊢ Mono (F.map f)

Tactic:
suffices ∃ h, F.map f ≫ h = Injective.ι (F.obj X) from mono_of_mono_fac this.choose_spec

Goal state after:
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
⊢ ∃ h, F.map f ≫ h = Injective.ι (F.obj X)
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
⊢ (colimitSetoid F) x y → descFunLift F s x = descFunLift F s y

Tactic:
r

Goal state after:
case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
r : (colimitSetoid F) x y
⊢ descFunLift F s x = descFunLift F s y
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝²⁸ : Semiring R₁
inst✝²⁷ : Semiring R₂
inst✝²⁶ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝²⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁴ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²³ : RingHomInvPair σ₂₃ σ₃₂
inst✝²² : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝²¹ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁰ : RingHomInvPair σ₃₁ σ₁₃
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : AddCommMonoid M₁
M₂ : Type u_5
inst✝¹⁵ : TopologicalSpace M₂
inst✝¹⁴ : AddCommMonoid M₂
M₃ : Type u_6
inst✝¹³ : TopologicalSpace M₃
inst✝¹² : AddCommMonoid M₃
M₄ : Type u_7
inst✝¹¹ : TopologicalSpace M₄
inst✝¹⁰ : AddCommMonoid M₄
inst✝⁹ : Module R₁ M₁
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Module R₃ M₃
R₄ : Type u_8
inst✝⁶ : Semiring R₄
inst✝⁵ : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝⁴ : RingHomInvPair σ₃₄ σ₄₃
inst✝³ : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst✝² : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
f : M₂ →SL[σ₂₃] M₃
x : M₂
⊢ ((fun f ↦ ↑e₄₃ ∘SL f ∘SL ↑e₁₂.symm) ((fun f ↦ ↑e₄₃.symm ∘SL f ∘SL ↑e₁₂) f)) x = f x

Tactic:
simp only [ContinuousLinearMap.comp_apply, apply_symm_apply, coe_coe]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
⊢ (𝟭 TopCat).map f ≫ TopCat.ofHom { toFun := fun x ↦ Finsupp.single x 1, continuous_toFun := ⋯ } =
    TopCat.ofHom { toFun := fun x ↦ Finsupp.single x 1, continuous_toFun := ⋯ } ≫
      (free R ⋙ forget₂ (TopModuleCat R) TopCat).map f

Tactic:
by ext x; simp [freeMap_map]

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ ((forget₂ (TopModuleCat R) TopCat).obj X).str ≤
    TopologicalSpace.induced
      (((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun ∘ fun x ↦
        Finsupp.single x 1)
      ((𝟭 (TopModuleCat R)).obj X).topologicalSpace

Tactic:
convert! induced_id.symm.le

Goal state after:
case e'_4.e'_3
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
e_2✝ : ↑((𝟭 (TopModuleCat R)).obj X).toModuleCat = ↑((forget₂ (TopModuleCat R) TopCat).obj X)
⊢ (((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun ∘ fun x ↦
      Finsupp.single x 1) =
    id
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
⊢ (piScalarRight R S N ι).symm (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1

Tactic:
by
  simp [piScalarRight]

Goal state after:
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁹ : AddCommGroup M₁
inst✝¹⁸ : Module R M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : Module R M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : Module R M₃
inst✝¹³ : AddCommGroup N₁
inst✝¹² : Module R N₁
inst✝¹¹ : AddCommGroup N₂
inst✝¹⁰ : Module R N₂
inst✝⁹ : AddCommGroup N₃
inst✝⁸ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁷ : AddCommGroup K₂
inst✝⁶ : Module R K₂
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
r : R
x : K₃
⊢ π₁ (ρ (i₂ (σ (ι₃ (r • x))))) = (RingHom.id R) r • π₁ (ρ (i₂ (σ (ι₃ x))))

Tactic:
simp only [← map_smul, RingHom.id_apply]

Goal state after:
R : Type u_1
inst✝²⁰ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁹ : AddCommGroup M₁
inst✝¹⁸ : Module R M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : Module R M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : Module R M₃
inst✝¹³ : AddCommGroup N₁
inst✝¹² : Module R N₁
inst✝¹¹ : AddCommGroup N₂
inst✝¹⁰ : Module R N₂
inst✝⁹ : AddCommGroup N₃
inst✝⁸ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁷ : AddCommGroup K₂
inst✝⁶ : Module R K₂
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
r : R
x : K₃
⊢ π₁ (ρ (i₂ (σ (ι₃ (r • x))))) = π₁ (r • ρ (i₂ (σ (ι₃ x))))