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

Goal state before:
pp: case refine_2.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).toPullback k =
    f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯
⊢ (E.sieve₁' i₁ i₂).arrows (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)

pp: case refine_2.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).toPullback k =
    f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯
⊢ f = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)

Tactic:
· use E.Y k, 𝟙 _, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), ⟨k⟩
      simp

Goal state after:
case refine_2.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).toPullback k =
    f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯
⊢ f = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F 𝒰.presieve₀ ↔ Presieve.IsSheafFor F 𝒱.presieve₀

Tactic:
rw [Presieve.isSheafFor_iff_generate, ← Sieve.ofArrows, ← PreZeroHypercover.sieve₀,
    PreZeroHypercover.sieve₀_eq_of_iso e, ← Presieve.isSheafFor_iff_generate]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
X₁ : C
f₁ : X₁ ⟶ Z
h₁ : Z₁ ⟶ G.obj X₁
hf₁ : T f₁
H₁ : Presieve.functorPushforward G T (h₁ ≫ G.map f₁)
X₂ : C
f₂ : X₂ ⟶ Z
h₂ : Z₂ ⟶ G.obj X₂
hf₂ : T f₂
H₂ : Presieve.functorPushforward G T (h₂ ≫ G.map f₂)
eq : g₁ ≫ h₁ ≫ G.map f₁ = g₂ ≫ h₂ ≫ G.map f₂
this :
  (ConcreteCategory.hom (ℱ.obj.map (g₁ ≫ h₁).op)) (x f₁ hf₁) =
    (ConcreteCategory.hom (ℱ.obj.map (g₂ ≫ h₂).op)) (x f₂ hf₂)
⊢ (ConcreteCategory.hom (ℱ.obj.map g₁.op))
      (FunctorPushforwardStructure.casesOn { preobj := X₁, premap := f₁, lift := h₁, cover := hf₁, fac := ⋯ }
        fun Z_1 g h h₁_1 fac ↦ (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁_1)) =
    (ConcreteCategory.hom (ℱ.obj.map g₂.op))
      (FunctorPushforwardStructure.casesOn { preobj := X₂, premap := f₂, lift := h₂, cover := hf₂, fac := ⋯ }
        fun Z_1 g h h₁ fac ↦ (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁))

Tactic:
simpa using this

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 : PreOneHypercover S
F : Cᵒᵖ ⥤ A
i₁ i₂ : E.I₀
j : E.I₁ i₁ i₂
⊢ F.map (E.f i₁).op ≫ F.map (E.p₁ j).op = F.map (E.f i₂).op ≫ F.map (E.p₂ j).op

Tactic:
simp only [← F.map_comp, ← op_comp, E.w]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝² : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : G.IsCocontinuous J K
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
X : D
S : K.Cover X
⊢ Nonempty (IsLimit (S.multifork (G.op.ran.obj ℱ.obj)))

Tactic:
exact ⟨RanIsSheafOfIsCocontinuous.isLimitMultifork ℱ.2
    (G.op.isPointwiseRightKanExtensionRanCounit ℱ.obj) S⟩

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

Goal state before:
pp: case h.right
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
x : Aᵒᵖ
⊢ ((sheafYonedaHom i.inv).app X).app x ≫ ((sheafYonedaHom i.hom).app X).app x = 𝟙 ((yoneda.obj (ℱ'.obj.obj X)).obj x)

Tactic:
· exact ((Types.presheafIso (isoOver i (unop x))).app X).inv_hom_id

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

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op (G.map i ≫ g₁))).hom
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩
⊢ f ≫ Y.obj.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op =
    ⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i ≫ I.f.op)

Tactic:
let I' : GrothendieckTopology.Cover.Arrow ⟨_, IsDenseSubsite.imageSieve_mem J K G g₁⟩ :=
          ⟨_, I.f ≫ i, ⟨l _ _ _ _ _ I.hf, by simp [hl]⟩⟩

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op (G.map i ≫ g₁))).hom
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩
I' : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g₁, ⋯⟩ := { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
⊢ f ≫ Y.obj.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op =
    ⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i ≫ I.f.op)
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F✝ : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ colim.mapCone c ≅ colim.mapCone (limit.cone F)

Tactic:
exact Functor.mapIso _ (hc.uniqueUpToIso (limit.isLimit F))

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : J.W f
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
by
    rw [← J.W_whiskerLeft_iff (G := G) (K := K)] at hf
    have := K.W_of_preservesSheafification F (whiskerLeft G.op f) hf
    rw [whiskerRight_left] at this
    have := K.W.of_postcomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_inv _) <|
      K.W.of_precomp (W' := MorphismProperty.isomorphisms _) _ _ (Iso.isIso_hom _) this
    rwa [K.W_whiskerLeft_iff (G := G) (J := J) (f := whiskerRight f F)] at this

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
⊢ b ≫ (E.Y k).hom = (Over.mk (f✝ ≫ W.hom)).hom

Tactic:
simpa using (hb₁ =≫ (E.X i₁).hom).symm

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
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
⊢ m = multiforkLift c

Tactic:
apply F.property.hom_ext_ofArrows _ E.mem₀

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
⊢ ∀ (i : E.I₀), m ≫ F.obj.map (E.f i).op = multiforkLift c ≫ F.obj.map (E.f i).op
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (fun j_1 ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).f

Tactic:
ext <;> simp [PreOneHypercover.toPullback]

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₂)
⊢ (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
simp_rw [GrothendieckTopology.mem_over_iff, Sieve.overEquiv_preOneHypercover_sieve₁,
      ← PreOneHypercover.map_comp, Over.post_forget_eq_forget_comp, PreOneHypercover.map_comp]

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.forget X)).map F).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂) ∈ K W.left
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2.refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
⊢ (ConcreteCategory.hom (P.map f)) (val Y₁) = val Y₂

pp: case refine_2.refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
⊢ F.sectionsPrecomp ⟨val, ⋯⟩ = t

Tactic:
· let X : CostructuredArrow F Y₁ := Classical.arbitrary _
      simp [← hval Y₁ X, ← hval Y₂ ((CostructuredArrow.map f).obj X)]

Goal state after:
case refine_2.refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
⊢ F.sectionsPrecomp ⟨val, ⋯⟩ = t
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2.refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
⊢ F.sectionsPrecomp ⟨val, ⋯⟩ = t

Tactic:
ext X : 2

Goal state after:
case refine_2.refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
X : C
⊢ ↑(F.sectionsPrecomp ⟨val, ⋯⟩) X = ↑t X
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi (factorThruImage f ≫ image.ι f)

Tactic:
have : IsIso (image.ι f) := isIso_of_mono_of_nonzero fun h => w (eq_zero_of_image_eq_zero h)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
this : IsIso (image.ι f)
⊢ Epi (factorThruImage f ≫ image.ι f)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
⊢ False

Tactic:
have := isIso_of_epi_of_nonzero h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
this : IsIso (cokernel.π f)
⊢ False
Module: Mathlib.CategoryTheory.Simple

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

Tactic:
change biprod.inl ≠ 0 at h

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

Goal state before:
pp: α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cone F
j : J
⊢ s.pt ≤ F.obj j

Tactic:
exact (s.π.app j).le

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
h : F.IsSheaf
⊢ Sieve.generate (presieveOfCoveringAux U (iSup U)) ∈ (Opens.grothendieckTopology ↑X) (iSup U)

Tactic:
apply presieveOfCovering.mem_grothendieckTopology

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

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
⊢ F.IsGluing U sf s ↔
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i

Tactic:
refine ⟨fun h ↦ ?_, fun h i ↦ h (op <| Pairwise.single i)⟩

Goal state after:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
⊢ ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
    (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case hcover
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₁ ⊔ U₂ ≤ ⨆ t, if t = true then U₁ else U₂

Tactic:
sup_le_iff

Goal state after:
case hcover
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₂) ∧ U₂ ≤ ⨆ t, if t = true then U₁ else U₂
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Set M
⊢ closure[inst✝⁴] s ⊆ closure[inst✝⁴] ↑(span R s)

Tactic:
exact closure_mono subset_span

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
A : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : (i : ι) → TopologicalSpace (A i)
inst✝ : ∀ (i : ι), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : ι) → A i)

Tactic:
induction ι using Finite.induction_empty_option
  · -- invariance under equivalence of the finite type we're taking the product over
    case of_equiv X Y e _ _ _ _ _ =>
    exact .iso (ContinuousLinearEquiv.piCongrLeft R A e)
  · -- empty case
    infer_instance
  · -- "inductive step" is to check for product over `Option ι` case when known for product over `ι`
    case h_option ι _ hind _ _ _ _ =>
    -- `Option ι` is a `Sum` of `ι` and `Unit`
    let e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
    -- so suffices to check for a product of modules over `ι ⊕ Unit`
    suffices IsModuleTopology R ((i' : ι ⊕ Unit) → A (e.symm i')) from
      .iso (.piCongrLeft R A e.symm)
    -- but such a product is isomorphic to a binary product
    -- of (product over `ι`) and (product over `Unit`)
    suffices IsModuleTopology R
      (((s : ι) → A (e.symm (Sum.inl s))) × ((t : Unit) → A (e.symm (Sum.inr t)))) from
      .iso (ContinuousLinearEquiv.sumPiEquivProdPi R ι Unit _).symm
    -- The product over `ι` has the module topology by the inductive hypothesis,
    -- and the product over `Unit` is just a module which is assumed to have the module topology
    have :=
      IsModuleTopology.iso (ContinuousLinearEquiv.piUnique R (fun t ↦ A (e.symm (Sum.inr t)))).symm
    -- so the result follows from the previous lemma (binary products).
    infer_instance

Goal state after:
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
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → descFunLift F s a = descFunLift F s b

Tactic:
· intro x y r
    induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (φ i)
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
h✝ : i ∈ I
⊢ Continuous[Pi.topologicalSpace, inst✝³ i] fun a ↦ (LinearMap.proj ⟨i, h✝⟩) a

Tactic:
apply continuous_apply

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
x y : (M →L[R] M)ˣ
⊢ ofUnit (x * y) = ofUnit x * ofUnit y

Tactic:
ext
    rfl

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
h : IsEffective R S
⊢ ↑(TensorProduct.includeLeftRingHom.eqLocus TensorProduct.includeRight.toRingHom) = Set.range ⇑(algebraMap R S)

Tactic:
by
  ext s
  refine ⟨?_, fun ⟨_, hr⟩ ↦ by simp [← hr]⟩
  intro hs
  exact (h s).mp <| (TensorProduct.includeLeftSubRight_apply (R := R) s).symm ▸ sub_eq_zero.mpr hs

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

Goal state before:
pp: 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).IsInvertible

Tactic:
simp [hf]

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

Goal state before:
pp: 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).IsInvertible

Tactic:
simp [hf]

Goal state after: