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
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x : (fun X ↦ X) ((G.op ⋙ ℱ).obj (op Y))
this :
  ∀ {X Y : C} (i : X ⟶ Y) (x : (fun X ↦ X) ((G.op ⋙ ℱ).obj (op Y))),
    (ConcreteCategory.hom (ℱ'.obj.map (G.map i).op)) ((ConcreteCategory.hom (α.app (op Y))) x) =
      (ConcreteCategory.hom (α.app (op X))) ((ConcreteCategory.hom (ℱ.map (G.map i).op)) x)
V : C
iVX : V ⟶ X
iVY : V ⟶ Y
e : G.map iVY = G.map iVX ≫ i
⊢ (ConcreteCategory.hom (ℱ'.obj.map (G.map iVX).op))
      ((ConcreteCategory.hom (ℱ'.obj.map i.op)) ((ConcreteCategory.hom (α.app (op Y))) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (G.map iVX).op))
      ((ConcreteCategory.hom (α.app (op X))) ((ConcreteCategory.hom (ℱ.map i.op)) x))

Tactic:
simp only [← Functor.map_comp_apply, ← op_comp, ← e, this]

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
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ pushforwardFamily α x f ⋯ = (ConcreteCategory.hom (α.app (op Y))) ((ConcreteCategory.hom (ℱ.map f.op)) x)

Tactic:
simp only [pushforwardFamily_def, op_obj]
  generalize Nonempty.some (Presieve.in_coverByImage G f) = l
  obtain ⟨W, iYW, iWX, rfl⟩ := l
  simp only [← op_comp, ← Functor.map_comp_apply, naturality_apply]

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

Goal state before:
pp: case refine_2
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
H : ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)
⊢ ∀ P ∈ Set.range fun G ↦ F.op ⋙ G.obj, ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows

Tactic:
rintro - ⟨P, rfl⟩ Y f

Goal state after:
case refine_2
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
H : ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)
P : Sheaf K (Type (max u₁ v₁ u₂ v₂))
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor ((fun G ↦ F.op ⋙ G.obj) P) (Sieve.pullback f S).arrows
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
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫
        eqToHom ⋯ ≫
          (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv ≫ E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    E.p₁ k ≫ eqToHom ⋯

Tactic:
PreOneHypercover.isoMk_aux_assoc,

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✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) = E.p₁ k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case 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
⊢ (comap F K).toGrothendieck ≤ F.restrictedTopology K.toGrothendieck

Tactic:
apply toGrothendieck_comap_le_restrictedTopology

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫
        eqToHom ⋯ ≫
          (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv ≫ E.p₂ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    E.p₂ k ≫ eqToHom ⋯

Tactic:
PreOneHypercover.isoMk_aux_assoc,

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✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ E.p₂ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) = E.p₂ k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J : Type u_1
⊢ IsConnected (WidePushoutShape J)

Tactic:
by
  apply IsConnected.of_constant_of_preserves_morphisms
  intro α F H
  suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm
  rintro ⟨⟩
  exacts [rfl, (H (.init _)).symm]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ Sieve.ofObjects Y X ∈ J X → J.CoversTop Y

Tactic:
intro h W

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
h : Sieve.ofObjects Y X ∈ J X
W : C
⊢ Sieve.ofObjects Y W ∈ J W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ generate (Presieve.functorPushforward (Over.forget X) R) ≤ (overEquiv Y) (generate R)

Tactic:
rw [generate_le_iff]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ Presieve.functorPushforward (Over.forget X) R ≤ ((overEquiv Y) (generate R)).arrows
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ generate (Presieve.functorPullback (Over.forget X) R) ≤ (overEquiv Y).symm (generate R)

Tactic:
rw [generate_le_iff]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ Presieve.functorPullback (Over.forget X) R ≤ ((overEquiv Y).symm (generate R)).arrows
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
⊢ 𝟙 W.left ≫ ((Over.map f).obj (Over.mk (Over.Hom.left g ≫ Z.hom))).hom = W.hom

Tactic:
by simpa using Over.w g

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
a : Subobject X
⊢ a = ⊥ ∨ a = ⊤

Tactic:
obtain ⟨Y, i, _, rfl⟩ := Subobject.mk_surjective a
    by_cases h : i = 0
    · exact Or.inl (mk_eq_bot_iff_zero.mpr h)
    · exact Or.inr ((isIso_iff_mk_eq_top _).mp ((Simple.mono_isIso_iff_nonzero i).mpr h))

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

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y : α
⊢ limit (pair x y) = Finset.univ.inf (pair x y).obj

Tactic:
by rw [finite_limit_eq_finset_univ_inf (pair.{u} x y)]

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
⊢ pushforwardNatTrans φ α.hom ≫
      pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) α.inv ≫
        (pushforwardCongr ⋯).hom =
    𝟙 (pushforward φ)

Tactic:
ext X U x

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 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
X : SheafOfModules S
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ModuleCat.Hom.hom
        (((pushforwardNatTrans φ α.hom ≫
                    pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) α.inv ≫
                      (pushforwardCongr ⋯).hom).app
                X).val.app
          U))
      x =
    (ModuleCat.Hom.hom (((𝟙 (pushforward φ)).app 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 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
⊢ (pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) α.inv ≫
        (pushforwardCongr ⋯).hom) ≫
      pushforwardNatTrans φ α.hom =
    𝟙 (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S))

Tactic:
ext X U x

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 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
X : SheafOfModules S
U : Cᵒᵖ
x : ↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)).obj X).val.obj U)
⊢ (ModuleCat.Hom.hom
        ((((pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) α.inv ≫
                      (pushforwardCongr ⋯).hom) ≫
                    pushforwardNatTrans φ α.hom).app
                X).val.app
          U))
      x =
    (ModuleCat.Hom.hom
        (((𝟙 (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S))).app X).val.app U))
      x
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
⊢ ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
U

Goal state after:
case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
U : Opens ↑X
⊢ ∀ {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
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
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
⊢ Epi (M.freeHomEquiv.symm (M.freeHomEquiv g))

Tactic:
by simpa using! epi_of_isColimit_cofork H'

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ germToPullbackStalk C f F U x hx ≫ stalkPullbackHom C f F x = ((pullback C f).obj F).germ U x hx

Tactic:
ext V hV
  dsimp
  simp only [pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc,
    germ_stalkPullbackHom, germ_res]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
V : Opens ↑X
hV : x ∈ V
⊢ ((pullback C f).obj F).germ V x hV ≫ stalkPullbackInv C f F x = germToPullbackStalk C f F V x hV

Tactic:
by
  apply colimit.ι_desc

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✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 • p.2

Tactic:
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (fun x ↦ (AddMonoidHom.smul x.1) x.2) (0, 0)

case refine_2
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R), ContinuousAt (⇑(AddMonoidHom.smul x)) 0

case refine_3
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ∀ (y : M), ContinuousAt (fun x ↦ (AddMonoidHom.smul x) y) 0
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c ↦ x + c • y) (𝓝 0) (𝓝 x)

pp: case refine_2
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ ∀ a ∈ {0}ᶜ, x + a • y ∈ {x}ᶜ

Tactic:
· convert! tendsto_const_nhds.add ((@tendsto_id R _).zero_smul_const y)
    rw [add_zero]

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ ∀ a ∈ {0}ᶜ, x + a • y ∈ {x}ᶜ
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
⊢ ∀ (o : Set ((i : ι) → M i)),
    IsOpen[Pi.topologicalSpace] o → x ∈ o → (o ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty

Tactic:
U

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
⊢ IsOpen[Pi.topologicalSpace] U → x ∈ U → (U ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
⊢ ∃ x, f x ≠ 0

Tactic:
by
  by_contra! h
  exact hf (ContinuousLinearMap.ext h)

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

Goal state before:
pp: R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₂
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₂
c : R₁ →L[R₁] M₂
⊢ toSpanSingleton R₁ (c 1) = c

Tactic:
by
  ext
  simp [← ContinuousLinearMap.map_smul_of_tower]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: M N : AddCommMonCat
f : M ⟶ N
⊢ (forget AddCommMonCat ⋙ free).map f ≫ ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑N)) =
    ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑M)) ≫ (𝟭 AddCommMonCat).map f

Tactic:
ext1; apply Finsupp.liftAddHom.symm.injective; cat_disch

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

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

Tactic:
let isPushout : IsPushout (ofHom (algebraMap R S)) (ofHom (algebraMap R S))
      (pushoutCocone R S S).inl (pushoutCocone R S S).inr :=
    ⟨⟨PushoutCocone.condition (pushoutCocone R S S)⟩, ⟨pushoutCoconeIsColimit R S S⟩⟩

Goal state after:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
fork : Fork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr := Fork.ofι (ofHom (algebraMap ↑R ↑S)) ⋯
isPushout : IsPushout (ofHom (algebraMap ↑R ↑S)) (ofHom (algebraMap ↑R ↑S)) (pushoutCocone ↑R ↑S ↑S).inl
  (pushoutCocone ↑R ↑S ↑S).inr :=
  { w := PushoutCocone.condition (pushoutCocone ↑R ↑S ↑S),
    isColimit' := Nonempty.intro (pushoutCoconeIsColimit ↑R ↑S ↑S) }
⊢ IsLimit (Fork.ofι f ⋯)
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case pos
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₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (↑e.symm ∘SL ↑e')⁻¹ʳ ∘SL ↑e.symm

Tactic:
change _ = (e'.trans e.symm : M →L[R] M)⁻¹ʳ ∘L (e.symm : M₂ →L[R] M)

Goal state after:
case pos
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₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (↑(e'.trans e.symm))⁻¹ʳ ∘SL ↑e.symm
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Ring.inverse = inverse

Tactic:
by
  ext
  simp [inverse_eq_ringInverse (ContinuousLinearEquiv.refl R M)]

Goal state after: