mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) i (Sum.inr j) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n) i (Sum.inr j)

Tactic:
· suffices (if j.1 ≤ i then f.coeff (i - j) else 0) =
      if j ≤ i.1 ∧ ↑i ≤ j + m then f.coeff (i - j) else 0 by
        simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']
    rw [ite_and]
    split_ifs with h₁ h₂ <;> try rfl
    exact coeff_eq_zero_of_natDegree_lt (by lia)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : f.natDegree = 0
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g

pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g

Tactic:
· obtain rfl := eq_one_of_monic_natDegree_zero hf hf0; simp [isCoprime_one_left]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
⊢ IsUnit (f.resultant g) ↔ IsCoprime f g
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
I : Ideal R
hI : (Ideal.map (algebraMap R S) I).FG
⊢ I.FG

Tactic:
by
  change Submodule.FG I
  rw [← Module.Finite.iff_fg]
  let f : S ⊗[R] I →ₗ[S] S :=
    (AlgebraTensorModule.rid _ _ _).toLinearMap ∘ₗ AlgebraTensorModule.lTensor S S I.subtype
  have hf : Function.Injective f := by simp [f]
  have : I.map (algebraMap R S) = LinearMap.range f := by
    refine le_antisymm ?_ ?_
    · rw [Ideal.map_le_iff_le_comap]
      intro x hx
      use 1 ⊗ₜ ⟨x, hx⟩
      simp [f, Algebra.smul_def]
    · rintro - ⟨x, rfl⟩
      induction x with
      | zero => simp
      | add _ _ _ _ => simp_all [Ideal.add_mem]
      | tmul s x =>
        have : f (s ⊗ₜ[R] x) = s • f (1 ⊗ₜ x) := by simp [f]
        rw [this]
        apply Ideal.mul_mem_left
        simpa [f, Algebra.smul_def] using Ideal.mem_map_of_mem _ x.2
  let e : S ⊗[R] I ≃ₗ[S] I.map (algebraMap R S) := .ofInjective _ hf ≪≫ₗ .ofEq _ _ this.symm
  have : Module.Finite S (S ⊗[R] ↥I) := by
    rwa [Module.Finite.equiv_iff e, Module.Finite.iff_fg]
  apply Module.Finite.of_finite_tensorProduct_of_faithfullyFlat S

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: case left
X✝ : Scheme
P : MorphismProperty Scheme
S : Scheme
U X Y : P.Over ⊤ S
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f.left
inst✝ : IsOpenImmersion g.left
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        ((span f g ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).map
          (WidePushoutShape.Hom.init WalkingPair.left)))

Tactic:
simpa using! f.left.isOpenEmbedding.injective

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : StrictPseudofunctor B C
G : StrictPseudofunctor C D
a✝ b✝ c✝ : B
x✝¹ : a✝ ⟶ b✝
x✝ : b✝ ⟶ c✝
⊢ (F.comp G.toStrictlyUnitaryPseudofunctor).mapComp x✝¹ x✝ = eqToIso ⋯

Tactic:
by
    ext
    simp [StrictPseudofunctor.mapComp_eq_eqToIso,
      PrelaxFunctor.map₂_eqToHom]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
η' : g ≅ h
ih_η : η'.hom = η
⊢ (f ◁ᵢ η').hom = f ◁ η

Tactic:
simp [ih_η]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
h : b ⟶ c
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
⊢ (η' ▷ᵢ h).hom = η ▷ h

Tactic:
simp [ih_η]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
η η' : f ⟶ g
θ θ' : g ⟶ h
ι : f ⟶ h
e_η : η = η'
e_θ : θ = θ'
e_ηθ : η' ≫ θ' = ι
⊢ η ≫ θ = ι

Tactic:
by
  simp [e_η, e_θ, e_ηθ]

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a b : B
f : a ⟶ b
g : b ⟶ a
F : StrictPseudofunctor B C
adj : f ⊣ g
⊢ (F.mapAdjunction adj).unit = eqToHom ⋯ ≫ F.map₂ adj.unit ≫ eqToHom ⋯

Tactic:
by
  simp [F.mapId_eq_eqToIso, F.mapComp_eq_eqToIso]

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
a b : B
f : a ⟶ b
g : b ⟶ a
F : StrictPseudofunctor B C
adj : f ⊣ g
⊢ (F.mapAdjunction adj).counit = eqToHom ⋯ ≫ F.map₂ adj.counit ≫ eqToHom ⋯

Tactic:
by
  simp [F.mapId_eq_eqToIso, F.mapComp_eq_eqToIso]

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ↔ Function.Surjective (PrimeSpectrum.comap (algebraMap R S))

Tactic:
PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Flat R S
inst✝ : Module.Finite R S
⊢ Function.Surjective (PrimeSpectrum.comap (algebraMap R S)) ↔
    Function.Surjective (PrimeSpectrum.comap (algebraMap R S))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
y : ↥Y
⊢ finrank f y = 1 y

Tactic:
obtain ⟨R, g, _, y, rfl⟩ := Y.exists_Spec_apply_eq y

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
⊢ finrank f (g y) = 1 (g y)
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
ϖ : R
hϖ : Irreducible ϖ
⊢ (ordFrac R) ((algebraMap R K) ϖ) = WithZero.exp 1

Tactic:
by
  simp [ordFrac_eq_valuation_inv, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap,
    IsDiscreteValuationRing.intValuation_maximalIdeal,
    IsDiscreteValuationRing.addVal_uniformizer hϖ, ← WithZero.exp_eq_coe_ofAdd]

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
x y : K
h : (ordFrac R) x = (ordFrac R) y
⊢ ∃ u, u • x = y

Tactic:
ordFrac_eq_valuation_inv,

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
x y : K
h : ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) x)⁻¹ = (ordFrac R) y
⊢ ∃ u, u • x = y
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
x y : K
h : ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) x)⁻¹ = (ordFrac R) y
⊢ ∃ u, u • x = y

Tactic:
ordFrac_eq_valuation_inv,

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
x y : K
h :
  ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) x)⁻¹ =
    ((valuation K (IsDiscreteValuationRing.maximalIdeal R)) y)⁻¹
⊢ ∃ u, u • x = y
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ)

Tactic:
by
  dsimp only [comp, vcomp, hcomp]
  calc
    _ = 𝟙 _ ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory

Goal state after:
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₁
⊢ (conjugateEquiv adj₁ adj₁).symm (𝟙 r₁) = 𝟙 l₁

Tactic:
rw [Equiv.symm_apply_eq, conjugateEquiv_id]

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₃
α : r₁ ⟶ r₂
β : r₂ ⟶ r₃
⊢ (conjugateEquiv adj₁ adj₃) ((conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α) = α ≫ β

Tactic:
← conjugateEquiv_comp _ adj₂

Goal state after:
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₃
α : r₁ ⟶ r₂
β : r₂ ⟶ r₃
⊢ (conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α) ≫
      (conjugateEquiv adj₂ adj₃) ((conjugateEquiv adj₂ adj₃).symm β) =
    α ≫ β
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case mp
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : (GradedRing.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
⊢ ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u

Tactic:
exact ⟨basicOpen 𝒜 (GradedRing.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩

Goal state after:
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:
rw [← DirectSum.sum_support_decompose 𝒜 x, map_sum, DirectSum.decompose_sum,
    DirectSum.decompose_sum, map_sum]
  congr 1
  simp [DirectSum.decompose_of_mem _ (map_mem f (Subtype.prop _)),
    DirectSum.decompose_of_mem _ (Subtype.prop _), DirectSum.map_of, GradedRingHom.gradedAddHom]

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 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ Va ⊓ Vb
wa :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b : a_1 ∈ Va),
    a ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
wb :
  ∀ (a : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a ∈ Vb),
    b ⟨a, ⋯⟩ = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ (fun x ↦ (a * b) ((Va.infLELeft Vb ≫ ia) x)) ⟨y, hy⟩ =
    HomogeneousLocalization.mk { deg := ja + jb, num := ⟨ra * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }

Tactic:
simp [wa y hy.1, wb y hy.2, ext_iff_val, Localization.mk_mul]

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 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ val (↑(sectionInBasicOpen 𝒜 x f) ((homOfLE ⋯ ≫ homOfLE ⋯).op.unop ⟨t, ⋯⟩)) =
    val (↑(sectionInBasicOpen 𝒜 x g) ((homOfLE ⋯ ≫ homOfLE ⋯).op.unop ⟨t, ⋯⟩))

Tactic:
simp only [sectionInBasicOpen, HomogeneousLocalization.val_mk, Localization.mk_eq_mk',
      IsLocalization.mk'_eq_iff_eq]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑g.den * ↑f.num) =
    (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑f.den * ↑g.num)
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 𝒜
x : Submonoid A
f g : ↥(𝒜 0)
⊢ mk { deg := 0, num := f + g, den := 1, den_mem := ⋯ } =
    mk { deg := 0, num := f, den := 1, den_mem := ⋯ } + mk { deg := 0, num := g, den := 1, den_mem := ⋯ }

Tactic:
ext; simp [Localization.add_mk, add_comm f.1 g.1]

Goal state after:
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
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)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
⊢ (ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯))) x =
    (ConcreteCategory.hom (Hom.appIso (X.homOfLE ⋯) (Opposite.unop W)).inv) x

Tactic:
rw [Scheme.Hom.appIso_homOfLE_inv]

Goal state after:
case refine_2
X✝ Y Z T : Scheme
M N K : X✝.Modules
φ : M ⟶ N
U✝ V✝ : X✝.Opens
X : Scheme
U V : X.Opens
f : V ⟶ U
this✝⁴ :
  (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥↑V) (Opens.grothendieckTopology ↑U.carrier)
this✝³ :
  Functor.IsDenseSubsite (Opens.grothendieckTopology ↥U) ((Opens.grothendieckTopology ↥X).over U)
    (Opens.overEquivalence U).inverse
this✝² : (Hom.opensFunctor (X.homOfLE ⋯)).IsContinuous (Opens.grothendieckTopology ↥V) (Opens.grothendieckTopology ↥↑U)
this✝¹ :
  ((Opens.overEquivalence V).symm.functor ⋙ Over.map f).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
this✝ :
  (Opens.overEquivalence U).symm.functor.IsContinuous (Opens.grothendieckTopology ↥↑U)
    ((Opens.grothendieckTopology ↥X).over U)
this :
  (Hom.opensFunctor (X.homOfLE ⋯) ⋙ (Opens.overEquivalence U).symm.functor).IsContinuous (Opens.grothendieckTopology ↥V)
    ((Opens.grothendieckTopology ↥X).over U)
W : (TopologicalSpace.Opens ↥V)ᵒᵖ
x : ↑(((Opens.sheafRestrict V).obj X.ringCatSheaf).obj.obj W)
⊢ (ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯))) x = (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case refine_1
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j) ∈ 𝒜 ?m.548

Tactic:
apply GradedMonoid.toGradedMul.mul_mem

Goal state after:
case refine_1.a
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) a ^ j ∈ 𝒜 ?refine_1.i

case refine_1.a
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ (proj 𝒜 i) b ^ (m - j) ∈ 𝒜 ?refine_1.j

case refine_1.i
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ℕ

case refine_1.j
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ℕ
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
⊢ IsUnit ((algebraMap (Away 𝒜 f) (Away 𝒜 x)) (isLocalizationElem hf hg) ^ n)

Tactic:
RingHom.algebraMap_toAlgebra

Goal state after:
case map_units
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
⊢ IsUnit ((awayMap 𝒜 hg hx) (isLocalizationElem hf hg) ^ n)
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'
⊢ awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g = PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)

Tactic:
by
  ext1
  trans Set.range (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg rfl)))
  · rw [← pullbackAwayιIso_inv_fst 𝒜 f_deg hm g_deg hm' rfl]
    simp only [TopologicalSpace.Opens.map_coe, Scheme.Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_comp]
    rw [Set.range_eq_univ.mpr (by exact
      (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective),
      ← opensRange_awayι _ _ g_deg hm']
    simp [IsOpenImmersion.range_pullbackFst]
  · let := (awayMap (f := f) 𝒜 g_deg rfl).toAlgebra
    let := HomogeneousLocalization.Away.isLocalization_mul f_deg g_deg rfl hm.ne'
    exact PrimeSpectrum.localization_away_comap_range _ _

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 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
⊢ X ⟶ Proj 𝒜

Tactic:
by
  refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).glueMorphisms
    (fun ri ↦ toBasicOpenOfGlobalSections 𝒜 f rfl ri.2.2.1 ri.2.2.2 ≫ Scheme.Opens.ι _) ?_
  rintro x y
  let e : pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x)
      ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅ (X.basicOpen (f (x.snd.fst * y.snd.fst))) :=
    (isPullback_opens_inf _ _).isoPullback.symm ≪≫ X.isoOfEq (by simp)
  rw [← cancel_epi e.inv]
  trans toBasicOpenOfGlobalSections 𝒜 f rfl (Nat.add_pos_left x.2.2.1 y.1)
    (SetLike.mul_mem_graded x.2.2.2 y.2.2.2) ≫ (Scheme.Opens.ι _)
  · simpa [e, openCoverOfMapIrrelevantEqTop, Scheme.isoOfEq_inv] using
      homOfLE_toBasicOpenOfGlobalSections_ι _ _ rfl rfl y.2.2.2
  · simpa [e, openCoverOfMapIrrelevantEqTop, Scheme.isoOfEq_inv] using
      (homOfLE_toBasicOpenOfGlobalSections_ι _ _ (mul_comm _ _) (add_comm _ _) x.2.2.2).symm

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 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
⊢ Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (X.basicOpen (f r)) ⋯ =
    toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr

Tactic:
rw [← (Iso.inv_comp_eq _).mpr (fromOfGlobalSections_morphismRestrict 𝒜 f hf hn hr),
    ← Scheme.Hom.resLE_eq_morphismRestrict]

Goal state after:
σ : 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
⊢ Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (X.basicOpen (f r)) ⋯ =
    (X.isoOfEq ⋯).inv ≫
      Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r) ⋯
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M N : ModuleCat ↑R
f : M ⟶ N
U : Opens (PrimeSpectrum ↑R)
⊢ toOpen M U ≫ (modulesSpecToSheaf.map (tilde.map f)).hom.app (op U) = f ≫ toOpen N U

Tactic:
ext x; exact Subtype.ext (funext fun y ↦ IsLocalizedModule.map_apply y.1.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl M)
     (LocalizedModule.mkLinearMap y.1.asIdeal.primeCompl N) _ x)

Goal state after: