mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
this : (↑(Algebra.TensorProduct.comm R S T)).comp includeLeftRingHom = ↑includeRight
⊢ ((pullbackSpecIso' R T S).inv ≫ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
Category.assoc,

Goal state after:
case h₀
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
this : (↑(Algebra.TensorProduct.comm R S T)).comp includeLeftRingHom = ↑includeRight
⊢ (pullbackSpecIso' R T S).inv ≫
      (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
        pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.fst (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
Module: Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

Goal state before:

Tactic:
η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_η)]
    _ = θ.hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_θ)]

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

Goal state before:
pp: case h₁
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
this : (↑(Algebra.TensorProduct.comm R S T)).comp ↑includeRight = includeLeftRingHom
⊢ ((pullbackSpecIso' R T S).inv ≫ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))

Tactic:
Category.assoc,

Goal state after:
case h₁
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
this : (↑(Algebra.TensorProduct.comm R S T)).comp ↑includeRight = includeLeftRingHom
⊢ (pullbackSpecIso' R T S).inv ≫
      (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom ≫
        pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R)) =
    (Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv) ≫
      pullback.snd (Spec (of S) ↘ Spec (of R)) (Spec (of T) ↘ Spec (of R))
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    ((pullbackSpecIso' R S T).inv ≫ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).inv) ≫
      pullback.snd (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))

Tactic:
Category.assoc,

Goal state after:
R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    (pullbackSpecIso' R S T).inv ≫
      (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).inv ≫
        pullback.snd (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
X M G : Scheme
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ≪≫ pullbackSpecIso' R S T).hom ≫
      Spec (of (S ⊗[R] T)) ↘ Spec (of S) =
    pullback (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R)) ↘ Spec (of S)

Tactic:
by
    rw [← cancel_epi (pullbackSymmetry .. ≪≫ pullbackSpecIso' ..).inv,
      Scheme.canonicallyOverPullback_over, Iso.inv_hom_id_assoc, Iso.trans_inv, Category.assoc,
      pullbackSymmetry_inv_comp_snd]
    exact (pullbackSpecIso_inv_fst ..).symm

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

Goal state before:

Tactic:
_ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory

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

Goal state before:
pp: C✝ D✝ E : Type u
inst✝² : Category.{v, u} C✝
inst✝¹ : Category.{v, u} D✝
inst✝ : Category.{v, u} E
F✝ : C✝ ⥤ D✝
G✝ : D✝ ⥤ C✝
adj✝ : F✝ ⊣ G✝
F' : D✝ ⥤ E
G' : E ⥤ D✝
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : ↑D
⊢ adj.unit.toNatTrans.app (G.toFunctor.obj X) ≫ G.toFunctor.map (adj.counit.toNatTrans.app X) = 𝟙 (G.toFunctor.obj X)

Tactic:
simpa using congr($(adj.right_triangle).toNatTrans.app X)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
⊢ IsOpenImmersion f

Tactic:
let f' := hU.lift U.ι f (by simp [U])

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := lift U.ι f ⋯
⊢ IsOpenImmersion f
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
⊢ IsAffine.finrank (Spec.map f) x✝ = (CommRingCat.Hom.hom f).finrank x✝

Tactic:
IsAffine.finrank

Goal state after:
R S : CommRingCat
f : R ⟶ S
hf₁✝ : IsFinite (Spec.map f)
hf₂✝ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x✝ : ↥(Spec R)
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Spec R).isoSpec.hom x✝) = (CommRingCat.Hom.hom f).finrank x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
⊢ 1 ≤ finrank f (f x)

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
hY : ∃ R, Y = Spec R
⊢ 1 ≤ finrank f (f x)

Tactic:
· obtain ⟨R, g, hg, y, hy⟩ := Y.exists_Spec_apply_eq (f x)
    rw [← hy, ← finrank_pullback_snd]
    obtain ⟨z, hzl, hzr⟩ := Scheme.Pullback.exists_preimage_pullback (f := f) (g := g) x y hy.symm
    rw [hzr.symm]
    refine this _ _ ⟨_, rfl⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
hY : ∃ R, Y = Spec R
⊢ 1 ≤ finrank f (f x)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
⊢ (Submodule.mkQ (a • I) ∘ₗ (mul R R) a).ker ≤ I

Tactic:
· have m : I = Submodule.comap (mul R R a) (a • I) := by
      ext b
      exact (Submodule.mul_mem_smul_iff ha).symm
    simp [← m, ker_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ zeroLocus ↑(Ideal.span (⇑(Pi.evalRingHom (fun x ↦ ↑(R x)) i) '' t)) = ∅

Tactic:
zeroLocus_span,

Goal state after:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → ↑(R i)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → ↑(R i))))
hV : ↑(Scheme.Hom.opensRange (sigmaSpec R)) ⊆ V
hV' : IsCompact V
hVU : V ⊆ ↑U
s : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hs : U.carrierᶜ = zeroLocus s
t : Set ↑(CommRingCat.of ((i : ι) → ↑(R i)))
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ zeroLocus (⇑(Pi.evalRingHom (fun x ↦ ↑(R x)) i) '' t) = ∅
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ 𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁ = 𝟙 r₁

Tactic:
rw [adj₁.right_triangle]

Goal state after:
B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ 𝟙 r₁ ⊗≫ ((ρ_ r₁).hom ≫ (λ_ r₁).inv) ⊗≫ 𝟙 r₁ = 𝟙 r₁
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₂
⊢ (conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₃) β = (conjugateEquiv adj₁ adj₃) (β ≫ α)

Tactic:
by
  simp only [conjugateEquiv_apply]
  calc
    _ = 𝟙 r₁ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ _).hom ≫ α ≫ (ρ_ _).inv))
            (mateEquiv adj₂ adj₃ ((λ_ _).hom ≫ β ≫ (ρ_ _).inv)) ⊗≫ 𝟙 r₃ := by
      dsimp only [rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply']
      bicategory

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩)) ≫
      (Sigma.ι (fun i ↦ Spec (R' i)) (j i) ≫ sigmaSpec R') ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀) =
    f i

Tactic:
Category.assoc,

Goal state after:
ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝¹ : CompactSpace ↥X
inst✝ : ∀ (i : ι), IsLocalRing ↑(R i)
f : (i : ι) → Spec (R i) ⟶ X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
j : ι → 𝒰.I₀
hj : ∀ (i : ι), Set.range ⇑(f i) ⊆ ↑(Scheme.Hom.opensRange (𝒰.f (j i)))
g : (j₀ : 𝒰.I₀) → Spec (CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))) ⟶ 𝒰.X j₀
hg :
  ∀ (j₀ : 𝒰.I₀) (x : { i // j i = j₀ }),
    Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x ↦ ↑(R ↑x)) x)) ≫ g j₀ = IsOpenImmersion.lift (𝒰.f j₀) (f ↑x) ⋯
R' : 𝒰.I₀ → CommRingCat := fun j₀ ↦ CommRingCat.of ((i : { i // j i = j₀ }) → ↑(R ↑i))
e : ((i : ι) → ↑(R i)) ≃+* ((j₀ : 𝒰.I₀) → ↑(R' j₀)) :=
  { toFun := fun f x i ↦ f ↑i, invFun := fun f i ↦ f (j i) ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ (Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩)) ≫
      Sigma.ι (fun i ↦ Spec (R' i)) (j i) ≫ sigmaSpec R' ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀) =
    f i
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_2
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
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ ∀ ⦃X_1 Y_1 : (TopologicalSpace.Opens ↥X)ᵒᵖ⦄ (f_1 : X_1 ⟶ Y_1),
    ((SheafOfModules.forget X.ringCatSheaf).obj (restrict (unit Y.ringCatSheaf) f)).map f_1 ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (X.ringCatSheaf.obj.map f_1))).map
          (ModuleCat.isoMk
              ((forget₂ CommRingCat RingCat ⋙ forget₂ RingCat Ab).mapIso (Hom.appIso f (Opposite.unop Y_1))) ⋯).hom =
      (ModuleCat.isoMk ((forget₂ CommRingCat RingCat ⋙ forget₂ RingCat Ab).mapIso (Hom.appIso f (Opposite.unop X_1)))
            ⋯).hom ≫
        ((SheafOfModules.forget X.ringCatSheaf).obj (unit X.ringCatSheaf)).map f_1

Tactic:
· intro U V g
    have : Y.presheaf.map (homOfLE (by grw [leOfHom g.unop])).op ≫
        (f.appIso _).hom = (f.appIso U.unop).hom ≫ X.presheaf.map g := by
      simp [Hom.appIso_hom']
    ext x
    exact congr($(this) x)

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

Goal state before:
pp: X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ (((restrictFunctor f).obj M).presheaf.germ U x hxU ≫ (restrictStalkNatIso f x).hom.app M) ≫
      (restrictStalkNatIso f x).inv.app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU

Tactic:
Category.assoc,

Goal state after:
X Y : Scheme
U : X.Opens
f : X ⟶ Y
inst✝ : IsOpenImmersion f
x : ↥X
M : Y.Modules
hxU : x ∈ U
⊢ ((restrictFunctor f).obj M).presheaf.germ U x hxU ≫
      (restrictStalkNatIso f x).hom.app M ≫ (restrictStalkNatIso f x).inv.app M =
    ((restrictFunctor f).obj M).presheaf.germ U x hxU
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
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    (basicOpen 𝒜 f).ι ≫ (Proj 𝒜).topIso.inv ≫ ((Proj 𝒜).isoOfEq e).inv = (Proj 𝒜).homOfLE ⋯
⊢ (basicOpen 𝒜 f).toSpecΓ ≫
      Spec.map ((Proj 𝒜).presheaf.map (homOfLE ⋯).op) ≫
        Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    ((basicOpen 𝒜 f).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f)) ≫
      Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))

Tactic:
Category.assoc,

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
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    (basicOpen 𝒜 f).ι ≫ (Proj 𝒜).topIso.inv ≫ ((Proj 𝒜).isoOfEq e).inv = (Proj 𝒜).homOfLE ⋯
⊢ (basicOpen 𝒜 f).toSpecΓ ≫
      Spec.map ((Proj 𝒜).presheaf.map (homOfLE ⋯).op) ≫
        Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))) =
    (basicOpen 𝒜 f).toSpecΓ ≫
      Spec.map (awayToSection 𝒜 f) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)))
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' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ ((basicOpen 𝒜 x).toSpecΓ ≫ Spec.map (awayToSection 𝒜 x)) ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) =
    (Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f

Tactic:
Category.assoc,

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ (basicOpen 𝒜 x).toSpecΓ ≫ Spec.map (awayToSection 𝒜 x) ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) =
    (Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f
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'
x : A
hx : x = f * g
⊢ ((pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))) ≫
      awayι 𝒜 f f_deg hm =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ?hx).hom ≫ awayι 𝒜 ?x ⋯ ⋯

pp: case x
σ : 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'
x : A
hx : x = f * g
⊢ A

pp: case hx
σ : 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'
x : A
hx : x = f * g
⊢ ?x = f * g

Tactic:
Category.assoc,

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'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ?hx).hom ≫ awayι 𝒜 ?x ⋯ ⋯

case x
σ : 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'
x : A
hx : x = f * g
⊢ A

case hx
σ : 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'
x : A
hx : x = f * g
⊢ ?x = f * g
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'
x : A
hx : x = f * g
⊢ ((pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯))) ≫
      awayι 𝒜 g g_deg hm' =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯

Tactic:
Category.assoc,

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'
x : A
hx : x = f * g
⊢ (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯)) ≫ awayι 𝒜 g g_deg hm' =
    (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom ≫ awayι 𝒜 x ⋯ ⋯
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
⊢ (tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen 1) ≫
        (modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).presheaf.map (homOfLE ⋯).op) ≫
      (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
    (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op

Tactic:
Category.assoc,

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
⊢ tilde.toOpen ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)) (PrimeSpectrum.basicOpen 1) ≫
      (modulesSpecToSheaf.obj (tilde ((modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)))).presheaf.map (homOfLE ⋯).op ≫
        (modulesSpecToSheaf.map M.fromTildeΓ).hom.app (op U) =
    (modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ ((basicOpenIsoSpec ℬ (f s) ⋯ hi).inv ≫ (basicOpen ℬ (f s)).ι) ≫ map f hf =
    Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ (basicOpenIsoSpec 𝒜 s hs hi).inv ≫ (basicOpen 𝒜 s).ι

Tactic:
Category.assoc,

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ (basicOpenIsoSpec ℬ (f s) ⋯ hi).inv ≫ (basicOpen ℬ (f s)).ι ≫ map f hf =
    Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ (basicOpenIsoSpec 𝒜 s hs hi).inv ≫ (basicOpen 𝒜 s).ι
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor

Goal state before:
pp: A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ awayι ℬ (f s) ⋯ hi ≫ map f hf = Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ awayι 𝒜 s hs hi

Tactic:
rw [awayι, awayι, Category.assoc, ι_comp_map, ← Category.assoc, ← Category.assoc]

Goal state after:
A B σ τ : Type u
inst✝⁷ : CommRing A
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubgroupClass σ A
inst✝⁴ : CommRing B
inst✝³ : SetLike τ B
inst✝² : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst✝¹ : GradedRing 𝒜
inst✝ : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : ℬ₊ ≤ HomogeneousIdeal.map f (𝒜₊)
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ ((basicOpenIsoSpec ℬ (f s) ⋯ hi).inv ≫ Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯) ≫
      (basicOpen 𝒜 s).ι =
    (Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ (basicOpenIsoSpec 𝒜 s hs hi).inv) ≫ (basicOpen 𝒜 s).ι
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
⊢ A ≤ (ofPrime A P).toSubring

Tactic:
intro x hx
  exact ⟨algebraMap A _ ⟨x, hx⟩, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
⊢ R.toLocalSubring ≤ S → S ≤ R.toLocalSubring

Tactic:
hS

Goal state after:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
hS : R.toLocalSubring ≤ S
⊢ S ≤ R.toLocalSubring