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
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.pullback b (G.imageSieve g), ⋯⟩),
    (mapPreimage K G F (f ≫ g) ≫ F.obj.map { Y := T₀, f := a, hf := ⋯ }.f.op) ≫ F.obj.map I.f.op =
      ((mapPreimage K G F g ≫ mapPreimage K G F f) ≫ F.obj.map { Y := T₀, f := a, hf := ⋯ }.f.op) ≫ F.obj.map I.f.op

Tactic:
rintro ⟨U₀, c, ⟨d, fac₂⟩⟩

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
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ (mapPreimage K G F (f ≫ g) ≫ F.obj.map { Y := T₀, f := a, hf := ⋯ }.f.op) ≫
      F.obj.map { Y := U₀, f := c, hf := ⋯ }.f.op =
    ((mapPreimage K G F g ≫ mapPreimage K G F f) ≫ F.obj.map { Y := T₀, f := a, hf := ⋯ }.f.op) ≫
      F.obj.map { Y := U₀, f := c, hf := ⋯ }.f.op
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
u₀ v₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)
h₀ : u₀ = v₀
h₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), u₁ k = (congrIndexOneOfEq ⋯ ⋯) (v₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) (v₁ k) = u₁ k

Tactic:
subst h₀

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
u₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
i j : E.I₀
k : E.I₁ i j
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
h₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), u₁ k = (congrIndexOneOfEq ⋯ ⋯) (v₁ k)
⊢ (congrIndexOneOfEq ⋯ ⋯) (v₁ k) = u₁ k
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 F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ IsIso (e.hom.h₁ k)

Tactic:
use e.inv.h₁ _ ≫ eqToHom (by congr 1; simp) ≫ (E.congrIndexOneOfEqIso (by simp) (by simp) k).hom

Goal state after:
case h
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 F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).hom = 𝟙 (E.Y k) ∧
    (e.inv.h₁ (e.hom.s₁ k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).hom) ≫ e.hom.h₁ k = 𝟙 (F.Y (e.hom.s₁ k))
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
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
⊢ (proj K B).mapCone (raiseCone c) = c

Tactic:
cat_disch

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

Goal state before:
pp: case refine_1
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
G : Cᵒᵖ ⥤ A
⊢ (E.multicospanIndex G).multicospan ≅ (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan

Tactic:
refine WalkingMulticospan.functorExt ?_ ?_ ?_ ?_
    · intro i
      exact G.mapIso (asIso (f.hom.h₀ i)).symm.op
    · intro i
      exact G.mapIso (asIso (f.hom.h₁ i.2)).symm.op
    · simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₁]
    · simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₂]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
⊢ functorPullback (Over.forget X) (map (Over.forget X) S) = S

Tactic:
suffices hR : (R.functorPullback (Over.forget X)) = S by
    rw [← hR, functorPullback_map_functorPullback]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Presieve Y
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
⊢ functorPullback (Over.forget X) R = S
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = T.hom

Tactic:
dsimp [T]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = b ≫ W.hom
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ Over.homMk f✝ ⋯ ≫ p₁ = Over.homMk b ⋯ ≫ E.p₁ k

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ Over.homMk f✝ ⋯ ≫ p₂ = Over.homMk b ⋯ ≫ E.p₂ k

Tactic:
cat_disch

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
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
hg : ((overEquiv ((Over.map f).obj Z)).symm S).arrows g
⊢ g = Over.homMk (𝟙 W.left) ⋯ ≫ (Over.map f).map (Over.homMk (Over.Hom.left g) ⋯)

Tactic:
cat_disch

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
x✝² : Sheaf J (Type u_1)
Z : Over X
x✝¹ : Presieve Z
x✝ : Presieve.FamilyOfElements ((Over.forget X).op ⋙ x✝².obj) x✝¹
hx : x✝.Compatible
Y₁ Y₂ : Over X
W : C
f₁ : W ⟶ (Over.forget X).obj Y₁
f₂ : W ⟶ (Over.forget X).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝¹ g₁
hg₂ : x✝¹ g₂
h : f₁ ≫ (Over.forget X).map g₁ = f₂ ≫ (Over.forget X).map g₂
W' : Over X := Over.mk (f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂ ⋯
⊢ (ConcreteCategory.hom (x✝².obj.map f₁.op)) (x✝ g₁ hg₁) = (ConcreteCategory.hom (x✝².obj.map f₂.op)) (x✝ g₂ hg₂)

Tactic:
exact hx g₁' g₂' hg₁ hg₂ (by ext; exact h)

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ (Sieve.overEquiv W) ((E.map (Over.post F)).sieve₁ p₁ p₂) ∈ K W.left

Tactic:
Sieve.overEquiv_preOneHypercover_sieve₁,

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ i₂ : E.I₀
W : Over (F.obj X)
p₁ : W ⟶ (Over.post F).obj (E.X i₁)
p₂ : W ⟶ (Over.post F).obj (E.X i₂)
w : p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂)
⊢ ((E.map (Over.post F)).map (Over.forget (F.obj X))).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂) ∈ K W.left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ (Over.mapId Y).inv.app ((Over.map f).obj (Opposite.unop x✝)) ≫ (Over.mapComp f (𝟙 Y)).inv.app (Opposite.unop x✝) =
    (Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x✝)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ (Over.map f).map ((Over.mapId X).inv.app (Opposite.unop x✝)) ≫ (Over.mapComp (𝟙 X) f).inv.app (Opposite.unop x✝) =
    (Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x✝)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x✝¹ : Sheaf (J.over T) A
x✝ : (Over X)ᵒᵖ
⊢ (Over.mapComp (f ≫ g) h).hom.app (Opposite.unop x✝) ≫
      (Over.map h).map ((Over.mapComp f g).hom.app (Opposite.unop x✝)) ≫
        (Over.mapComp g h).inv.app ((Over.map f).obj (Opposite.unop x✝)) ≫
          (Over.mapComp f (g ≫ h)).inv.app (Opposite.unop x✝) =
    (Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x✝)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
h : ¬kernel.ι f = 0
this : IsIso (kernel.ι f)
⊢ False

Tactic:
exact w (eq_zero_of_epi_kernel f)

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

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
inst✝¹ : Preorder X✝
inst✝ : Preorder Y✝
l : X✝ → Y✝
u : Y✝ → X✝
gc : GaloisConnection l u
X : X✝
Y : Y✝
⊢ Function.LeftInverse (fun f ↦ CategoryTheory.homOfLE ⋯) fun f ↦ CategoryTheory.homOfLE ⋯

Tactic:
cat_disch

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

Goal state before:
pp: X✝ : Type u
Y✝ : Type v
inst✝¹ : Preorder X✝
inst✝ : Preorder Y✝
l : X✝ → Y✝
u : Y✝ → X✝
gc : GaloisConnection l u
X : X✝
Y : Y✝
⊢ Function.RightInverse (fun f ↦ CategoryTheory.homOfLE ⋯) fun f ↦ CategoryTheory.homOfLE ⋯

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
by_cases h : i = 0

Goal state after:
case pos
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X✝ Y✝ Z : TopCat
U✝ V W : Opens ↑X✝
X Y : TopCat
H : X ≅ Y
U : Opens ↑Y
⊢ (𝟭 (Opens ↑Y)).obj U = ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).obj U

Tactic:
cat_disch

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

Goal state before:
pp: X✝ Y✝ Z : TopCat
U V W : Opens ↑X✝
X Y : TopCat
H : X ≅ Y
⊢ ∀ {X_1 Y_1 : Opens ↑Y} (f : X_1 ⟶ Y_1),
    (𝟭 (Opens ↑Y)).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ ((mapMapIso H).functor ⋙ (mapMapIso H).inverse).map f

Tactic:
cat_disch

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

Goal state before:
pp: X✝ Y✝ Z : TopCat
U✝ V W : Opens ↑X✝
X Y : TopCat
H : X ≅ Y
U : Opens ↑X
⊢ ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).obj U = (𝟭 (Opens ↑X)).obj U

Tactic:
cat_disch

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

Goal state before:
pp: X✝ Y✝ Z : TopCat
U V W : Opens ↑X✝
X Y : TopCat
H : X ≅ Y
⊢ ∀ {X_1 Y_1 : Opens ↑X} (f : X_1 ⟶ Y_1),
    ((mapMapIso H).inverse ⋙ (mapMapIso H).functor).map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (𝟭 (Opens ↑X)).map f

Tactic:
cat_disch

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 ι
g : ι → Opens ↑X
⊢ hf.functor.obj (⨅ i, g i) = ⨅ i, hf.functor.obj (g i)

Tactic:
ext : 1
  simp only [IsOpenMap.coe_functor_obj, TopologicalSpace.Opens.coe_iInf]
  rw [Set.InjOn.image_iInter_eq]
  exact hf.injective.injOn

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 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
⊢ φ = φ ≫ (sheafPushforwardContinuousNatTrans (𝟙 G) RingCat J K).app S

Tactic:
cat_disch

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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝ : G.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
⊢ pushforwardNatTrans φ (𝟙 G) = (pushforwardCongr ⋯).hom

Tactic:
cat_disch

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 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
β : G ⟶ H
φ : T ⟶ (H.sheafPushforwardContinuous RingCat J K).obj S
⊢ (φ ≫ (sheafPushforwardContinuousNatTrans β RingCat J K).app S) ≫
      (sheafPushforwardContinuousNatTrans α RingCat J K).app S =
    φ ≫ (sheafPushforwardContinuousNatTrans (α ≫ β) RingCat J K).app S

Tactic:
cat_disch

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
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
α : F ⟶ G
β : G ⟶ H
φ : T ⟶ (H.sheafPushforwardContinuous RingCat J K).obj S
⊢ pushforwardNatTrans φ (α ≫ β) =
    pushforwardNatTrans φ β ≫
      pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans β RingCat J K).app S) α ≫ (pushforwardCongr ⋯).hom

Tactic:
cat_disch

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

Goal state before:
pp: X : TopCat
F : Presheaf (Discrete Unit) X
x✝² : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝¹ : S ∈ (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op x✝²)) S.arrows
x✝ : x.Compatible
⊢ (fun t ↦ x.IsAmalgamation t) (eqToHom ⋯)

Tactic:
cat_disch

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

Goal state before:
pp: X : TopCat
F : Presheaf (Discrete Unit) X
x✝³ : Discrete Unit
U : Opens ↑X
S : Sieve U
x✝² : S ∈ (Opens.grothendieckTopology ↑X) U
x : Presieve.FamilyOfElements (F ⋙ coyoneda.obj (op x✝³)) S.arrows
x✝¹ : x.Compatible
x✝ : (F ⋙ coyoneda.obj (op x✝³)).obj (op U)
⊢ (fun t ↦ x.IsAmalgamation t) x✝ → x✝ = eqToHom ⋯

Tactic:
cat_disch

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

Goal state before:
pp: case op
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
U : Opens ↑X
⊢ f.app (op U) = g.app (op U)

Tactic:
| _ U =>

Goal state after:
case op
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
P Q : Presheaf C X
f g : P ⟶ Q
w : ∀ (U : Opens ↑X), f.app (op U) = g.app (op U)
U : Opens ↑X
⊢ f.app (op U) = g.app (op U)
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
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (Opens.map f).op.obj U = (Opens.map g).op.obj U

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
⊢ ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)).ι.app
      ((CostructuredArrow.map (homOfLE le).op).obj j)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)).ι.app
      ((CostructuredArrow.map (homOfLE le).op).obj j)
⊢ ℱ.map
      ((CostructuredArrow.proj (Opens.map f).op (op U)).map
        (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
          ((CostructuredArrow.map (homOfLE le).op).obj j))) =
    ℱ.map
      ((CostructuredArrow.proj (Opens.map f).op (op V)).map
          (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ } j) ≫
        (IsOpenMap.functorMap HU HV le).op)

Tactic:
cat_disch

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

Goal state before:
pp: case id_single
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ id_single i ∈ if h : i = i then {eqToHom ⋯} else ∅

Tactic:
cat_disch

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

Goal state before:
pp: case left
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ left i j ∈ (if h : i = i then {left i j ≫ eqToHom ⋯} else ∅) ∪ if h : j = i then {right i j ≫ eqToHom ⋯} else ∅

Tactic:
cat_disch

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

Goal state before:
pp: case right
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ right i j ∈ (if h : i = j then {left i j ≫ eqToHom ⋯} else ∅) ∪ if h : j = j then {right i j ≫ eqToHom ⋯} else ∅

Tactic:
cat_disch

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

Goal state before:
pp: case id_pair
ι : Type v
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i j : ι
⊢ id_pair i j ∈ if h : i = i ∧ j = j then {eqToHom ⋯} else ∅

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 : ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom),
    (𝟭 (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)).obj X_1 =
      (generateEquivalenceOpensLe_functor' U ⋙ generateEquivalenceOpensLe_inverse' U hY).obj X_1

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ ∀ (X_1 : OpensLeCover U),
    (generateEquivalenceOpensLe_inverse' U hY ⋙ generateEquivalenceOpensLe_functor' U).obj X_1 =
      (𝟭 (OpensLeCover U)).obj X_1

Tactic:
cat_disch

Goal state after: