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

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
⊢ CreatesColimit F (MorphismProperty.Over.forget P ⊤ S)

Tactic:
have : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S) :=
    hasColimit_of_created _ (Over.forget S)
  refine createsColimitOfFullyFaithfulOfIso
      { toComma := colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
        prop := ?_ } (Iso.refl _)
  let e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
      colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
    preservesColimitIso (Over.forget S) _
  let 𝒰 : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left.OpenCover :=
    (Scheme.IsLocallyDirected.openCover _).pushforwardIso e.inv
  rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) 𝒰]
  intro i
  simpa [𝒰, e] using! (F.obj i).prop

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:
pullbackSymmetry_hom_comp_snd

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 ≫ pullback.fst (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ 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.CategoryTheory.Bicategory.Adjunction.Cat

Goal state before:
pp: C D E : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
F' : D ⟶ E
G' : E ⟶ D
adj' : F' ⊣ G'
⊢ Adjunction.ofCat (adj.comp adj') = (Adjunction.ofCat adj).comp (Adjunction.ofCat adj')

Tactic:
ext
  simp [bicategoricalComp]

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mp
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H :
  ∀ x ∈ U.overEquivalence.functor.obj V,
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
⊢ S ∈ ((Opens.grothendieckTopology X).over U) V

Tactic:
x

Goal state after:
case mp
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H :
  ∀ x ∈ U.overEquivalence.functor.obj V,
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
x : X
⊢ x ∈ V.left → ∃ U_1 f, ((Sieve.overEquiv V) S).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H : S ∈ ((Opens.grothendieckTopology X).over U) V
⊢ ∀ x ∈ U.overEquivalence.functor.obj V,
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1

Tactic:
x

Goal state after:
case mpr
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
S : Sieve V
H : S ∈ ((Opens.grothendieckTopology X).over U) V
x : ↥U
⊢ x ∈ U.overEquivalence.functor.obj V →
    ∃ V_1 f, S.arrows (U.overEquivalence.inverse.map f ≫ U.overEquivalence.unitInv.app V) ∧ x ∈ V_1
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) = γ

Tactic:
rw [adj.left_triangle]
        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
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α = α

Tactic:
rw [adj.left_triangle]
        bicategory

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
⊢ rankAtStalk S = 1 ↔ Function.Injective ⇑(algebraMap R S) ∧ Function.Surjective ⇑(algebraMap R S)

Tactic:
← rankAtStalk_pos_iff_algebraMap_injective,

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
⊢ rankAtStalk S = 1 ↔ (∀ (p : PrimeSpectrum R), 0 < rankAtStalk S p) ∧ Function.Surjective ⇑(algebraMap R S)
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: case neg
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
a : K
ha : ¬a = 0
⊢ (ordFrac R) a =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      a

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := R) a

Goal state after:
case neg
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 : R
hy : y ∈ nonZeroDivisors R
ha : ¬(algebraMap R K) x / (algebraMap R K) y = 0
⊢ (ordFrac R) ((algebraMap R K) x / (algebraMap R K) y) =
    (MonoidWithZero.inverse.comp
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom)
      ((algebraMap R K) x / (algebraMap R K) y)
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)))
this : ∀ (j₀ : 𝒰.I₀), ∃ a, pointsPi (fun x ↦ R ↑x) (𝒰.X j₀) a = fun i ↦ IsOpenImmersion.lift (𝒰.f j₀) (f ↑i) ⋯
⊢ ∃ a, pointsPi R X a = f

Tactic:
choose g hg using this

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₀), pointsPi (fun x ↦ R ↑x) (𝒰.X j₀) (g j₀) = fun i ↦ IsOpenImmersion.lift (𝒰.f j₀) (f ↑i) ⋯
⊢ ∃ a, pointsPi R X a = f
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' := ⋯ }
⊢ ∃ a, pointsPi R X a = f

Tactic:
refine ⟨Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫
    Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀, ?_⟩

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' := ⋯ }
⊢ pointsPi R X
      (Spec.map (CommRingCat.ofHom e.symm.toRingHom) ≫ inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀) =
    f
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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t))).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal

Tactic:
rw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (closure t) = vanishingIdeal t

Tactic:
by
  have : (vanishingIdeal (zeroLocus 𝒜 (vanishingIdeal t))).toIdeal = _ := (gc_ideal 𝒜).u_l_u_eq_u t
  ext1
  rw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this
  exact this

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)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x ↦ (a * b) (i x)

Tactic:
rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩
  rcases hb x with ⟨Vb, mb, ib, jb, ⟨rb, rb_mem⟩, ⟨sb, sb_mem⟩, hwb, wb⟩
  refine
    ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ja + jb,
      ⟨ra * rb, SetLike.mul_mem_graded ra_mem rb_mem⟩,
      ⟨sa * sb, SetLike.mul_mem_graded sa_mem sb_mem⟩, fun y =>
      y.1.asHomogeneousIdeal.toIdeal.primeCompl.mul_mem (hwa ⟨y.1, y.2.1⟩) (hwb ⟨y.1, y.2.2⟩), ?_⟩
  rintro ⟨y, hy⟩
  simp only [Subtype.forall, Opens.apply_mk] at wa wb
  simp [wa y hy.1, wb y hy.2, ext_iff_val, Localization.mk_mul]

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

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
⊢ ↑(GradedMonoid.GMonoid.gnpow n c.den) ∈ x

Tactic:
by
        induction n with
        | zero => simp only [coe_gnpow, pow_zero, one_mem]
        | succ n ih => simpa only [pow_succ, coe_gnpow] using x.mul_mem ih c.den_mem

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

Goal state before:
pp: case exists_of_eq
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
a b : Away 𝒜 f
⊢ (algebraMap (Away 𝒜 f) (Away 𝒜 x)) a = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) b → ∃ c, ↑c * a = ↑c * b

Tactic:
e

Goal state after:
case exists_of_eq
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
a b : Away 𝒜 f
e : (algebraMap (Away 𝒜 f) (Away 𝒜 x)) a = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) b
⊢ ∃ c, ↑c * a = ↑c * b
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case exists_of_eq
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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e : (algebraMap (Away 𝒜 f) (Away 𝒜 x)) (Away.mk 𝒜 hf n a ha) = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) (Away.mk 𝒜 hf m b hb)
⊢ ∃ c, ↑c * Away.mk 𝒜 hf n a ha = ↑c * Away.mk 𝒜 hf m b hb

Tactic:
replace e := congr_arg val e

Goal state after:
case exists_of_eq
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 : ℕ
a : A
ha : a ∈ 𝒜 (n • d)
m : ℕ
b : A
hb : b ∈ 𝒜 (m • d)
e :
  val ((algebraMap (Away 𝒜 f) (Away 𝒜 x)) (Away.mk 𝒜 hf n a ha)) =
    val ((algebraMap (Away 𝒜 f) (Away 𝒜 x)) (Away.mk 𝒜 hf m b hb))
⊢ ∃ c, ↑c * Away.mk 𝒜 hf n a ha = ↑c * Away.mk 𝒜 hf m b hb
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg
ι : 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
⊢ ⊤ ≤ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
rintro x -

Goal state after:
case neg
ι : 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 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
x : Away 𝒜 f
⊢ x ∈ Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case pos.e_a.e_x
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 : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + m - j) =
    ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m - j + m)

Tactic:
add_comm (m - j),

Goal state after:
case pos.e_a.e_x
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 : ℕ
g : ℕ → A⁰_ f :=
  fun j ↦
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + m - j) =
    ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + (m - j))
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x y : Localization.AtPrime P
⊢ (IsLocalization.liftAlgHom ⋯) x = (IsLocalization.liftAlgHom ⋯) y → x = y

Tactic:
e

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x y : Localization.AtPrime P
e : (IsLocalization.liftAlgHom ⋯) x = (IsLocalization.liftAlgHom ⋯) y
⊢ x = y
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
s : Finset ι' := {x | 0 < dv x}
⊢ ∀ (i : ↥s), 0 < (dv ∘ Subtype.val) i

Tactic:
by simp [s]

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

Goal state before:
pp: case refine_1
K : Type u_3
inst✝ : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
a : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
⊢ ⟨a, ha⟩ + ⟨b, hb⟩ = 1 → IsUnit ⟨a, ha⟩ ∨ IsUnit ⟨b, hb⟩

Tactic:
e

Goal state after:
case refine_1
K : Type u_3
inst✝ : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
a : K
ha : a ∈ ⨆ i, (↑i).toSubring
b : K
hb : b ∈ ⨆ i, (↑i).toSubring
e : ⟨a, ha⟩ + ⟨b, hb⟩ = 1
⊢ IsUnit ⟨a, ha⟩ ∨ IsUnit ⟨b, hb⟩
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: case refine_1
K : Type u_3
inst✝ : Field K
A : LocalSubring K
s : Set (LocalSubring K)
hs : s ⊆ Set.Ici A
H : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
y : LocalSubring K
hys : y ∈ s
inst : Nonempty ↑s
hdir : Directed LE.le (toSubring ∘ fun x ↦ ↑x)
⊢ ∀ {a b : ↥(⨆ i, (↑i).toSubring)}, a + b = 1 → IsUnit a ∨ IsUnit b

Tactic:
intro ⟨a, ha⟩ ⟨b, hb⟩ e
    obtain ⟨A, haA : a ∈ A.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp ha
    obtain ⟨B, hbB : b ∈ B.1.toSubring⟩ := (Subring.mem_iSup_of_directed hdir).mp hb
    obtain ⟨C, hCA, hCB⟩ := hdir A B
    refine (C.1.2.2 (a := ⟨a, hCA haA⟩) (b := ⟨b, hCB hbB⟩) (Subtype.ext congr(($e).1))).imp ?_ ?_
    · exact fun h ↦ h.map (Subring.inclusion (le_iSup (fun i : s ↦ i.1.toSubring) C))
    · exact fun h ↦ h.map (Subring.inclusion (le_iSup (fun i : s ↦ i.1.toSubring) C))

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

Goal state before:
pp: case exists_of_eq
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 z : A⁰_ f
⊢ (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) y =
      (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) z →
    ∃ c, ↑c * y = ↑c * z

Tactic:
e

Goal state after:
case exists_of_eq
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 z : A⁰_ f
e :
  (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) y =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) z
⊢ ∃ c, ↑c * y = ↑c * z