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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ ((ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (λ_ r₃).hom =
    𝟙 r₁ ⊗≫
      ((α_ r₁ (𝟙 c) (𝟙 c)).inv ≫
          (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ 𝟙 c ≫
            (α_ (𝟙 d) r₂ (𝟙 c)).hom ≫
              𝟙 d ◁ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (α_ (𝟙 d) (𝟙 d) r₃).inv) ⊗≫
        𝟙 r₃

Tactic:
bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ 𝟙 r₁ ⊗≫
      (𝟙 (r₁ ≫ 𝟙 c ≫ 𝟙 c) ⊗≫
          r₁ ◁ (𝟙 c ≫ 𝟙 c) ◁ adj₃.unit ⊗≫
            r₁ ◁
                ((α_ (𝟙 c) (𝟙 c) l₃).hom ≫
                    𝟙 c ◁ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
                      (α_ (𝟙 c) l₂ (𝟙 d)).inv ≫ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ 𝟙 d ≫ (α_ l₁ (𝟙 d) (𝟙 d)).hom) ▷
                  r₃ ⊗≫
              adj₁.counit ▷ (𝟙 d ≫ 𝟙 d) ▷ r₃ ⊗≫ 𝟙 ((𝟙 d ≫ 𝟙 d) ≫ r₃)) ⊗≫
        𝟙 r₃ =
    (ρ_ r₁).inv ≫
      (𝟙 (r₁ ≫ 𝟙 c) ⊗≫
          r₁ ◁ 𝟙 c ◁ adj₃.unit ⊗≫
            r₁ ◁ ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ▷ r₃ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₃ ⊗≫ 𝟙 (𝟙 d ≫ r₃)) ≫
        (λ_ r₃).hom

Tactic:
bicategory

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₂) α ≫ (conjugateEquiv adj₂ adj₁) β = 𝟙 r₁

Tactic:
rw [conjugateEquiv_comp, βα, conjugateEquiv_id]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : f₁ ≫ l₂ ⟶ l₁ ≫ f₂
⊢ 𝟙 (u₂ ≫ r₁) ⊗≫
      u₂ ◁ r₁ ◁ adj₃.unit ⊗≫
        u₂ ◁ (𝟙 (r₁ ≫ f₁) ⊗≫ r₁ ◁ f₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ f₂ ▷ r₂ ⊗≫ 𝟙 (f₂ ≫ r₂)) ▷ u₁ ⊗≫
          adj₄.counit ▷ r₂ ▷ u₁ ⊗≫ 𝟙 (r₂ ≫ u₁) =
    (ρ_ (u₂ ≫ r₁)).inv ≫
      (𝟙 ((u₂ ≫ r₁) ≫ 𝟙 a) ⊗≫
          (u₂ ≫ r₁) ◁ 𝟙 a ◁ (adj₃.unit ⊗≫ f₁ ◁ adj₂.unit ▷ u₁ ⊗≫ 𝟙 ((f₁ ≫ l₂) ≫ r₂ ≫ u₁)) ⊗≫
            (u₂ ≫ r₁) ◁ ((λ_ (f₁ ≫ l₂)).hom ≫ α ≫ (ρ_ (l₁ ≫ f₂)).inv) ▷ (r₂ ≫ u₁) ⊗≫
              (𝟙 ((u₂ ≫ r₁) ≫ l₁ ≫ f₂) ⊗≫ u₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₄.counit) ▷ 𝟙 d ▷ (r₂ ≫ u₁) ⊗≫
                𝟙 (𝟙 d ≫ r₂ ≫ u₁)) ≫
        (λ_ (r₂ ≫ u₁)).hom

Tactic:
bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ (mateEquiv adj₁ adj₂) α ≫ h ◁ ((ρ_ r₂).inv ≫ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (λ_ r₃).hom) =
    𝟙 (r₁ ≫ g) ⊗≫
      ((α_ r₁ g (𝟙 c)).inv ≫
          (mateEquiv adj₁ adj₂) α ▷ 𝟙 c ≫
            (α_ h r₂ (𝟙 c)).hom ≫ h ◁ (mateEquiv adj₂ adj₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (α_ h (𝟙 d) r₃).inv) ⊗≫
        𝟙 (h ≫ r₃)

Tactic:
bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
⊢ 𝟙 (r₁ ≫ g) ⊗≫
      (𝟙 (r₁ ≫ g ≫ 𝟙 c) ⊗≫
          r₁ ◁ (g ≫ 𝟙 c) ◁ adj₃.unit ⊗≫
            r₁ ◁
                ((α_ g (𝟙 c) l₃).hom ≫
                    g ◁ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (α_ g l₂ (𝟙 d)).inv ≫ α ▷ 𝟙 d ≫ (α_ l₁ h (𝟙 d)).hom) ▷
                  r₃ ⊗≫
              adj₁.counit ▷ (h ≫ 𝟙 d) ▷ r₃ ⊗≫ 𝟙 ((h ≫ 𝟙 d) ≫ r₃)) ⊗≫
        𝟙 (h ≫ r₃) =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₃.unit ⊗≫ r₁ ◁ (g ◁ β ≫ α) ▷ r₃ ⊗≫ adj₁.counit ▷ h ▷ r₃ ⊗≫ 𝟙 (h ≫ r₃)

Tactic:
bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ ((ρ_ r₁).inv ≫ (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫ (λ_ r₂).hom) ▷ g ≫ (mateEquiv adj₂ adj₃) β =
    𝟙 (r₁ ≫ g) ⊗≫
      ((α_ r₁ (𝟙 a) g).inv ≫
          (mateEquiv adj₁ adj₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ g ≫
            (α_ (𝟙 b) r₂ g).hom ≫ 𝟙 b ◁ (mateEquiv adj₂ adj₃) β ≫ (α_ (𝟙 b) h r₃).inv) ⊗≫
        𝟙 (h ≫ r₃)

Tactic:
bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ 𝟙 (r₁ ≫ g) ⊗≫
      (𝟙 (r₁ ≫ 𝟙 a ≫ g) ⊗≫
          r₁ ◁ (𝟙 a ≫ g) ◁ adj₃.unit ⊗≫
            r₁ ◁
                ((α_ (𝟙 a) g l₃).hom ≫
                    𝟙 a ◁ β ≫ (α_ (𝟙 a) l₂ h).inv ≫ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ h ≫ (α_ l₁ (𝟙 b) h).hom) ▷
                  r₃ ⊗≫
              adj₁.counit ▷ (𝟙 b ≫ h) ▷ r₃ ⊗≫ 𝟙 ((𝟙 b ≫ h) ≫ r₃)) ⊗≫
        𝟙 (h ≫ r₃) =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₃.unit ⊗≫ r₁ ◁ (β ≫ α ▷ h) ▷ r₃ ⊗≫ adj₁.counit ▷ h ▷ r₃ ⊗≫ 𝟙 (h ≫ r₃)

Tactic:
bicategory

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
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
U : X.Opensᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
⊢ X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map (eqToHom ⋯).op = 𝟙 Γ(X, Opposite.unop U)

Tactic:
← Functor.map_comp,

Goal state after:
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
U : X.Opensᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
⊢ X.presheaf.map ((eqToHom ⋯).op ≫ (eqToHom ⋯).op) = 𝟙 Γ(X, Opposite.unop U)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case neg
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ n, f i ∈ 𝒜 n
hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤
x : A
i : ι
n : ℕ
hn : f i ∈ 𝒜 n
hn' : ¬n = 0
⊢ f i - ↑(((DirectSum.decompose 𝒜) (f i)) 0) ∈ Ideal.span (Set.range f)

Tactic:
· rw [DirectSum.decompose_of_mem_ne 𝒜 hn hn', sub_zero]
      exact Ideal.subset_span ⟨_, rfl⟩

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

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx : ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)

Tactic:
rw [← SetLike.mem_coe] at hx

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx : ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ ↑(fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r)
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)
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)
t : ↑((Spec R).ringCatSheaf.obj.obj (op (basicOpen r)))
this✝² : Module ↑R ↑Γ(M, basicOpen r) := Module.compHom (↑Γ(M, basicOpen r)) (algebraMap ↑R ↑Γ(Spec R, basicOpen r))
this✝¹ : IsScalarTower ↑R ↑Γ(Spec R, basicOpen r) ↑Γ(M, basicOpen r)
this✝ : Module ↑R ↑Γ(N, basicOpen r) := Module.compHom (↑Γ(N, basicOpen r)) (algebraMap ↑R ↑Γ(Spec R, basicOpen r))
this : IsScalarTower ↑R ↑Γ(Spec R, basicOpen r) ↑Γ(N, 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)

Tactic:
exact (IsLocalization.linearMap_compatibleSMul (.powers (M := R) r)
      Γ(Spec R, basicOpen r) Γ(M, basicOpen r) Γ(N, basicOpen r)).map_smul
      (f.hom.app _).hom _ _

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

Goal state before:
pp: case e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ ((IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp
          (algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst))).comp
      (algebraMap (↥(𝒜 0)) (HomogeneousLocalization 𝒜 (Submonoid.powers x.snd.fst))) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))

Tactic:
RingHom.comp_assoc,

Goal state after:
case e_a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
⊢ (IsLocalization.map (Localization.Away (f x.snd.fst)) f ⋯).comp
      ((algebraMap (Away 𝒜 x.snd.fst) (Localization.Away x.snd.fst)).comp
        (algebraMap (↥(𝒜 0)) (HomogeneousLocalization 𝒜 (Submonoid.powers x.snd.fst)))) =
    (algebraMap (↑Γ(X, ⊤)) (Localization.Away (f x.snd.fst))).comp (f.comp (algebraMap (↥(𝒜 0)) A))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case inr
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op ≫ (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op =
    (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

pp: case inr.hU
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ PrimeSpectrum.basicOpen 1 = PrimeSpectrum.basicOpen 1

Tactic:
← Functor.map_comp,

Goal state after:
case inr
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ (modulesSpecToSheaf.obj M).obj.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) =
    (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

case inr.hU
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
U : (Spec (CommRingCat.of ↑R)).Opens
this :
  ∀ (U : (Spec (CommRingCat.of ↑R)).Opens),
    U = PrimeSpectrum.basicOpen 1 →
      tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) U ≫
          (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
        (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
hU : ¬U = PrimeSpectrum.basicOpen 1
⊢ PrimeSpectrum.basicOpen 1 = PrimeSpectrum.basicOpen 1
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
⊢ IsLocalizing N

Tactic:
intro f

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))
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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HomogeneousLocalization.mk { deg := m • n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ } *
    HomogeneousLocalization.mk
      { deg := m • (i - n), num := ⟨(proj 𝒜 (i - n)) x ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩, den_mem := ⋯ }
h : n ≤ i
⊢ Localization.mk
      ↑{ deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(a * ↑(((decompose 𝒜) x) (i - n))) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    Localization.mk ↑{ deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ }.num
        ⟨↑{ deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ?refine_2.refine_1⟩, den_mem := ⋯ }.den, ⋯⟩ *
      Localization.mk
        ↑{ deg := m * (i - n), num := ⟨↑(((decompose 𝒜) x) (i - n)) ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩,
              den_mem := ⋯ }.num
        ⟨↑{ deg := m * (i - n), num := ⟨↑(((decompose 𝒜) x) (i - n)) ^ m, ⋯⟩, den := ⟨f ^ (i - n), ?refine_2.refine_2⟩,
                den_mem := ⋯ }.den,
          ⋯⟩

Tactic:
simp_rw [mul_pow]; rw [Localization.mk_mul]
            · congr; rw [← pow_add, Nat.add_sub_of_le h]

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

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
⊢ IsLocalizing (modulesSpecToSheaf.obj (tilde M))

Tactic:
intro f

Goal state after:
R : CommRingCat
M : ModuleCat ↑R
f : ↑R
⊢ IsLocalizedModule (Submonoid.powers f)
    (ModuleCat.Hom.hom ((modulesSpecToSheaf.obj (tilde M)).obj.map (basicOpen f).leTop.op))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case surj.refine_2
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x).asHomogeneousIdeal
⊢ HomogeneousLocalization.val
      (HomogeneousLocalization.mk { deg := i, num := a, den := ⟨b, hb⟩, den_mem := hb' } *
        (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
          ↑(HomogeneousLocalization.mk { deg := i * m, num := ⟨↑a * b ^ (m - 1), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
                ⟨HomogeneousLocalization.mk { deg := i * m, num := ⟨b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
                  ⋯⟩).2) =
    HomogeneousLocalization.val
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
        (HomogeneousLocalization.mk { deg := i * m, num := ⟨↑a * b ^ (m - 1), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ },
            ⟨HomogeneousLocalization.mk { deg := i * m, num := ⟨b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }, ⋯⟩).1)

Tactic:
simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mul, val_mk,
        mk_eq_mk', ← IsLocalization.mk'_mul, Submonoid.mk_mul_mk, IsLocalization.mk'_eq_iff_eq]
      rw [mul_comm b, mul_mul_mul_comm, ← pow_succ', mul_assoc, tsub_add_cancel_of_le (by lia)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
⊢ S.i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f ≫ f

Tactic:
simp [← S.commSq.w_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f = S.i₁

Tactic:
simp [← S.commSq.w_assoc]

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

Goal state before:
pp: case refine_1
R : CommRingCat
M : (Spec R).Modules
φ : (f : ↑R) →
  ↑((modulesSpecToSheaf.obj M).obj.obj (op ⊤)) →ₗ[↑R] ↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen f))) :=
  fun f ↦ ModuleCat.Hom.hom ((modulesSpecToSheaf.obj M).obj.map (basicOpen f).leTop.op)
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ Aux M ⊤

Tactic:
have hf (f : R) : IsLocalizedModule.Away f (φ f) := h f
    refine ⟨fun f hle s ↦ ?_, fun f hle s hs ↦ ?_⟩
    · obtain ⟨n, y, hy⟩ := (hf f).surj _ _ s
      use n, y, hy.symm
    · obtain ⟨⟨_, n, rfl⟩, hn⟩ := (IsLocalizedModule.eq_zero_iff (.powers f) (φ f)).mp hs
      use n, hn

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

Goal state before:
pp: case e'_4.succ
σ : 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₀
n✝ : ℕ
h : d j = n✝ + 1
⊢ a * d i₀ * (n✝ + 1) = a * d i₀ + a * (n✝ + 1 - 1) * d i₀

Tactic:
· simp only [add_tsub_cancel_right]; ring

Goal state after:
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
B : Type u''
inst✝⁴ : Category.{v'', u''} B
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasColimitsOfSize.{w, w, v'', u''} B
F : A ⥤ B
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F
X : C
x : Φ.fiber.obj X
P : Cᵒᵖ ⥤ A
this : PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ F
⊢ Φ.toPresheafFiber X x (P ⋙ F) ≫
      (((Functor.whiskeringLeft Φ.fiber.Elementsᵒᵖ Cᵒᵖ A).obj (CategoryOfElements.π Φ.fiber).op).isoWhiskerLeft
              (preservesColimitNatIso F).symm).hom.app
        P =
    F.map (Φ.toPresheafFiber X x P)

Tactic:
exact ι_preservesColimitIso_inv F ((CategoryOfElements.π Φ.fiber).op ⋙ P) _

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

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
i : Sigma κ
t : ↑(PrimeSpectrum.basicOpen (a i.fst i.snd)) ⟶ ↑(U ↑i.fst) := (Spec R).homOfLE ⋯
⊢ ((basicOpenIsoSpecAway (a i.fst i.snd)).inv ≫ t) ≫ (U ↑i.fst).ι =
    Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away (a i.fst i.snd))))

Tactic:
simp [t, basicOpenIsoSpecAway]

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ liftAux hG₀ s j ≫ G.map c.op ≫ G.map (F.map d).op = s.ι a ≫ G.map (F.map d ≫ F.map b ≫ (data a.Y).f i).op

Tactic:
← Functor.map_comp,

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
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
he : (↑S).arrows (F.map e ≫ (data X).f j)
⊢ liftAux hG₀ s j ≫ G.map (c.op ≫ (F.map d).op) = s.ι a ≫ G.map (F.map d ≫ F.map b ≫ (data a.Y).f i).op