mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ (mateEquiv adj₁ adj₂).symm β = 𝟙 (g ≫ l₂) ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ h)

Tactic:
mateEquiv_symm_apply,

Goal state after:
B : Type u
inst✝ : Bicategory B
c d e f : B
g : c ⟶ e
h : d ⟶ f
l₁ : c ⟶ d
r₁ : d ⟶ c
l₂ : e ⟶ f
r₂ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ adj₂.homEquiv₂.symm (adj₁.homEquiv₁.symm β ≫ (α_ l₁ h r₂).inv) =
    𝟙 (g ≫ l₂) ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ h)
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
i : X.affineCover.I₀
⊢ Smooth (X.affineCover.f i ≫ f)

Tactic:
have _ (y) : Smooth (pullback.snd f ((Spec R).fromSpecResidueField y)) :=
      inferInstanceAs <| Smooth (f.fiberToSpecResidueField y)

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X : Scheme} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ S, X = Spec S) → Smooth f
h : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x✝ : ∀ (y : ↥(Spec R)), Smooth (pullback.snd f ((Spec R).fromSpecResidueField y))
⊢ Smooth (X.affineCover.f i ≫ f)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : KrullDimLE 1 R
inst✝ : Nontrivial R
y : ↥(nonZeroDivisors R)
⊢ IsUnit ((ordMonoidWithZeroHom R) ↑y)

Tactic:
by
  simp [ordMonoidWithZeroHom_eq_zero_iff, ord_ne_top]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
β : l₁ ⟶ l₂
βα : β ≫ α = 𝟙 l₁
⊢ (conjugateEquiv adj₁ adj₁) (β ≫ α) = 𝟙 r₁

Tactic:
βα,

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
β : l₁ ⟶ l₂
βα : β ≫ α = 𝟙 l₁
⊢ (conjugateEquiv adj₁ adj₁) (𝟙 l₁) = 𝟙 r₁
Module: Mathlib.RingTheory.GradedAlgebra.RingHom

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : DecidableEq ι
inst✝⁷ : AddMonoid ι
inst✝⁶ : AddSubmonoidClass σ A
inst✝⁵ : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝⁴ : GradedRing 𝒜
inst✝³ : GradedRing ℬ
F : Type u_10
inst✝² : FunLike F A B
inst✝¹ : GradedFunLike F 𝒜 ℬ
inst✝ : RingHomClass F A B
f : F
x : A
⊢ (decompose ℬ) (f x) = (map (↑f).gradedAddHom) ((decompose 𝒜) x)

Tactic:
← DirectSum.sum_support_decompose 𝒜 x,

Goal state after:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : DecidableEq ι
inst✝⁷ : AddMonoid ι
inst✝⁶ : AddSubmonoidClass σ A
inst✝⁵ : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝⁴ : GradedRing 𝒜
inst✝³ : GradedRing ℬ
F : Type u_10
inst✝² : FunLike F A B
inst✝¹ : GradedFunLike F 𝒜 ℬ
inst✝ : RingHomClass F A B
f : F
x : A
⊢ (decompose ℬ) (f (∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i))) =
    (map (↑f).gradedAddHom) ((decompose 𝒜) (∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i)))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
⊢ Continuous (ToSpec.toFun f)

Tactic:
PrimeSpectrum.isTopologicalBasis_basic_opens.continuous_iff

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
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
⊢ U.ι ''ᵁ X.homOfLE ⋯ ''ᵁ W = V.ι ''ᵁ W

Tactic:
simp [← Scheme.Hom.comp_image]

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝¹³ : CommRing A
inst✝¹² : SetLike σ A
inst✝¹¹ : AddSubgroupClass σ A
inst✝¹⁰ : AddCommMonoid ι
inst✝⁹ : DecidableEq ι
𝒜 : ι → σ
inst✝⁸ : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
f : A
⊢ Submonoid.powers f ≤ Submonoid.comap g (Submonoid.powers (g f))

Tactic:
by rintro _ ⟨n, rfl⟩; exact ⟨n, by simp⟩

Goal state after:
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
X : Scheme
U V : X.Opens
f : V ⟶ U
⊢ overMap X.ringCatSheaf f ⋙ (overEquiv V).functor ≅ (overEquiv U).functor ⋙ restrictFunctor (X.homOfLE ⋯)

Tactic:
haveI : (Hom.opensFunctor (X.homOfLE <| leOfHom f)).IsContinuous
      (Opens.grothendieckTopology V.toScheme) (Opens.grothendieckTopology U.carrier) :=
    inferInstanceAs <|
      (Hom.opensFunctor (X.homOfLE <| leOfHom f)).IsContinuous _
      (Opens.grothendieckTopology U.toScheme)
  haveI := U.instIsDenseSubsiteSubtypeMemOverGrothendieckTopologyOverInverseOverEquivalence
  haveI : (Hom.opensFunctor (X.homOfLE <| leOfHom f)).IsContinuous
      (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology U.toScheme) :=
    inferInstanceAs <| (X.homOfLE <| leOfHom f).opensFunctor.IsContinuous
      (Opens.grothendieckTopology V.toScheme) (Opens.grothendieckTopology U.toScheme)
  haveI : ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous
      (Opens.grothendieckTopology ↥V) ((Opens.grothendieckTopology X).over U) :=
    Functor.isContinuous_comp _ _ _ (.over (Opens.grothendieckTopology _) _) _
  haveI : (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology U)
      ((Opens.grothendieckTopology X).over U) :=
    inferInstanceAs <| U.overEquivalence.inverse.IsContinuous (Opens.grothendieckTopology U.carrier)
      ((Opens.grothendieckTopology X).over U)
  haveI : ((X.homOfLE (leOfHom f)).opensFunctor ⋙
        (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
      ((Opens.grothendieckTopology ↥X).over U) :=
    Functor.isContinuous_comp _ _ _ (Opens.grothendieckTopology _) _
  refine (SheafOfModules.pushforwardComp _ _) ≪≫ ?_ ≪≫ (SheafOfModules.pushforwardComp _ _).symm
  refine SheafOfModules.pushforwardCongr₂ _ ?_ ?_
  · refine NatIso.ofComponents (fun W ↦ Over.isoMk (eqToIso ?_) ?_) ?_
    · suffices U.ι ''ᵁ ((X.homOfLE (leOfHom f)) ''ᵁ W) = V.ι ''ᵁ W by simpa
      simp [← Scheme.Hom.comp_image]
    · cat_disch
    · cat_disch
  · ext W x
    suffices X.presheaf.map _ x = ((X.homOfLE <| leOfHom f).appIso _).inv x by simpa
    rw [Scheme.Hom.appIso_homOfLE_inv]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)
⊢ ⨆ i, basicOpen 𝒜 (f i) = ⊤

Tactic:
refine top_le_iff.mp fun x hx ↦ TopologicalSpace.Opens.mem_iSup.mpr ?_
  by_contra! H
  simp only [mem_basicOpen, Decidable.not_not] at H
  refine x.not_irrelevant_le (hf.trans ?_)
  rwa [Ideal.span_le, Set.range_subset_iff]

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ val ((awayMap 𝒜 hg hx) (mk { deg := n, num := a, den := ⟨f ^ i, hi⟩, den_mem := ⋯ })) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
by
  rw [val_awayMap_eq_aux, awayMapAux_mk 𝒜 (hx := hx)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ Set.range ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯))) =
    ↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg))

Tactic:
let := (awayMap (f := f) 𝒜 g_deg rfl).toAlgebra

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := (awayMap 𝒜 g_deg ⋯).toAlgebra
⊢ Set.range ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯))) =
    ↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case refine_1
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)) (Set.range (v ∘ Subtype.val)) = ⊤

Tactic:
rw [← top_le_iff, ← hx, Algebra.adjoin_le_iff, Set.range_subset_iff]
    intro i
    rcases (dv i).eq_zero_or_pos with hi | hi
    · exact algebraMap_mem (R := 𝒜 0) _ ⟨v i, hi ▸ hxd i⟩
    exact Algebra.subset_adjoin ⟨⟨i, by simpa [s] using hi⟩, rfl⟩

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 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
⊢ ⊤.FG

Tactic:
simp_rw [Subalgebra.fg_def, ← top_le_iff,
    ← Away.adjoin_mk_prod_pow_eq_top hf (ι' := s) Subtype.val (by simpa) dx hxd]

Goal state after:
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
f : A
d : ℕ
hf : f ∈ 𝒜 d
s : Finset A
hs : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
hs' : ∀ i ∈ s, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n
dx : ↥s → ℕ
hdx : ∀ (x : ↥s), dx x ≠ 0
hxd : ∀ (x : ↥s), ↑x ∈ 𝒜 (dx x)
⊢ ∃ t,
    t.Finite ∧
      Algebra.adjoin ↥(𝒜 0)
          {x |
            ∃ a ai,
              ∃ (hai : ∑ i, ai i • dx i = a • d) (_ : ∀ (i : ↥s), ai i ≤ d), Away.mk 𝒜 hf a (∏ i, ↑i ^ ai i) ⋯ = x} ≤
        Algebra.adjoin (↥(𝒜 0)) t
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
⊢ ∃ B, A ≤ B.toSubring ∧ ⇑A.subtype '' ↑I ⊆ ↑B.nonunits

Tactic:
have ⟨M, hM, le⟩ := I.exists_le_maximal hI

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
⊢ ∃ B, A ≤ B.toSubring ∧ ⇑A.subtype '' ↑I ⊆ ↑B.nonunits
Module: Mathlib.CategoryTheory.Sites.Point.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
X : C
x : Φ.fiber.obj X
⊢ ∀ (p₁ p₂ : ToType (P.obj (op X))),
    (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
      (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂

Tactic:
p₁

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁶ : Category.{v', u'} A
inst✝⁵ : HasColimitsOfSize.{w, w, v', u'} A
FC : A → A → Type u_1
CC : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
P Q : Cᵒᵖ ⥤ A
inst✝² : PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (forget A)
inst✝¹ : LocallySmall.{w, v, u} C
f : P ⟶ Q
inst✝ : Presheaf.IsLocallyInjective J f
X : C
x : Φ.fiber.obj X
p₁ : ToType (P.obj (op X))
⊢ ∀ (p₂ : ToType (P.obj (op X))),
    (ConcreteCategory.hom (f.app (op X))) p₁ = (ConcreteCategory.hom (f.app (op X))) p₂ →
      (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₁ = (ConcreteCategory.hom (Φ.toPresheafFiber X x P)) p₂
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
⊢ SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf ≤ (tilde.functor R).essImage

Tactic:
intro M (h : M.IsQuasicoherent)

Goal state after:
case refine_2
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
h : SheafOfModules.IsQuasicoherent M
⊢ (tilde.functor R).essImage M
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case h.e_a.e_a
σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ ∑ i, d i * ((∏ i, d i) * ai i) + d i₀ * ((∏ i, d i) * a * (d j - 1)) = a * d i₀ * (d j * ∏ i, d i)

Tactic:
simp only [mul_comm _ (∏ i, d i), mul_assoc, mul_left_comm _ (∏ i, d i),
              mul_comm (d _) (ai _), ← Finset.mul_sum, hai]
            cases h : d j
            · cases (hdi j).ne' h
            · simp; ring

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 : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = F.map b₂ ≫ (data X).f h₂.i₀

Tactic:
w₂,

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 : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S : Scheme
⊢ qcPrecoverage.IsStableUnderComposition

Tactic:
refine .of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_

Goal state after:
S : Scheme
X : Scheme
E : PreZeroHypercover X
F : (i : E.I₀) → PreZeroHypercover (E.X i)
hE : qcCoverFamily.property E
hF : ∀ (i : E.I₀), qcCoverFamily.property (F i)
⊢ qcCoverFamily.property (E.bind F)
Module: Mathlib.AlgebraicGeometry.Sites.QuasiCompact

Goal state before:
pp: S : Scheme
⊢ qcPrecoverage.IsStableUnderSup

Tactic:
refine .of_preZeroHypercoverFamily fun {X} E F hE hF ↦ ?_

Goal state after:
S : Scheme
X : Scheme
E F : PreZeroHypercover X
hE : qcCoverFamily.property E
hF : qcCoverFamily.property F
⊢ qcCoverFamily.property (E.sum F)
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
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (F.map x₁) =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj.map x₁.op

Tactic:
IsDenseSubsite.mapPreimage_map

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
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
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj.map x₁.op =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ G₀.obj.map x₁.op
Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : MorphismProperty C
S : C
inst✝ : P.IsStableUnderComposition
K : Precoverage C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover ((Over.forget P ⊤ S).obj X)
𝒱 : PreZeroHypercover X :=
  { I₀ := 𝒰.I₀, X := fun i ↦ Over.mk ⊤ (𝒰.X i).hom ⋯, f := fun i ↦ Over.homMk (Over.Hom.left (𝒰.f i)) ⋯ trivial }
⊢ ∃ T, Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
use 𝒱.presieve₀
    rw [Presieve.map_ofArrows]
    rfl

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

Goal state before:
pp: S : Scheme
X : S.ProEt
inst✝ : IsEmpty ↥X.left
⊢ ⊥ ∈ (precoverage S).coverings X

Tactic:
simp [precoverage, proetalePrecoverage, bot_mem_propQCPrecoverage]

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₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : z ≫ cokernel.map t b l r ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
w✝¹ : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.Exact
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
x₃ : A₂ ⟶ { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.X₁
hx₃ : π₂ ≫ x₂ ≫ r = x₃ ≫ { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.f
⊢ z = 0

Tactic:
obtain ⟨x₁, hx₁, rfl⟩ := sq.exists_lift (π₂ ≫ x₂) x₃ (by simpa)

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₄
sq : IsPullback t l r b
A₀ : C
z : A₀ ⟶ cokernel t
hz : z ≫ cokernel.map t b l r ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A₀
w✝¹ : Epi π₁
x₂ : A₁ ⟶ X₂
hx₂ : π₁ ≫ z = x₂ ≫ cokernel.π t
this : { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.Exact
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
x₁ : A₂ ⟶ X₁
hx₁ : x₁ ≫ t = π₂ ≫ x₂
hx₃ : π₂ ≫ x₂ ≫ r = (x₁ ≫ l) ≫ { X₁ := X₃, X₂ := X₄, X₃ := cokernel b, f := b, g := cokernel.π b, zero := ⋯ }.f
⊢ z = 0