mathlib-initiative/mathlib-tactics huggingface dataset:
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
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ Hom.right g₁ = hc.lift (c.extend (Hom.right g₁))

Tactic:
apply hc.uniq (c.extend _)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := ⋯
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := ⋯
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₀ : Cone (biconeMk J c₁ c₂) := ⋯
g₁ : c₀.pt ⟶ c₁.pt := ⋯
g₂ : c₀.pt ⟶ c₂.pt := ⋯
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ ∀ (j : J), Hom.right g₁ ≫ c.π.app j = (c.extend (Hom.right g₁)).π.app j
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
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := ⋯
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := ⋯
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₀ : Cone (biconeMk J c₁ c₂) := ⋯
g₁ : c₀.pt ⟶ c₁.pt := ⋯
g₂ : c₀.pt ⟶ c₂.pt := ⋯
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ Hom.right g₂ = hc.lift (c.extend (Hom.right g₂))

Tactic:
apply hc.uniq (c.extend _)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := ⋯
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := ⋯
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₀ : Cone (biconeMk J c₁ c₂) := ⋯
g₁ : c₀.pt ⟶ c₁.pt := ⋯
g₂ : c₀.pt ⟶ c₂.pt := ⋯
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ ∀ (j : J), Hom.right g₂ ≫ c.π.app j = (c.extend (Hom.right g₂)).π.app j
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
i : F.I₀
⊢ (eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv) ≫ E.f (s₀.symm i) = F.f i

Tactic:
obtain ⟨i, rfl⟩ := s₀.surjective i
    simp only [← cancel_epi (h₀ i).hom, w₀, Category.assoc, Equiv.symm_apply_apply,
      eqToHom_iso_hom_naturality_assoc, Iso.hom_inv_id_assoc]
    rw [← CategoryTheory.eqToHom_naturality _ (by simp)]
    simp

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

Goal state before:
pp: case h
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
S T✝ : C
E : J.ZeroHypercover S
inst✝² : E.Small
T : C
f : T ⟶ S
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : ∀ (i : E.I₀), HasPullback f (E.f i)
x✝ : ∀ (i : E.restrictIndexOfSmall.I₀), HasPullback f (E.restrictIndexOfSmall.f i)
⊢ ((pullback₁ f E).restrictIndex (Small.restrictFun E)).presieve₀ ∈ J.coverings T

Tactic:
exact ((restrictIndexOfSmall.{w'} E).pullback₁ f).mem₀

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) = E.presieve₀

Tactic:
exact Presieve.ofArrows_comp_eq_of_surjective _ (fun i ↦ ⟨e.hom.s₀ i, by simp⟩)

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
hP : Presheaf.IsSheaf J P
X : C
⊢ ∀ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))

Tactic:
E

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
hP : Presheaf.IsSheaf J P
X : C
E : J.OneHypercover X
⊢ H E → Nonempty (IsLimit (E.multifork P))
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ (ConcreteCategory.hom
          (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op ≫ P.map (pullbackComparison F (f i) (f j)).op))
        (x i) =
      (ConcreteCategory.hom
          (P.map ((pullback.snd (F.map (f i)) (F.map (f j))).op ≫ (pullbackComparison F (f i) (f j)).op)))
        (x j) ↔
    (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
      (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)

Tactic:
Functor.map_comp

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ (ConcreteCategory.hom
          (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op ≫ P.map (pullbackComparison F (f i) (f j)).op))
        (x i) =
      (ConcreteCategory.hom
          (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op ≫ P.map (pullbackComparison F (f i) (f j)).op))
        (x j) ↔
    (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
      (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)
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
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
X : C
⊢ ∀ (E : J.OneHypercover X), Nonempty (IsLimit (E.multifork (F.op ⋙ P)))

Tactic:
E

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
X : C
E : J.OneHypercover X
⊢ Nonempty (IsLimit (E.multifork (F.op ⋙ P)))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
α' : ℱ ⋙ yoneda ⟶ ℱ'.obj ⋙ yoneda := sheafYonedaHom α
X Y : Dᵒᵖ
f : X ⟶ Y
⊢ yoneda.map (ℱ.map f ≫ yoneda.preimage (α'.app Y)) = yoneda.map (yoneda.preimage (α'.app X) ≫ ℱ'.obj.map f)

Tactic:
by simpa using! α'.naturality f

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
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ᵒᵖ
⊢ IsIso ((sheafHom i.hom).app X)

Tactic:
rw [← isIso_iff_of_reflects_iso _ yoneda]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
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ᵒᵖ
⊢ IsIso (yoneda.map ((sheafHom i.hom).app X))
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₁), ⋯⟩
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)

Tactic:
refine Eq.trans ?_ (Y.2.amalgamate_map _ _ _ I').symm

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 = f ≫ Y.obj.map (l I'.Y W₁ U I'.f g₁ ⋯).op
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝ E : PreOneHypercover S
F : PreOneHypercover S
G : PreOneHypercover S
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq : d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op = d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op
⊢ d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op ≫ P.map (f.h₁ k.snd).op =
    d.ι (f.s₀ k.fst.2) ≫ P.map ((F.p₂ (f.s₁ k.snd)).op ≫ (f.h₁ k.snd).op)

Tactic:
Functor.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝ E : PreOneHypercover S
F : PreOneHypercover S
G : PreOneHypercover S
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq : d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op = d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op
⊢ d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op ≫ P.map (f.h₁ k.snd).op =
    d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op ≫ P.map (f.h₁ k.snd).op
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ ∀ {a b : Sieve Y},
    { toFun := functorPushforward (Over.forget X), invFun := functorPullback (Over.forget X), left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := functorPushforward (Over.forget X), invFun := functorPullback (Over.forget X), left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by
    rw [Equiv.coe_fn_mk]
    exact ⟨fun h ↦ by simpa using functorPullback_monotone _ _ h,
      fun h ↦ functorPushforward_monotone _ _ h⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ (Sieve.overEquiv ((Over.map f).obj U)).symm S ∈ (J.over Y) ((Over.map f).obj U)

Tactic:
apply overEquiv_symm_mem_over

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ S ∈ J ((Over.map f).obj U).left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
hS : (Sieve.overEquiv ((Over.map f).obj U)) S ∈ J ((Over.map f).obj U).left
⊢ (Sieve.overEquiv U) (Sieve.functorPullback (Over.map f) S) ∈ J U.left

Tactic:
rwa [Sieve.overEquiv_functorPullback_map]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
⊢ ∀ (E : (J.over X).OneHypercover Y), E.IsPreservedBy (Over.forget X) J

Tactic:
E

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ E.IsPreservedBy (Over.forget X) J
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: 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.IsPreservedBy (Over.post F) (K.over (F.obj X))

Tactic:
E

Goal state after:
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.IsPreservedBy (Over.post F) (K.over (F.obj X))
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd = 0
⊢ biprod.snd ≫ biprod.inr = 0

Tactic:
h,

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd = 0
⊢ 0 ≫ biprod.inr = 0
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
this : Simple (Y ⊞ Z)
⊢ IsZero Z

Tactic:
← Simple.mono_isIso_iff_nonzero biprod.inl

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 : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
G : Sheaf C X
f : F ⟶ G
s : ToType (F.obj.obj (op (iSup U)))
t : ToType (G.obj.obj (op V))
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsGluing F.obj U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι), (ConcreteCategory.hom (f.hom.app (op (U i)))) (sf i) = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t
x✝ : ι
⊢ (ConcreteCategory.hom (f.hom.app (op (U x✝)))) ((ConcreteCategory.hom (F.obj.map (leSupr U x✝).op)) s) =
    (ConcreteCategory.hom (G.obj.map (leSupr U x✝).op)) ((ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t)

Tactic:
h,

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
G : Sheaf C X
f : F ⟶ G
s : ToType (F.obj.obj (op (iSup U)))
t : ToType (G.obj.obj (op V))
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsGluing F.obj U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι), (ConcreteCategory.hom (f.hom.app (op (U i)))) (sf i) = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t
x✝ : ι
⊢ (ConcreteCategory.hom (f.hom.app (op (U x✝)))) (sf x✝) =
    (ConcreteCategory.hom (G.obj.map (leSupr U x✝).op)) ((ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case mpr
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₁ → M₂
⊢ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe → f ∈ Set.range DFunLike.coe

Tactic:
· rintro ⟨hfc, f, rfl⟩
    exact ⟨⟨f, hfc⟩, rfl⟩

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

Goal state before:
pp: R₁ : Type u_1
inst✝⁴ : Semiring R₁
M₁ : Type u_4
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
inst✝ : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : f 1 = g 1
x : R₁
⊢ x • f 1 = g (x • 1)

Tactic:
h,

Goal state after:
R₁ : Type u_1
inst✝⁴ : Semiring R₁
M₁ : Type u_4
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
inst✝ : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : f 1 = g 1
x : R₁
⊢ x • g 1 = g (x • 1)
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
s : S
hs : s ∈ Set.range ⇑(algebraMap R S)
⊢ (includeLeftSubRight R S) s = 0

Tactic:
obtain ⟨_, hr⟩ := Set.mem_range.mp hs
  simp [← hr, algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (eqToHom ⋯ ≫ Hom.snd b) = ?m.568

Tactic:
subst h₂; simp only [eqToHom_refl, Category.id_comp, f]

Goal state after:
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
h₁ : J.fst b = J.snd b
f : (left (J.snd b) ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ False = ?m.571 (J.snd b) ⋯ h₁
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
D : J ⥤ C
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
f : c.pt ⟶ X
j : Jᵒᵖ
p : (D.op ⋙ yoneda.obj X).obj j
hp : (ConcreteCategory.hom (((yoneda.obj X).mapCocone c.op).ι.app j)) p = f
⊢ ∃ j p, c.π.app j ≫ p = f

Tactic:
exact ⟨j.unop, p, hp⟩

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
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ piRightHom R S N M ∘ₗ piRightInv R S N M = LinearMap.id

Tactic:
ext i x m j

Goal state after:
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
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : N
m : M i
j : ι
⊢ ((AlgebraTensorModule.curry ((piRightHom R S N M ∘ₗ piRightInv R S N M) ∘ₗ single S (fun i ↦ N ⊗[R] M i) i)) x) m j =
    ((AlgebraTensorModule.curry (LinearMap.id ∘ₗ single S (fun i ↦ N ⊗[R] M i) i)) x) m j