mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := ⋯
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ ((a ≫ b) ≫ p₁) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd) =
    (pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₁ (k, l)) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd)

Tactic:
· simpa using u₁

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
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ F.obj.map ((Exists.choose ha).op ≫ { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁.op) =
    F.obj.map ((Exists.choose ha').op ≫ { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂.op)

Tactic:
← op_comp,

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
E : Type u_3
inst✝² : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ F.obj.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ Exists.choose ha).op =
    F.obj.map ((Exists.choose ha').op ≫ { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂.op)
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
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ mapPreimage K G F f ≫ F.obj.map (p.op ≫ a.op) = F.obj.map g.op ≫ F.obj.map a.op

Tactic:
← op_comp,

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
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
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ mapPreimage K G F f ≫ F.obj.map (a ≫ p).op = F.obj.map g.op ≫ F.obj.map a.op
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
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq : d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op = d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op
⊢ d.ι (f.s₀ k.fst.1) ≫ P.map ((f.h₀ k.fst.1).op ≫ (E.p₁ k.snd).op) =
    d.ι (f.s₀ k.fst.2) ≫ P.map (f.h₀ k.fst.2).op ≫ P.map (E.p₂ k.snd).op

Tactic:
← op_comp,

Goal state after:
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
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq : d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op = d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op
⊢ d.ι (f.s₀ k.fst.1) ≫ P.map (E.p₁ k.snd ≫ f.h₀ k.fst.1).op =
    d.ι (f.s₀ k.fst.2) ≫ P.map (f.h₀ k.fst.2).op ≫ P.map (E.p₂ k.snd).op
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
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq : d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op = d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op
⊢ d.ι (f.s₀ k.fst.1) ≫ P.map (f.h₁ k.snd ≫ F.p₁ (f.s₁ k.snd)).op =
    d.ι (f.s₀ k.fst.2) ≫ P.map ((f.h₀ k.fst.2).op ≫ (E.p₂ k.snd).op)

Tactic:
← op_comp,

Goal state after:
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
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq : d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op = d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op
⊢ d.ι (f.s₀ k.fst.1) ≫ P.map (f.h₁ k.snd ≫ F.p₁ (f.s₁ k.snd)).op =
    d.ι (f.s₀ k.fst.2) ≫ P.map (E.p₂ k.snd ≫ f.h₀ k.fst.2).op
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✝
S : C
E✝ : PreOneHypercover S
F : PreOneHypercover S
i✝ i'✝ j✝ j'✝ : E✝.I₀
hii'✝ : i✝ = i'✝
hjj'✝ : j✝ = j'✝
E : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ E.Y ((congrIndexOneOfEq hii' hjj') k) = E.Y k

Tactic:
subst hii' hjj'; 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
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✝¹ : HasSheafify J A
inst✝ : HasFiniteLimits A
this✝ : PreservesFiniteLimits (presheafToSheaf J A ⋙ (G.sheafPushforwardContinuous A J K).inv)
this : PreservesFiniteLimits (sheafifyOfIsEquivalence J K G A)
⊢ HasSheafify K A

Tactic:
exact HasSheafify.mk' _ _ (sheafifyAdjunctionOfIsEquivalence J K G A)

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
x✝ : (Sieve.pullback g R).arrows f
⊢ Presieve.IsSeparatedFor P (Sieve.pullback (f ≫ g) S).arrows

Tactic:
apply (hS _ _).isSeparatedFor

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

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
⊢ S ∈ (F.inducedTopology K) X →
    ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)

Tactic:
intro hS Y f
    apply Functor.W_map_of_adjunction_of_isContinuous (F.inducedTopology K) K _ G adj
    refine Sieve.W_shrinkFunctor_ι_of_mem (F.inducedTopology K) (Sieve.pullback f S) ?_
    exact GrothendieckTopology.pullback_stable (F.inducedTopology K) f 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✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.op

Tactic:
apply +allowSynthFailures createsLimitsOfShapeOp
    exact createsColimitsOfShapeOfEquiv (Discrete.opposite _).symm _

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ (PreZeroHypercover.map (Over.forget X) E.toPreZeroHypercover).sieve₀ ∈ J Y.left

Tactic:
dsimp% PreZeroHypercover.sieve₀_map (F := Over.forget X)

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ Sieve.functorPushforward (Over.forget X) E.sieve₀ ∈ J Y.left
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False

Tactic:
rw [Simple.mono_isIso_iff_nonzero] at j

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : IsIso f
w : f = 0
j : f ≫ i.hom ≠ 0
⊢ False
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
H : Mono f
X✝ Y✝ : Opens ↑X
i : hf.functor.obj X✝ ⟶ hf.functor.obj Y✝
x : ↑X
hx : x ∈ X✝
⊢ x ∈ Y✝

Tactic:
obtain ⟨y, hy, eq⟩ := i.le ⟨x, hx, rfl⟩
      exact (TopCat.mono_iff_injective f).mp H eq ▸ hy

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X Y : Opens T
S : Sieve X
f : Y ⟶ X
hf : S ∈ {S | ∀ x ∈ X, ∃ U f, S.arrows f ∧ x ∈ U}
y : T
hy : y ∈ Y
U : Opens T
g : U ⟶ X
hg : S.arrows g
hU : y ∈ U
⊢ (Sieve.pullback f S).arrows (homOfLE ⋯)

Tactic:
apply S.downward_closed hg (homOfLE inf_le_left)

Goal state after:
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 : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules R
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ConcreteCategory.hom
        (X.val.presheaf.map
          ((adj.counit.app (F.obj (Opposite.unop U))).op ≫ (F.map (adj.unit.app (Opposite.unop U))).op)))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward φ).obj X)).val.app U)) x

Tactic:
← op_comp,

Goal state after:
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 : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules R
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ConcreteCategory.hom
        (X.val.presheaf.map (F.map (adj.unit.app (Opposite.unop U)) ≫ adj.counit.app (F.obj (Opposite.unop U))).op))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward φ).obj X)).val.app U)) x
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 : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules S
U : Dᵒᵖ
x : ↑(((pushforward ψ).obj X).val.obj U)
⊢ (ConcreteCategory.hom
        (X.val.presheaf.map
          ((G.map (adj.counit.app (Opposite.unop U))).op ≫ (adj.unit.app (G.obj (Opposite.unop U))).op)))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward ψ).obj X)).val.app U)) x

Tactic:
← op_comp,

Goal state after:
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 : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules S
U : Dᵒᵖ
x : ↑(((pushforward ψ).obj X).val.obj U)
⊢ (ConcreteCategory.hom
        (X.val.presheaf.map (adj.unit.app (G.obj (Opposite.unop U)) ≫ G.map (adj.counit.app (Opposite.unop U))).op))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward ψ).obj X)).val.app U)) x
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_1
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
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
⊢ ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj ≅
    ((forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
            sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
              F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).obj
        M).obj

Tactic:
refine NatIso.ofComponents (fun U ↦ ?_) ?_
    · refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫
        (ModuleCat.restrictScalarsComp _ _).app _
      rw [← RingCat.hom_comp, ← RingCat.hom_comp, φ.hom.naturality]
      dsimp
      rw [hX'.hom_ext (hX'.to (Opposite.op (F.obj (Opposite.unop U)))) _]
    · cat_disch

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsCompatible F.obj U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.obj.obj (op (iSup U)))
gl_spec : IsGluing F.obj U sf gl
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
⊢ ∀ (y : ToType (F.obj.obj (op V))),
    (fun s ↦ ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = sf i) y →
      y = (ConcreteCategory.hom (F.obj.map (eqToHom V_eq_supr_U).op)) gl

Tactic:
intro gl' gl'_spec
    convert! congr_arg _ (gl_uniq (F.1.map (eqToHom V_eq_supr_U.symm).op gl') fun i => _) <;>
      rw [← ConcreteCategory.comp_apply, ← F.1.map_comp]
    · simp
    · exact gl'_spec i

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

Goal state before:
pp: case hcover.right
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ U₂ ≤ ⨆ t, if t = true then U₁ else U₂

Tactic:
· exact le_iSup (fun t : Bool => if t then U₁ else U₂) false

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
S : Submodule R M
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalAddGroup M
inst✝ : ContinuousSMul R M
⊢ Continuous[instTopologicalSpaceProd, QuotientModule.Quotient.topologicalSpace S]
    ((fun p ↦ p.1 • p.2) ∘ Prod.map id ⇑S.mkQ)

Tactic:
exact continuous_quot_mk.comp continuous_smul

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

Goal state before:
pp: R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
⊢ Continuous ⇑φ

Tactic:
by
  let inst := Module.compHom B (φ.comp (algebraMap R A))
  let φ' : A →ₗ[R] B := ⟨φ, fun r m ↦ by simp [Algebra.smul_def]; rfl⟩
  have : ContinuousSMul R B := ⟨(hφ.comp continuous_fst).mul continuous_snd⟩
  exact continuous_of_linearMap φ'

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : f.IsInvertible
⊢ (↑e ∘SL f).inverse = f.inverse ∘SL ↑e.symm

Tactic:
rcases hf with ⟨A, rfl⟩

Goal state after:
case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
A : M ≃L[R] M₂
⊢ (↑e ∘SL ↑A).inverse = (↑A).inverse ∘SL ↑e.symm
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : f.IsInvertible
⊢ (f ∘SL ↑e).inverse = ↑e.symm ∘SL f.inverse

Tactic:
rcases hf with ⟨A, rfl⟩

Goal state after:
case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
A : M ≃L[R] M₂
⊢ (↑A ∘SL ↑e).inverse = ↑e.symm ∘SL (↑A).inverse
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map (γ ≫ minToLeft i₀ j) ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) =
    F.map γ ≫ F.map (minToRight i₀ j)

Tactic:
F.map_comp_assoc,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map γ ≫ F.map (minToLeft i₀ j) ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) =
    F.map γ ≫ F.map (minToRight i₀ j)