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

Goal state before:
pp: case refine_1.refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : TopologicalSpace.Opens ↥↑V
⊢ (eqToIso ⋯).hom ≫ (((Opens.overEquivalence V).symm.functor ⋙ Over.map f).obj W).hom =
    ((Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).obj W).hom

Tactic:
cat_disch

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

Goal state before:
pp: case refine_1.refine_3
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
⊢ ∀ {X_1 Y : TopologicalSpace.Opens ↥↑V} (f_1 : X_1 ⟶ Y),
    (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).map f_1 ≫ (Over.isoMk (eqToIso ⋯) ⋯).hom =
      (Over.isoMk (eqToIso ⋯) ⋯).hom ≫ ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).map f_1

Tactic:
cat_disch

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 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
⊢ s * g ^ (n * d) ∈ 𝒜 ((n * (e + 1)) • (d + 1))

Tactic:
by
      convert! SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg) using 2; simp; ring

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

Goal state before:
pp: R : CommRingCat
M N : TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace
φ : M ≅ N
hM : IsLocalizing M
f : ↑R
⊢ IsLocalizedModule (Submonoid.powers f)
    (ConcreteCategory.hom (φ.inv.hom.app (op (basicOpen f))) ∘ₗ ModuleCat.Hom.hom (N.obj.map (basicOpen f).leTop.op))

Tactic:
← ModuleCat.hom_comp,

Goal state after:
R : CommRingCat
M N : TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace
φ : M ≅ N
hM : IsLocalizing M
f : ↑R
⊢ IsLocalizedModule (Submonoid.powers f)
    (ModuleCat.Hom.hom (N.obj.map (basicOpen f).leTop.op ≫ φ.inv.hom.app (op (basicOpen f))))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case 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)
s : Finset ι' := ⋯
this :
  Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai,
          ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} =
    ⊤
⊢ {x |
      ∃ a ai,
        ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
          Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} ⊆
    {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 _ ⟨a, ai, hai : ∑ x ∈ s.attach, _ = _, h, rfl⟩

Goal state after:
case 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)
s : Finset ι' := {x | 0 < dv x}
this :
  Algebra.adjoin ↥(𝒜 0)
      {x |
        ∃ a ai,
          ∃ (hai : ∑ i, ai i • (dv ∘ Subtype.val) i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d),
            Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ = x} =
    ⊤
a : ℕ
ai : ↥s → ℕ
hai : ∑ x ∈ s.attach, ai x • (dv ∘ Subtype.val) x = a • d
h : ∀ (i : ↥s), ai i ≤ d
⊢ Away.mk 𝒜 hf a (∏ i, (v ∘ Subtype.val) i ^ ai i) ⋯ ∈
    {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 N : TopCat.Sheaf (ModuleCat ↑R) ↑(Spec R).toPresheafedSpace
φ : M ⟶ N
h : IsIso (φ.hom.app (op ⊤))
hM : IsLocalizing M
hN : IsLocalizing N
⊢ IsIso φ

Tactic:
by
  refine TopCat.Sheaf.isIso_iff_isIso_basis (φ := φ) isBasis_basic_opens (fun f => ?_)
  refine ModuleCat.isIso_of_isLocalizedModule_comp (hM f) ?_
  rw [φ.hom.naturality]
  exact IsLocalizedModule.of_linearEquiv_right _ _ (asIso (φ.hom.app (op ⊤))).toLinearEquiv

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

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
f : ↑R
heq :
  tilde.toOpen M ⊤ ≫ (modulesSpecToSheaf.obj (tilde M)).obj.map (basicOpen f).leTop.op = tilde.toOpen M (basicOpen f)
⊢ IsLocalizedModule (Submonoid.powers f)
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj (tilde M)).obj.map (basicOpen f).leTop.op) ∘ₗ
      ConcreteCategory.hom (tilde.toOpen M ⊤))

Tactic:
← ModuleCat.hom_comp,

Goal state after:
R : CommRingCat
M : ModuleCat ↑R
f : ↑R
heq :
  tilde.toOpen M ⊤ ≫ (modulesSpecToSheaf.obj (tilde M)).obj.map (basicOpen f).leTop.op = tilde.toOpen M (basicOpen f)
⊢ IsLocalizedModule (Submonoid.powers f)
    (ModuleCat.Hom.hom (tilde.toOpen M ⊤ ≫ (modulesSpecToSheaf.obj (tilde M)).obj.map (basicOpen f).leTop.op))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
M : (Spec S).Modules
h : IsIso M.fromTildeΓ
⊢ IsIso ((Scheme.Modules.pushforward (Spec.map φ)).obj M).fromTildeΓ

Tactic:
simp_all only [isIso_fromTildeΓ_iff_isLocalizing]
  exact isLocalizing_pushforward_of_isLocalizing φ h

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯ ≫ f' = commSq.i₁ ≫ f'

Tactic:
hP.lift_snd

Goal state after:
case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ = commSq.i₁ ≫ f'
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case right
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
hR : ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.I₀) → (𝒰.X i).Over S := ⋯
this : Cover.Over S 𝒰 := ⋯
⊢ 𝒰.toPresieveOver ≤ R.arrows

Tactic:
Cover.toPresieveOver_le_arrows_iff

Goal state after:
case right
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
hR : ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
𝒰 : Cover (precoverage P) X.left
hle : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
this✝ : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case h
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
hT : 𝒰.toPresieveOver ≤ R.arrows
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows

Tactic:
Cover.toPresieveOver_le_arrows_iff

Goal state after:
case h
P : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
X : Over S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
hT : Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
⊢ Presieve.ofArrows 𝒰.X 𝒰.f ≤ ((Sieve.overEquiv X) R).arrows
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
hPQ : P ≤ Q
X : Q.Over ⊤ S
R : Sieve X
this : (MorphismProperty.Over.forget Q ⊤ S).LocallyCoverDense (overGrothendieckTopology P S)
⊢ (∃ 𝒰 x, 𝒰.toPresieveOver ≤ (Sieve.functorPushforward (MorphismProperty.Over.forget Q ⊤ S) R).arrows) →
    ∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows

Tactic:
intro ⟨𝒰, h, le⟩
    have hj (j : 𝒰.I₀) : Q (𝒰.X j ↘ S) := by
      rw [← comp_over (𝒰.f j)]
      exact Q.comp_mem _ _ (hPQ _ <| 𝒰.map_prop _) X.prop
    refine ⟨𝒰.toPresieveOverProp hj, ?_, ?_⟩
    · use 𝒰, h, hj
    · rintro - - ⟨i⟩
      let fi : (𝒰.X i).asOverProp S (hj i) ⟶ X := (𝒰.f i).asOverProp S
      have : R.functorPushforward _ ((MorphismProperty.Over.forget Q ⊤ S).map fi) := le _ _ ⟨i⟩
      rwa [Sieve.functorPushforward_apply,
        Sieve.mem_functorPushforward_iff_of_full_of_faithful] at this

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
⊢ (∃ R_1 ∈ (smallPretopology P Q).coverings X, R_1 ≤ R.arrows) →
    ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x

Tactic:
rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩

Goal state after:
case refine_1
P Q : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : P.IsMultiplicative
inst✝³ : P.RespectsIso
inst✝² : Q.IsStableUnderComposition
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.HasOfPostcompProperty Q
X : Q.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
⊢ ∀ (x : ↥X.left), ∃ Y f y, R.arrows f ∧ P f.left ∧ f.left y = x
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
⊢ LocallyOfFiniteType (toSpecZero 𝒜)

Tactic:
obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜
  choose d hd hxd using hx'
  rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := @LocallyOfFiniteType) _
    (Proj.iSup_basicOpen_eq_top' 𝒜 (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx))]
  intro i
  rw [← MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType)
    (Proj.basicOpenIsoSpec 𝒜 (i : A) (hxd _ i.2) (hd _ i.2).bot_lt).inv, ← Category.assoc,
    ← Proj.awayι, Proj.awayι_toSpecZero, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]
  exact HomogeneousLocalization.Away.finiteType _ _ (hxd _ i.2)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
⊢ R ∈ (smallPretopology P P).toGrothendieck X →
    ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows

Tactic:
rintro ⟨T, ⟨𝒰, h, p, rfl⟩, hle⟩

Goal state after:
case mp
P : MorphismProperty Scheme
S : Scheme
inst✝³ : P.IsStableUnderBaseChange
inst✝² : P.IsMultiplicative
inst✝¹ : P.RespectsIso
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
R : Sieve X
𝒰 : Cover (precoverage P) X.left
h : Cover.Over S 𝒰
p : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)
hle : 𝒰.toPresieveOverProp p ≤ R.arrows
⊢ ∃ 𝒰 x, ∃ (h : ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)), 𝒰.toPresieveOverProp h ≤ R.arrows
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.left := Cover.changeProp U.left.affineCover ⋯
x✝² : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ U.hom }
x✝¹ : Cover.Over S 𝒰 := { over := inferInstance, isOver_map := ⋯ }
X : P.Over ⊤ S
f : X ⟶ U
x✝ : 𝒰.toPresieveOverProp ⋯ f
i : 𝒰.I₀
⊢ MorphismProperty.CostructuredArrow.homMk (𝟙 ((𝒰.X i).asOverProp S ⋯).left) True.intro ⋯ ≫
      MorphismProperty.Over.homMk (𝒰.f i) ⋯ trivial =
    Hom.asOverProp (𝒰.f i) S

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Affine

Goal state before:
pp: S : Scheme
P : MorphismProperty Scheme
inst✝³ : P.IsMultiplicative
inst✝² : IsZariskiLocalAtSource P
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
X : P.Over ⊤ S
𝒰 : X.left.AffineOpenCover := X.left.affineOpenCover
𝒱 : Cover (precoverage P) X.left := Cover.changeProp 𝒰.openCover ⋯
x✝³ : (i : 𝒱.I₀) → (𝒱.X i).Over S := fun i ↦ { hom := 𝒰.f i ≫ X.hom }
this : Cover.Over S 𝒱 := { over := inferInstance, isOver_map := ⋯ }
x✝² : P.Over ⊤ S
x✝¹ : x✝² ⟶ X
x✝ : 𝒱.toPresieveOverProp ⋯ x✝¹
i : 𝒱.I₀
⊢ Hom.asOverProp (𝒱.f i) S = 𝟙 ((𝒱.X i).asOverProp S ⋯) ≫ MorphismProperty.CostructuredArrow.homMk (𝒰.f i) ⋯ ⋯

Tactic:
cat_disch

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
⊢ Aux M (basicOpen g)

Tactic:
let iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
    M.restrictAppIso _ _ ≪≫ M.presheaf.mapIso (eqToIso <| by simp [ψ, a]).op

Goal state after:
R : CommRingCat
M : (Spec R).Modules
g : ↑R
a : R ⟶ CommRingCat.of (Localization.Away g) := CommRingCat.ofHom (algebraMap (↑R) (Localization.Away g))
ψ : Spec (CommRingCat.of (Localization.Away g)) ⟶ Spec (CommRingCat.of ↑R) := Spec.map a
M' : (Spec (CommRingCat.of (Localization.Away g))).Modules := M.restrict ψ
h : Aux M' ⊤
heq : ∀ (f : ↑R), basicOpen f ≤ basicOpen g → basicOpen f = ψ ''ᵁ basicOpen ((ConcreteCategory.hom a) f)
iso : Γ(M.restrict ψ, ⊤) ≅ Γ(M, basicOpen g) :=
  Scheme.Modules.restrictAppIso ψ M ⊤ ≪≫ Functor.mapIso M.presheaf (eqToIso ⋯).op
⊢ Aux M (basicOpen g)
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
i : ↥W.left → ι
z : (w : ↥W.left) → ↥(Z (i w)).left
hz : ∀ (w : ↥W.left), (f (i w)).left (z w) = w
V : Cover (precoverage @Etale) W.left :=
  Cover.mkOfCovers (↥W.left) (fun w ↦ (Z (i w)).left) (fun w ↦ (f (i w)).left) ⋯ ⋯
w : V.I₀
⊢ Hom.IsOver (V.f w) X

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.Etale

Goal state before:
pp: X : Scheme
W : X.Etale
ι : Type u_1
Z : ι → X.Etale
f : (i : ι) → Z i ⟶ W
hf : ⋃ i, Set.range ⇑(f i).left = Set.univ
i : ↥W.left → ι
z : (w : ↥W.left) → ↥(Z (i w)).left
hz : ∀ (w : ↥W.left), (f (i w)).left (z w) = w
V : Cover (precoverage @Etale) W.left :=
  Cover.mkOfCovers (↥W.left) (fun w ↦ (Z (i w)).left) (fun w ↦ (f (i w)).left) ⋯ ⋯
this✝ : Cover.Over X V := { over := fun w ↦ { hom := (Z (i w)).hom }, isOver_map := ⋯ }
this : ∀ (w : ↥W.left), Etale (V.X w ↘ X)
Y : MorphismProperty.Over @Etale ⊤ X
w : V.I₀
⊢ 𝟙 ((V.X w).asOverProp X ⋯) ≫ f (i w) = Hom.asOverProp (V.f w) X

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
⊢ (fun K ↦ K.preZeroHypercoverFamily) ((fun P ↦ P.precoverage) P) = P

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
𝒰 : Cover (propQCPrecoverage P) S
⊢ ∀ (i : (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).I₀),
    𝟙 ((QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).X i) ≫
        (𝒰.restrictIndex (Sum.elim 𝒰.forgetQc.idx (QuasiCompactCover.uliftHom 𝒰.forgetQc.toPreZeroHypercover).s₀)).f
          (Sum.inr i) =
      (QuasiCompactCover.ulift 𝒰.toPreZeroHypercover).f i

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
hF : Presieve.IsSheaf (propQCTopology P) F
R S : CommRingCat
f : R ⟶ S
hf : P (Spec.map f)
hs : Surjective (Spec.map f)
⊢ Sieve.generate (Hom.cover (Spec.map f) hf).presieve₀ ∈ (propQCTopology P) (Spec R)

Tactic:
exact Cover.mem_propQCTopology _

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

Goal state before:
pp: case e_a
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
T : C
x₄ : T ⟶ X₄
this : Epi ⋯.shortComplex.g
T' : C
π : T' ⟶ T
w✝ : Epi π
u : T' ⟶ ⋯.shortComplex.X₂
hu : π ≫ x₄ = u ≫ ⋯.shortComplex.g
⊢ ⋯.shortComplex.g = biprod.fst ≫ r + biprod.snd ≫ b

Tactic:
cat_disch

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'
x₂' : T₁ ⟶ X₂
hx₄ : x₂' ≫ r' = 0
hx₂' : π ≫ x₄ = x₂' ≫ r
⊢ x₄ = 0

Tactic:
obtain rfl := zero_of_comp_mono _ hx₄

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 ≫ r
⊢ 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
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
f : (Functor.const (Under j₀)).obj (X.obj j₀) ⟶ Under.forget j₀ ⋙ X := { app := fun j ↦ X.map j.hom, naturality := ⋯ }
this : Mono f
⊢ ∀ (j : Under j₀),
    (constCocone (Under j₀) (X.obj j₀)).ι.app j ≫ c.ι.app j₀ = f.app j ≫ (Cocone.whisker (Under.forget j₀) c).ι.app j

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W : MorphismProperty C
inst✝¹ : W.IsStableUnderTransfiniteComposition
inst✝ : UnivLE.{w, w'}
J : Type w
x✝³ : LinearOrder J
x✝² : SuccOrder J
x✝¹ : OrderBot J
x✝ : WellFoundedLT J
⊢ W.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
rw [isStableUnderTransfiniteCompositionOfShape_iff_of_orderIso W
      (orderIsoShrink.{w'} J)]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
⊢ ∀ {X_1 Y : ↑(Set.Iic j)} (f : X_1 ⟶ Y),
    (restrictionLE (extendToSucc hj F τ) ⋯).map f ≫ (extendToSuccObjIso hj F τ ↑Y ⋯).hom =
      (extendToSuccObjIso hj F τ ↑X_1 ⋯).hom ≫ F.map f

Tactic:
rintro ⟨i₁, h₁⟩ ⟨i₂, h₂⟩ f

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ : J
h₁ : i₁ ∈ Set.Iic j
i₂ : J
h₂ : i₂ ∈ Set.Iic j
f : ⟨i₁, h₁⟩ ⟶ ⟨i₂, h₂⟩
⊢ (restrictionLE (extendToSucc hj F τ) ⋯).map f ≫ (extendToSuccObjIso hj F τ ↑⟨i₂, h₂⟩ ⋯).hom =
    (extendToSuccObjIso hj F τ ↑⟨i₁, h₁⟩ ⋯).hom ≫ F.map f
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
⊢ (ConcreteCategory.hom ((sqFunctor c p f g).map (homOfLE ⋯).op))
      (have this := ⋯;
      have this_1 := ⋯;
      { f' := ⋯.lift, w₁ := ⋯, w₂ := ⋯ }) =
    sq'

Tactic:
cat_disch

Goal state after: