mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ restrictFunctor f ⊣ pushforward f

Tactic:
refine pushforwardPushforwardAdj (by exact f.isOpenEmbedding.isOpenMap.adjunction) _ _ ?_ ?_
  · ext U x; exact congr($((f.app_appIso_inv _).symm).hom x)
  · ext U x
    have : (f.appIso U.unop).inv ≫ f.app _ ≫
      X.presheaf.map (eqToHom (f.preimage_image_eq U.unop).symm).op = 𝟙 _ := by
      rw [Scheme.Hom.appIso_inv_app_assoc, ← Functor.map_comp, ← X.presheaf.map_id]; rfl
    exact congr($this x)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_1.refine_1
X Y Z T : Scheme
M✝ N K : X.Modules
φ✝ : M✝ ⟶ N
U✝ V : X.Opens
R S : CommRingCat
φ : R ⟶ S
M : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))
U : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ
⊢ CommRingCat.Hom.hom (φ ≫ (ΓSpecIso S).inv) =
    (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ))).comp (CommRingCat.Hom.hom (ΓSpecIso R).inv)

Tactic:
Scheme.ΓSpecIso_inv_naturality,

Goal state after:
case refine_1.refine_1
X Y Z T : Scheme
M✝ N K : X.Modules
φ✝ : M✝ ⟶ N
U✝ V : X.Opens
R S : CommRingCat
φ : R ⟶ S
M : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))
U : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ
⊢ CommRingCat.Hom.hom ((ΓSpecIso R).inv ≫ Hom.appTop (Spec.map φ)) =
    (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ))).comp (CommRingCat.Hom.hom (ΓSpecIso R).inv)
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t : ↑((Spec R).ringCatSheaf.obj.obj U)
m : ↑(M.val.1 U)
x : ↥(Spec R)
hxU : x ∈ unop U
r : ↑R
hxr : x ∈ ↑(basicOpen r)
hrU : basicOpen r ≤ unop U
this :
  ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (unop U)))),
    (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) x) =
      (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) x)
⊢ (ConcreteCategory.hom (f.hom.app (op (basicOpen r))))
      ((ConcreteCategory.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op)) t •
        (ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) m) =
    (ConcreteCategory.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op)) t •
      (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) m)

Tactic:
generalize (Spec R).ringCatSheaf.obj.map (homOfLE hrU).op t = t

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M N : (Spec R).Modules
f : modulesSpecToSheaf.obj M ⟶ modulesSpecToSheaf.obj N
U : (Opens ↥(Spec R))ᵒᵖ
t✝ : ↑((Spec R).ringCatSheaf.obj.obj U)
m : ↑(M.val.1 U)
x : ↥(Spec R)
hxU : x ∈ unop U
r : ↑R
hxr : x ∈ ↑(basicOpen r)
hrU : basicOpen r ≤ unop U
this :
  ∀ (x : ↑((modulesSpecToSheaf.obj M).obj.obj (op (unop U)))),
    (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) x) =
      (ConcreteCategory.hom (N.val.map (homOfLE hrU).op)) ((ConcreteCategory.hom (f.hom.app (op (unop U)))) x)
t : ↑((Spec R).ringCatSheaf.obj.obj (op (basicOpen r)))
⊢ (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) (t • (ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) m) =
    t • (ConcreteCategory.hom (f.hom.app (op (basicOpen r)))) ((ConcreteCategory.hom (M.val.map (homOfLE hrU).op)) m)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case hx.inr
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
hd : d > 0
⊢ ∀ (i : ι'), (fun x ↦ ai x % d) i ≤ d

Tactic:
exact fun i ↦ (Nat.mod_lt _ hd).le

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case hy.refine_2
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ ∀ (i : ι'), Pi.single j d i ≤ d

pp: case hy.refine_3
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ Away.mk 𝒜 hf (dv j) (∏ i, v i ^ Pi.single j d i) ⋯ = isLocalizationElem hf ⋯

Tactic:
· aesop (add simp Pi.single_apply)

Goal state after:
case hy.refine_3
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
j : ι'
⊢ Away.mk 𝒜 hf (dv j) (∏ i, v i ^ Pi.single j d i) ⋯ = isLocalizationElem hf ⋯
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case hy
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
⊢ ∀ c ∈ Finset.univ,
    isLocalizationElem hf ⋯ ^ (ai c / d) ∈
      Algebra.adjoin ↥(𝒜 0)
        {x |
          ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
rintro j -
    apply pow_mem
    apply Algebra.subset_adjoin
    refine ⟨dv j, Pi.single j d, ?_, ?_, ?_⟩
    · simp [Pi.single_apply, mul_comm]
    · aesop (add simp Pi.single_apply)
    ext
    simp [Pi.single_apply]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
⊢ Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
    ⊤

Tactic:
let s := Finset.univ.filter (0 < dv ·)

Goal state after:
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
s : Finset ι' := {x | 0 < dv x}
⊢ Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
    ⊤
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
n : ι → ℕ
t' : (i : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
⊢ ∃ N t, ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)

Tactic:
have hN (i : ι) : ⨆ i, n i = ((⨆ i, n i) - n i) + n i := by grind

Goal state after:
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
n : ι → ℕ
t' : (i : ι) → ↑Γ(M, basicOpen (g i))
ht' : ∀ (i : ι), f ^ n i • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t' i)
this : ∀ (i : ι), n i ≤ ⨆ i, n i
hN : ∀ (i : ι), ⨆ i, n i = (⨆ i, n i) - n i + n i
⊢ ∃ N t, ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆
    Subtype.val '' ↑(map (Subring.inclusion ⋯) (map (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring) M))

Tactic:
map_map

Goal state after:
K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ⇑A.subtype '' ↑I ⊆
    Subtype.val '' ↑(map ((Subring.inclusion ⋯).comp (algebraMap ↥A ↥(LocalSubring.ofPrime A M).toSubring)) M)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
⊢ ∃ V, R ≤ V.toLocalSubring ∧ x ∉ V

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `B)
   []
   []
   ":="
   (choice
    (Algebra.subalgebra_adjoin `R.toSubring "[" [(«term_⁻¹» `x "⁻¹")] [] "]")
    («term__[_]» `R.toSubring "[" («term_⁻¹» `x "⁻¹") "]")))))

Goal state after:
case inr
K : Type u_3
inst✝¹ : Field K
x : K
R : LocalSubring K
hxR : x ∉ R.toSubring
inst✝ : IsIntegrallyClosedIn (↥R.toSubring) K
hx0 : x ≠ 0
this : Invertible x := invertibleOfNonzero hx0
B : Subalgebra (↥R.toSubring) K := (↥R.toSubring)[x⁻¹]
⊢ ∃ V, R ≤ V.toLocalSubring ∧ x ∉ V
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (pullback.diagonal f)
⊢ IsClosedImmersion (pullback.diagonal f)

Tactic:
have := UniversallyClosed.of_valuativeCriterion (pullback.diagonal f) h
      exact .of_isPreimmersion _ (pullback.diagonal f).isClosedMap.isClosed_range

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Sheaf

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf J A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (match (X, i) with
    | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
    (sheafToPresheaf J A).obj F
⊢ a ≫ (sheafToPresheaf J A).map f = a ≫ (sheafToPresheaf J A).map g

Tactic:
apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : HasCoproducts A
inst✝ : HasWeakSheafify J A
ι : Type w
S : ι → A
hS : (ObjectProperty.ofObj S).IsSeparating
F G : Sheaf J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf J A),
    ObjectProperty.ofObj
        (fun x ↦
          match x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (match (X, i) with
    | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
    (sheafToPresheaf J A).obj F
⊢ ((sheafificationAdjunction J A).homEquiv
          (match (X, i) with
          | (X, i) => Presheaf.freeYoneda X (S i))
          G).symm
      (a ≫ (sheafToPresheaf J A).map f) =
    ((sheafificationAdjunction J A).homEquiv
          (match (X, i) with
          | (X, i) => Presheaf.freeYoneda X (S i))
          G).symm
      (a ≫ (sheafToPresheaf J A).map g)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).toPreOneHypercover.f i = F.map b ≫ a
⊢ (restriction data G₀ ((data X).f ((data X).multicospanShape.fst ⟨(i₁, i₂), j⟩) ≫ f) ≫
        ((data X).multicospanIndex G₀.obj).fst ⟨(i₁, i₂), j⟩) ≫
      G₀.obj.map { Y := W₀, f := b, hf := ⋯ }.f.op =
    (restriction data G₀ ((data X).f ((data X).multicospanShape.snd ⟨(i₁, i₂), j⟩) ≫ f) ≫
        ((data X).multicospanIndex G₀.obj).snd ⟨(i₁, i₂), j⟩) ≫
      G₀.obj.map { Y := W₀, f := b, hf := ⋯ }.f.op

Tactic:
dsimp at fac ⊢

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y✝ : C
f : X ⟶ Y✝
i₁ i₂ : (data X).I₀
j : (data X).I₁ (i₁, i₂).1 (i₁, i₂).2
a : F.obj ((data X).Y j) ⟶ Y✝
h₁ : a = F.map ((data X).p₁ j) ≫ (data X).f i₁ ≫ f
h₂ : a = F.map ((data X).p₂ j) ≫ (data X).f i₂ ≫ f
W₀ : C₀
b : W₀ ⟶ (data X).Y j
Y : C
i : (data Y✝).toPreOneHypercover.I₀
p : F.obj W₀ ⟶ (data Y✝).toPreOneHypercover.X i
fac : p ≫ (data Y✝).f i = F.map b ≫ a
⊢ (restriction data G₀ ((data X).f i₁ ≫ f) ≫ G₀.obj.map ((data X).p₁ j).op) ≫ G₀.obj.map b.op =
    (restriction data G₀ ((data X).f i₂ ≫ f) ≫ G₀.obj.map ((data X).p₂ j).op) ≫ G₀.obj.map b.op
Module: Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor F R

Tactic:
← isSheafFor_comp_uliftFunctor_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : C
R : Presieve X
hR : ∀ (Y : C), IsSheafFor (yoneda.obj Y) R
F : Cᵒᵖ ⥤ Type w
inst✝ : F.IsRepresentable
⊢ IsSheafFor (F ⋙ uliftFunctor.{?u.29, w}) R
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
G₀✝ : Sheaf J₀ A
⊢ (F.map c ≫ Sieve.ofArrows.h hd) ≫ (data X).f (Sieve.ofArrows.i hd) = F.map (c ≫ d) ≫ f

Tactic:
by simp; grind

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

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
G₀✝ : Sheaf J₀ A
⊢ Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) = F.map (c ≫ d) ≫ f ≫ g

Tactic:
by simp; grind

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : 0 ≫ r' = 0
hx₂' : π ≫ x₄ = 0 ≫ r
⊢ x₄ = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
hx₄ : 0 ≫ r' = 0
hx₂' : π ≫ x₄ = 0
⊢ x₄ = 0
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ 0 ≫ c₃.ι.app j = 0

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ c₂.ι.app j ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom ≫ colimMap S.g =
    c₂.ι.app j ≫ g ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom

Tactic:
rw [IsColimit.comp_coconePointUniqueUpToIso_hom_assoc,
      colimit.cocone_ι, ι_colimMap, reassoc_of% (hg j),
      IsColimit.comp_coconePointUniqueUpToIso_hom, colimit.cocone_ι]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: case inr
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
hj : ¬IsMax (Fin.last n)
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))

Tactic:
isMax_iff_eq_top

Goal state after:
case inr
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
n : ℕ
F : ComposableArrows C n
hF : ∀ (i : Fin n), W (F.map (homOfLE ⋯))
hj : ¬Fin.last n = ⊤
⊢ W ((CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows F).F.map (homOfLE ⋯))