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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ Sieve.pullback u ↑(x f hf) = ⊤

Tactic:
← show (x (u ≫ f) _).1 = (x f hf).1.pullback u from congr_arg Subtype.val (hx f u hf)

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ ↑(x (u ≫ f) ⋯) = ⊤
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)

Tactic:
exact
    { lift := PreservesFiniteLimitsOfFlat.lift F hc
      fac := PreservesFiniteLimitsOfFlat.fac F hc
      uniq := fun s m h => by
        apply PreservesFiniteLimitsOfFlat.uniq F hc
        · exact h
        · exact PreservesFiniteLimitsOfFlat.fac F hc s }

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
by
  let T := StructuredArrow.pre X F G
  obtain ⟨Y⟩ := IsCofiltered.nonempty (C := StructuredArrow X G)
  obtain ⟨A⟩ := IsCofiltered.nonempty (C := StructuredArrow Y.right F)
  have : Nonempty (StructuredArrow X (F ⋙ G)) := ⟨.mk (Y.hom ≫ G.map A.hom)⟩
  suffices IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G)) by constructor
  refine ⟨fun A B ↦ ?_, fun A B f g ↦ ?_⟩
  · let U := IsCofiltered.min (T.obj A) (T.obj B)
    let A' : StructuredArrow U.right F := .mk (IsCofiltered.minToLeft (T.obj A) (T.obj B)).right
    let B' : StructuredArrow U.right F := .mk (IsCofiltered.minToRight (T.obj A) (T.obj B)).right
    refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.min A' B').hom,
      StructuredArrow.homMk (IsCofiltered.minToLeft A' B').right ?_,
      StructuredArrow.homMk (IsCofiltered.minToRight A' B').right ?_, trivial⟩
    · simp [← Functor.map_comp, A', T]
    · simp [← Functor.map_comp, B', T]
  · let U := IsCofiltered.eq (T.map f) (T.map g)
    let A' : StructuredArrow _ F := .mk (IsCofiltered.eqHom (T.map f) (T.map g)).right
    let B' : StructuredArrow _ F := .mk (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f).right
    let f' : A' ⟶ B' := StructuredArrow.homMk f.right rfl
    let g' : A' ⟶ B' := StructuredArrow.homMk g.right
      congr($(IsCofiltered.eq_condition (T.map f) (T.map g)).right).symm
    refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.eq f' g').hom,
      StructuredArrow.homMk (IsCofiltered.eqHom f' g').right ?_, ?_⟩
    · simp [← Functor.map_comp, A', T]
    · ext
      exact congr($(IsCofiltered.eq_condition f' g').right)

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

Goal state before:
pp: case h
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ (Sieve.generate E.restrictIndexOfSmall.presieve₀).arrows ≤ (Sieve.generate E₀.presieve₀).arrows

Tactic:
exact Sieve.generate_mono (by simp [E])

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
⊢ Sieve.functorPushforward F (E.sieve₁ p₁ p₂) ≤ (E.map F).sieve₁ (F.map p₁) (F.map p₂)

Tactic:
rw [Sieve.functorPushforward_le_iff_le_functorPullback]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
⊢ E.sieve₁ p₁ p₂ ≤ Sieve.functorPullback F ((E.map F).sieve₁ (F.map p₁) (F.map p₂))
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
h : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
S : C
R : Presieve S
hR : R ∈ J.coverings S
⊢ IsSheafFor P R

Tactic:
simpa [Presieve.isSheafFor_iff_generate] using h (f := 𝟙 S) R hR

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
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
⊢ ∀ {Y Z : C} {f : Y ⟶ W},
    (∃ j h, f ≫ p₁ = h ≫ E.p₁ j ∧ f ≫ p₂ = h ≫ E.p₂ j) →
      ∀ (g : Z ⟶ Y), ∃ j h, (g ≫ f) ≫ p₁ = h ≫ E.p₁ j ∧ (g ≫ f) ≫ p₂ = h ≫ E.p₂ j

Tactic:
rintro Z Z' g ⟨j, h, fac₁, fac₂⟩ φ
    exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩

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
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
j j' : StructuredArrow (op X) G.op
φ : j ⟶ j'
⊢ (G.map (𝟙 (unop j'.right)) ≫ j'.hom.unop).op = (G.map (StructuredArrow.Hom.right φ).unop ≫ j.hom.unop).op

Tactic:
by simpa using (StructuredArrow.w φ).symm

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

Goal state before:
pp: case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.obj) S.arrows
hx : x.Compatible
⊢ ∀ (y₁ y₂ : (F.op ⋙ G.obj).obj (op X)), x.IsAmalgamation y₁ → x.IsAmalgamation y₂ → y₁ = y₂

Tactic:
intro y₁ y₂ hy₁ hy₂

Goal state after:
case hunique
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.obj) S.arrows
hx : x.Compatible
y₁ y₂ : (F.op ⋙ G.obj).obj (op X)
hy₁ : x.IsAmalgamation y₁
hy₂ : x.IsAmalgamation y₂
⊢ y₁ = y₂
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
⊢ mapPreimage K G F (f ≫ g) ≫ F.obj.map { Y := T₀, f := a, hf := ⋯ }.f.op =
    (mapPreimage K G F g ≫ mapPreimage K G F f) ≫ F.obj.map { Y := T₀, f := a, hf := ⋯ }.f.op

Tactic:
apply Presheaf.IsSheaf.hom_ext F.property
        ⟨_, J.pullback_stable b (imageSieve_mem J K G g)⟩

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
⊢ ∀ (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
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)
⊢ HasSheafify K A

Tactic:
have : PreservesFiniteLimits (sheafifyOfIsEquivalence J K G A) := by
    apply comp_preservesFiniteLimits

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
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
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
s₀ : E.I₀ ≃ F.I₀
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))

Tactic:
by
  apply Equiv.injective (s₁ (i := s₀.symm (s₀ i)) (j := s₀.symm (s₀ j)))
  simp [PreOneHypercover.congrIndexOneOfEq_naturality (u₁ := fun i j k ↦ s₁ k)]

Goal state after:
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
s₀ : E.I₀ ≃ F.I₀
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
i j : E.I₀
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ (h₁ k).hom ≫ (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv =
    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
by
  rw [← PreOneHypercover.congrIndexOneOfEqIso_inv_naturality_assoc
      (z := fun i j k ↦ (h₁ k).hom) (hii' := by simp) (hjj' := by simp),
      eqToHom_trans_assoc, eqToHom_iso_hom_naturality_assoc]
  · simp
  · apply PreOneHypercover.congrIndexOneOfEq_equiv

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),
    ((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
            { toHom := __Hom, s₁ := fun {i j} k ↦ s₁ k, h₁ := fun {i j} k ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
            let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
            { toHom := __Hom, s₁ := fun {i j} k ↦ s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k),
              h₁ := fun {i j} k ↦
                (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv,
              w₁₁ := ⋯, w₁₂ := ⋯ }).h₁
        k =
      (𝟙 E).h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ ((𝟙 E).s₁ k)).inv ≫ eqToHom ⋯

Tactic:
intro i j k

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
⊢ ((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
          { toHom := __Hom, s₁ := fun {i j} k ↦ s₁ k, h₁ := fun {i j} k ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
          let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
          { toHom := __Hom, s₁ := fun {i j} k ↦ s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k),
            h₁ := fun {i j} k ↦
              (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv,
            w₁₁ := ⋯, w₁₂ := ⋯ }).h₁
      k =
    (𝟙 E).h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ ((𝟙 E).s₁ k)).inv ≫ eqToHom ⋯
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✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹) F.rightOp

Tactic:
apply +allowSynthFailures createsColimitsOfShapeRightOp

Goal state after:
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✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹)ᵒᵖ F
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:
rw [← J.W_whiskerLeft_iff (G := G) (K := K)] at hf

Goal state after:
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 : K.W (G.op.whiskerLeft f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

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

Tactic:
intro y₁ y₂ hy₁ hy₂

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

Goal state before:
pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ᶜ f = Finset.univ.inf f

Tactic:
by
  trans
  · exact
      (IsLimit.conePointUniqueUpToIso (limit.isLimit _)
          (finiteLimitCone (Discrete.functor f)).isLimit).to_eq
  change Finset.univ.inf (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.inf f
  simp only [← Finset.inf_map, Finset.univ_map_equiv_to_embedding]
  rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F G : Sheaf C X
h : Opens.IsBasis (Set.range B)
φ : F ⟶ G
hi : ∀ (i : ι), IsIso (φ.hom.app (op (B i)))
⊢ IsIso φ

Tactic:
have : (inducedFunctor B).IsCoverDense (Opens.grothendieckTopology X) :=
    Opens.coverDense_inducedFunctor h

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F G : Sheaf C X
h : Opens.IsBasis (Set.range B)
φ : F ⟶ G
hi : ∀ (i : ι), IsIso (φ.hom.app (op (B i)))
this : (inducedFunctor B).IsCoverDense (Opens.grothendieckTopology ↑X)
⊢ IsIso φ
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
this : IsCompatible F.obj V sf
s : ToType (F.obj.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (iVU i).op)) s = sf i
x : ↥U
⊢ (ConcreteCategory.hom (G.obj.map (iVU x).op)) ((ConcreteCategory.hom (f.hom.app (op U))) s) =
    (ConcreteCategory.hom (G.obj.map (iVU x).op)) t

Tactic:
rw [← ConcreteCategory.comp_apply, ← f.1.naturality, ConcreteCategory.comp_apply, s_spec, heq]

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
i₁ : M →ₗ[R] P := LinearMap.inl R M N
i₂ : N →ₗ[R] P := LinearMap.inr R M N
⊢ Continuous i

Tactic:
show (i : M × N → P) =
       (fun abcd ↦ abcd.1 + abcd.2 : P × P → P) ∘
       (fun ab ↦ (i₁ ab.1, i₂ ab.2)) by
       ext ⟨a, b⟩ <;> aesop

Goal state after:
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
i₁ : M →ₗ[R] P := LinearMap.inl R M N
i₂ : N →ₗ[R] P := LinearMap.inr R M N
⊢ Continuous ((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2))
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
⊢ kerι φ ≫ φ = 0

Tactic:
by ext ⟨_, hm⟩; exact hm

Goal state after:
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β = F.map α ≫ (h.isoMap β ⋯).inv ≫ F.map β

Tactic:
isoMap_inv_hom_id,

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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β = F.map α ≫ 𝟙 (F.obj j')
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
⊢ Continuous (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun

Tactic:
by
    rw [continuous_iff_coinduced_le]
    refine le_iInf fun i ↦ ?_
    rw [coinduced_le_iff_le_induced, induced_compose, ← continuous_iff_le_induced]
    change Continuous (X := s.pt) (Y := F.obj i)
      (hc.lift ((forget₂ _ (ModuleCat R)).mapCone s) ≫ c.π.app i).hom
    rw [hc.fac]
    exact (s.π.app i).hom.2

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
⊢ (forget₂ (TopModuleCat R) TopCat ⋙ free R).map f ≫
      ConcreteCategory.ofHom
        { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat) R ↑Y.toModuleCat) id, cont := ⋯ } =
    ConcreteCategory.ofHom
        { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id, cont := ⋯ } ≫
      (𝟭 (TopModuleCat R)).map f

Tactic:
ext1
      apply ContinuousLinearMap.coe_injective
      refine Finsupp.lhom_ext' fun a ↦ LinearMap.ext_ring ?_
      dsimp [freeObj, freeMap]
      simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
⊢ (toSpanSingleton R N (s • x)).compLeft ι = (RingHom.id S) s • (toSpanSingleton R N x).compLeft ι

Tactic:
by
    ext i j
    dsimp only [coe_comp, coe_single, Function.comp_apply, compLeft_apply, toSpanSingleton_apply,
      RingHom.id_apply, smul_apply, Pi.smul_apply]
    rw [← IsScalarTower.smul_assoc, _root_.Algebra.smul_def, mul_comm, mul_smul]
    simp

Goal state after: