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

Goal state before:
pp: X✝ Y✝ S✝ : Scheme
f✝ : X✝ ⟶ S✝
inst✝³ : LocallyOfFiniteType f✝
X Y S : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
⊢ IsOpenImmersion ((Scheme.Hom.quasiFiniteLocus f).ι ≫ Scheme.Hom.toNormalization f)

Tactic:
obtain ⟨U, hU, e⟩ := Scheme.Hom.exists_isIso_morphismRestrict_toNormalization f
  convert!
    (inferInstance :
      IsOpenImmersion
        ((X.isoOfEq (U := f.quasiFiniteLocus) (SetLike.coe_injective e.symm)).hom ≫
          f.toNormalization ∣_ U ≫ U.ι)) using 1
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this : IsProper f
⊢ IsProper (Scheme.Hom.imageι f ≫ g)

Tactic:
suffices UniversallyClosed (f.imageι ≫ g) from ⟨⟩

Goal state after:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this : IsProper f
⊢ UniversallyClosed (Scheme.Hom.imageι f ≫ g)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.inv.τr ≫ e.hom.τr = 𝟙 adj₁.r

Tactic:
← comp_τr,

Goal state after:
B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ (e.hom ≫ e.inv).τr = 𝟙 adj₁.r
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ e.hom.τr ≫ e.inv.τr = 𝟙 adj₂.r

Tactic:
← comp_τr,

Goal state after:
B : Type u
inst✝ : Bicategory B
a✝ b✝ c d a b : Adj B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
⊢ (e.inv ≫ e.hom).τr = 𝟙 adj₂.r
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

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

Tactic:
rw [← whisker_exchange, ← whisker_exchange]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ α ▷ (r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
          (((r₁ ≫ l₁) ≫ h₁ ≫ r₂) ◁ β ≫ adj₁.counit ▷ (h₁ ≫ r₂) ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

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

Tactic:
rw [← whisker_exchange, ← whisker_exchange]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (Cover.pullbackHom Y.affineCover f i)

Tactic:
dsimp [Scheme.Cover.pullbackHom]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f], finrank f = 1 → (∃ R, Y = Spec R) → IsIso f
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (pullback.snd f (Y.affineCover.f i))
Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

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

Tactic:
dsimp [Scheme.Cover.pullbackHom]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
x : R
hx : x ∈ nonZeroDivisors R
n : ℕ
hn : ord R x = ↑n
⊢ (ordMonoidWithZeroHom R) x = ↑(Multiplicative.ofAdd ↑n)

Tactic:
simp [ordMonoidWithZeroHom_eq_ord hx, hn]

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ MonoidHom.mker (ordFrac R) = Submonoid.map (algebraMap R K) (IsUnit.submonoid R)

Tactic:
rw [ordFrac_eq_inverse_comp_valuation, ← MonoidWithZeroHom.comap_mker,
      MonoidWithZeroHom.mker_inverse]

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ Submonoid.comap (valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom ⊥ =
    Submonoid.map (algebraMap R K) (IsUnit.submonoid R)
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₂
α : r₁ ⟶ r₂
⊢ (conjugateEquiv adj₁ adj₂).symm α =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom

Tactic:
rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']

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₂
α : r₁ ⟶ r₂
⊢ (λ_ l₂).inv ≫
      (𝟙 (𝟙 c ≫ l₂) ⊗≫
          adj₁.unit ▷ 𝟙 c ▷ l₂ ⊗≫ l₁ ◁ ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ▷ l₂ ⊗≫ l₁ ◁ 𝟙 d ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ 𝟙 d)) ≫
        (ρ_ l₁).hom =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ (conjugateEquiv adj (Adjunction.id c)).symm α = adj.unit ≫ l ◁ α ≫ (ρ_ l).hom

Tactic:
rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']

Goal state after:
B : Type u
inst✝ : Bicategory B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ (λ_ (𝟙 c)).inv ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            l ◁ ((ρ_ r).hom ≫ α ≫ (λ_ (𝟙 c)).inv) ▷ 𝟙 c ⊗≫ l ◁ 𝟙 c ◁ (Adjunction.id c).counit ⊗≫ 𝟙 (l ≫ 𝟙 c)) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h₁
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ zeroLocus 𝒜 ↑(vanishingIdeal t) ⊆ closure t

pp: case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ closure t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)

Tactic:
· rintro x hx t' ⟨ht', ht⟩
    obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus 𝒜 s := by rwa [isClosed_iff_zeroLocus] at ht'
    rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht
    exact Set.Subset.trans ht hx

Goal state after:
case h₂
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ closure t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ z ∈ ↑(basicOpen 𝒜 f) ↔ z ∈ ↑(⨆ i, basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f))

Tactic:
by
      rw [mem_coe_basicOpen, mem_coe, iSup, TopologicalSpace.Opens.mem_sSup]
      constructor <;> intro hz
      · rcases show ∃ i, GradedRing.proj 𝒜 i f ∉ z.asHomogeneousIdeal by
          contrapose! hz with H
          classical
          rw [← DirectSum.sum_support_decompose 𝒜 f]
          apply Ideal.sum_mem _ fun i _ => H i with ⟨i, hi⟩
        exact ⟨basicOpen 𝒜 (GradedRing.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩
      · obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz
        exact fun rid => hz (z.1.2 i rid)

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ x ∈ ProjectiveSpectrum.basicOpen 𝒜 ↑f.den

Tactic:
rw [ProjectiveSpectrum.mem_basicOpen]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ ↑f.den ∉ x.asHomogeneousIdeal
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨x, rfl⟩ := Quotient.mk''_surjective x

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
R : ValuationSubring K
⊢ IsMax R.toLocalSubring

Tactic:
intro S

Goal state after:
K : Type u_3
inst✝ : Field K
R : ValuationSubring K
S : LocalSubring K
⊢ R.toLocalSubring ≤ S → S ≤ R.toLocalSubring
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
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (ConcreteCategory.hom (toSpec 𝒜 f).base) x =
    PrimeSpectrum.comap (mapId 𝒜 ⋯) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Tactic:
change PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x).hom
        (IsLocalRing.closedPoint ((Proj| pbo f).presheaf.stalk x)) = _
  rw [awayToΓ_ΓToStalk, CommRingCat.hom_comp, PrimeSpectrum.comap_comp]
  exact congr(PrimeSpectrum.comap _ $(@IsLocalRing.comap_closedPoint
    (HomogeneousLocalization.AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) _ _
    ((Proj| pbo f).presheaf.stalk x) _ _ _ (isLocalHom_of_isIso _)))

Goal state after:
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
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (Scheme.ΓSpecIso (CommRingCat.of (A⁰_ f))).inv ≫
      (toSpec 𝒜 f).c.app (op ⊤) ≫ (Proj.restrict ⋯).presheaf.germ ((Opens.map (toSpec 𝒜 f).base).obj ⊤) x ⋯ =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x

Tactic:
erw [toOpen_toSpec_val_c_app_assoc]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.map (homOfLE ⋯).op) ≫
      (Proj.restrict ⋯).presheaf.germ ((Opens.map (toSpec 𝒜 f).base).obj ⊤) x ⋯ =
    awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case map_units
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
y : NumDenSameDeg 𝒜 (Submonoid.powers f)
hy : HomogeneousLocalization.mk y ∈ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x).asIdeal.primeCompl
⊢ HomogeneousLocalization.val
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) ↑⟨HomogeneousLocalization.mk y, hy⟩ *
        HomogeneousLocalization.mk { deg := y.deg, num := y.den, den := y.num, den_mem := ⋯ }) =
    HomogeneousLocalization.val 1

Tactic:
simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mul, val_mk,
      mk_eq_mk', val_one, IsLocalization.mk'_mul_mk'_eq_one']

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

Goal state before:
pp: case hxj
σ : Type u_1
A : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
⊢ (fun x_1 ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))

Tactic:
convert! SetLike.pow_mem_graded _ _ using 2
      · infer_instance
      · exact hx ▸ SetLike.mul_mem_graded hf hg

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

Goal state before:
pp: P Q : MorphismProperty Scheme
S : Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
inst✝ : P.RespectsIso
⊢ ∀ ⦃X : Over S⦄ (S_1 : Presieve X) (Ti : ⦃Y : Over S⦄ → (f : Y ⟶ X) → S_1 f → Presieve Y),
    S_1 ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver} →
      (∀ ⦃Y : Over S⦄ (f : Y ⟶ X) (H : S_1 f), Ti f H ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}) →
        S_1.bind Ti ∈ {R | ∃ 𝒰 x, R = 𝒰.toPresieveOver}

Tactic:
by
    rintro X _ T ⟨𝒰, h, rfl⟩ H
    choose V h hV using H
    refine ⟨𝒰.bind (fun j => V ((𝒰.f j).asOver S) ⟨j⟩), inferInstance, ?_⟩
    convert!
      Presieve.ofArrows_bind _ (fun j ↦ (𝒰.f j).asOver S) _ (fun Y f H j ↦ ((V f H).X j).asOver S)
        (fun Y f H j ↦ ((V f H).f j).asOver S)
    apply hV

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

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

Tactic:
intro S

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
⊢ ⋯.HasLift
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
⊢ ValuativeCriterion.Uniqueness f

Tactic:
intro S

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
⊢ Subsingleton ⋯.LiftStruct
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: case right.smul
σ : 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 : ↥(𝒜 0)
x₀ : Away 𝒜 (x i₀)
hx :
  x₀ ∈
    Submodule.span ↥(𝒜 0) {x_1 | ∃ a ai, ∃ (hai : ∑ i, ai i • d i = a • d i₀), Away.mk 𝒜 ⋯ a (∏ i, x i ^ ai i) ⋯ = x_1}
hx1 : (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) x₀) ≤ 1
⊢ (valuation O K) ((φ'.comp (awayMap 𝒜 ⋯ ⋯)) (a • x₀)) ≤ 1

Tactic:
simp only [Algebra.smul_def, RingHom.coe_comp, Function.comp_apply, map_mul, ge_iff_le]
    refine mul_le_one' ?_ hx1
    rw [RingHom.algebraMap_toAlgebra, awayMap_fromZeroRingHom 𝒜 (hxdi j) (mul_comm (x j) (x i₀)),
      ← awayMap_fromZeroRingHom 𝒜 (hxdi i₀) rfl a, hφ'1]
    change valuation O K (φ.comp (fromZeroRingHom 𝒜 (.powers (x j))) a) ≤ 1
    simp only [← hcomm, RingHom.coe_comp, Function.comp_apply, ← Valuation.mem_integer_iff,
      IsFractionRing.coe_inj, exists_eq, mem_integer_iff]

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

Goal state before:
pp: case refine_1
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 : ⨆ 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, PrimeSpectrum.basicOpen (a i.fst i.snd)

Tactic:
rw [eq_comm, iSup_sigma, ← hs]

Goal state after:
case refine_1
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 : ⨆ 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, ⨆ j, PrimeSpectrum.basicOpen (a ⟨i, j⟩.fst ⟨i, j⟩.snd) = ⨆ i, U ↑i
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

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

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

Tactic:
· intro M ⟨N, ⟨e⟩⟩
    exact (SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf).prop_of_iso e
      (by dsimp; infer_instance)

Goal state after:
case refine_2
R : CommRingCat
⊢ SheafOfModules.isQuasicoherent (Spec R).ringCatSheaf ≤ (tilde.functor R).essImage
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
T : C
hT : IsTerminal T
⊢ ∀ ⦃X Y : Cᵒᵖ ⥤ D⦄ (f : X ⟶ Y),
    ((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).map f ≫
        {
          app := fun x ↦
            match x with
            | Opposite.op X => Y.map (hT.from X).op,
          naturality := ⋯ } =
      {
          app := fun x ↦
            match x with
            | Opposite.op X_1 => X.map (hT.from X_1).op,
          naturality := ⋯ } ≫
        (𝟭 (Cᵒᵖ ⥤ D)).map f

Tactic:
intros

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
T : C
hT : IsTerminal T
X✝ Y✝ : Cᵒᵖ ⥤ D
f✝ : X✝ ⟶ Y✝
⊢ ((evaluation Cᵒᵖ D).obj (Opposite.op T) ⋙ const Cᵒᵖ).map f✝ ≫
      {
        app := fun x ↦
          match x with
          | Opposite.op X => Y✝.map (hT.from X).op,
        naturality := ⋯ } =
    {
        app := fun x ↦
          match x with
          | Opposite.op X => X✝.map (hT.from X).op,
        naturality := ⋯ } ≫
      (𝟭 (Cᵒᵖ ⥤ D)).map 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 : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
⊢ F.map g ≫ f = p ≫ (data X).f i

Tactic:
fac

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ : C₀
f : F.obj X₀ ⟶ X
Y₀ : C₀
g : Y₀ ⟶ X₀
i : (data X).I₀
p : F.obj Y₀ ⟶ F.obj ((data X).X i)
fac : p ≫ (data X).f i = F.map g ≫ f
hg : ((data X).sieve f).arrows g
⊢ F.map g ≫ f = F.map g ≫ f