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

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := X.affineCover.f i
⊢ QuasiFiniteAt f ((X.affineCover.f i) x) ↔ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩}

Tactic:
convert! this (x := x) _ (f := ι ≫ f) ⟨_, rfl⟩ using 1

Goal state after:
case e'_1
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := ⋯
⊢ QuasiFiniteAt f ((X.affineCover.f i) x) ↔ QuasiFiniteAt (ι ≫ f) x

case e'_2
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X : Scheme} {x : ↥X} (R : CommRingCat) {f : X ⟶ Spec R} [LocallyOfFiniteType f],
    (∃ S, X = Spec S) → (QuasiFiniteAt f x ↔ IsOpen {⟨x, ⋯⟩})
hX : ¬∃ S, X = Spec S
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
ι : X.affineCover.X i ⟶ X := ⋯
⊢ IsOpen {⟨(X.affineCover.f i) x, ⋯⟩} ↔ IsOpen {⟨x, ⋯⟩}
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
| x * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p

Tactic:
← num_div_denom x

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
| (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
hx : x ≠ 0
⊢ x = x⁻¹⁻¹

Tactic:
rw [inv_inv]

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Ideal.span (Set.range ![(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)]) =
    (Algebra.Generators.ofAlgHom
        ((P.lift P.x ⋯).comp
          ((↑P.equivMvPolynomialQuotient.symm).comp
            (Ideal.Quotient.mkₐ R
              (Ideal.span {(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)}))))
        ⋯).ker

Tactic:
Algebra.Generators.ker_ofAlgHom,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P✝ : StandardEtalePair R
P : StandardEtalePresentation R S
⊢ Ideal.span (Set.range ![(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)]) =
    RingHom.ker
      ((P.lift P.x ⋯).comp
          ((↑P.equivMvPolynomialQuotient.symm).comp
            (Ideal.Quotient.mkₐ R
              (Ideal.span
                {(Bivariate.equivMvPolynomial R) (C P.f), (Bivariate.equivMvPolynomial R) (Y * C P.g - 1)})))).toRingHom
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
⊢ IsIntegral R t

Tactic:
have ht't : t' * algebraMap S St t = 1 := by rw [mul_comm, IsLocalization.Away.mul_invSelf]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p r : R[X]
ht : φ.IsIntegralElem t
hpm : p.Monic
hpr : r.natDegree < p.natDegree
hp : φ p * t = φ r
St : Type u_2 := Localization.Away t
t' : St := IsLocalization.Away.invSelf t
ht't : t' * (algebraMap S St) t = 1
⊢ IsIntegral R t
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this : IsScalarTower R R[X] S
n : S → ℕ
hn : ∀ (x : S), p.leadingCoeff ^ n x • (t * x) ∈ φ.range
s : Finset S
hs : Submodule.span R[X] ↑s = ⊤
x : S
x✝ : x ∈ Submodule.span R[X] ↑s
⊢ p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range

Tactic:
induction hs.ge (Set.mem_univ x) using Submodule.span_induction with

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
⊢ Matrix.of
      (fun i j ↦
        Fin.addCases (fun j₁ ↦ if ↑i ∈ Icc (↑j₁) (↑j₁ + m) then g.coeff (↑i - ↑j₁) else 0)
          (fun j₁ ↦ if ↑i ∈ Icc (↑j₁) (↑j₁ + 0) then f.coeff (↑i - ↑j₁) else 0) j)
      i (Fin.natAdd 0 j) =
    Matrix.diagonal (fun x ↦ f.coeff 0) i (Fin.natAdd 0 j)

Tactic:
Matrix.of_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
m : ℕ
i j✝ : Fin (0 + m)
j : Fin m
⊢ Fin.addCases (fun j₁ ↦ if ↑i ∈ Icc (↑j₁) (↑j₁ + m) then g.coeff (↑i - ↑j₁) else 0)
      (fun j₁ ↦ if ↑i ∈ Icc (↑j₁) (↑j₁ + 0) then f.coeff (↑i - ↑j₁) else 0) (Fin.natAdd 0 j) =
    Matrix.diagonal (fun x ↦ f.coeff 0) i (Fin.natAdd 0 j)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
m n : ℕ
⊢ resultant 0 0 m n = 0 ^ (m + n)

Tactic:
by simp [pow_add]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ n
⊢ (-1) ^ (m * (n + k)) * g.resultant f (n + k) m = f.coeff m ^ k * f.resultant g m n

Tactic:
resultant_add_left_deg _ _ _ _ _ hg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n k : ℕ
hg : g.natDegree ≤ n
⊢ (-1) ^ (m * (n + k)) * ((-1) ^ (m * k) * f.coeff m ^ k * g.resultant f n m) = f.coeff m ^ k * f.resultant g m n
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ IsIntegralHom (normalizationDesc f f₁ f₂ H)

Tactic:
have : IsIntegralHom (f.normalizationDesc f₁ f₂ H ≫ f₂) := by
    rw [f.normalizationDesc_comp]; infer_instance
  exact .of_comp _ f₂

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : Nontrivial R
⊢ ∀ (m : ℕ), ↑n < ↑m → (freeMonic R n).coeff m = 0

Tactic:
simp +contextual [coeff_freeMonic, LT.lt.not_gt, LT.lt.ne']

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

Goal state before:
pp: case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1) + f.natDegree) * f.resultant g

Tactic:
← Nat.mul_add_one,

Goal state after:
case neg
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
hR : IsDomain R
hg0 : ¬g = 0
this :
  g.leadingCoeff ^ f.natDegree *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g
⊢ g.leadingCoeff ^ (f.natDegree * g.natDegree) * f.resultant g =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1 + 1)) * f.resultant g
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
G H : Grp C
inst✝ : IsCommMonObj H.X
f : G ⟶ H
n : ℕ
⊢ (f ^ n).hom = f.hom ^ n

Tactic:
induction n with
  | zero => simp
  | succ n hn => simp [pow_succ, hn]

Goal state after:
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
I : Ideal S
a✝ : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
x y : T ⊗[R] ↥(Submodule.restrictScalars R I)
a : T ⊗[R] I.Cotangent
ha :
  (tensorCotangentHom R T I) a =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) x, ⋯⟩
b : T ⊗[R] I.Cotangent
hb :
  (tensorCotangentHom R T I) b =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) y, ⋯⟩
⊢ (tensorCotangentHom R T I) (a + b) =
    (map Algebra.TensorProduct.includeRight.toRingHom I).toCotangent
      ⟨(LinearMap.lTensor T (Submodule.restrictScalars R I).subtype) (x + y), ⋯⟩

Tactic:
simp only [map_add, ha, hb]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: case right
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.right)))

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

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
h_η : 𝟙 a ◁ η ≪≫ η_g = η_f
h_θ : 𝟙 a ◁ θ ≪≫ η_g = η_f
⊢ η = θ

Tactic:
by
  apply Iso.ext
  calc
    η.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.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : WeaklyEtale f
⊢ WeaklyEtale (Scheme.Hom.resLE f V U e)

Tactic:
delta Scheme.Hom.resLE

Goal state after:
W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : WeaklyEtale f
⊢ WeaklyEtale (X.homOfLE e ≫ f ∣_ V)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ord R 0 = Module.length R R

Tactic:
simp only [ord]
  let m := (Submodule.quotEquivOfEqBot (Ideal.span {0} : Submodule R R) (span_singleton_zero))
  exact le_antisymm (Module.length_le_of_injective m m.injective)
      (Module.length_le_of_surjective m m.surjective)

Goal state after:
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
I : ProjectiveSpectrum 𝒜
⊢ I ∈ (zeroLocus 𝒜 {f})ᶜ ↔ f ∉ I.asHomogeneousIdeal

Tactic:
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]; rfl

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

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ ↑F ⊆ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))

Tactic:
intro s hs

Goal state after:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
hs : s ∈ ↑F
⊢ s ∈ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
⊢ ∃ s, Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ i ∈ s, SetLike.IsHomogeneousElem 𝒜 i

Tactic:
classical
  obtain ⟨F, hF⟩ := Algebra.FiniteType.out (R := 𝒜 0) (A := S)
  let ι₀ := Σ (x : F), (DirectSum.decompose 𝒜 x.1).support
  let x (i : ι₀) : S := ((DirectSum.decompose 𝒜) i.1 i.2).1
  refine ⟨Finset.univ.image x, ?_, by simpa using fun f ↦ ⟨_, (DirectSum.decompose 𝒜 f.1 f.2).2⟩⟩
  rw [← top_le_iff, ← hF, Algebra.adjoin_le_iff]
  intro s hs
  rw [← DirectSum.sum_support_decompose 𝒜 s]
  exact sum_mem fun n hn ↦ Algebra.subset_adjoin (by simpa using ⟨⟨⟨s, hs⟩, n, hn⟩, rfl⟩)

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

Goal state before:
pp: case pos
ι : 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
N : ι
s : A
hs : s ∈ 𝒜 N
n : ℕ
hn : (fun x ↦ f ^ x) n ∈ 𝒜 N
hfn : f ^ n = 0
this : Subsingleton (HomogeneousLocalization 𝒜 (Submonoid.powers f))
⊢ ∃ n_1 a,
    ∃ (ha : a ∈ 𝒜 (n_1 • d)),
      Away.mk 𝒜 hf n_1 a ha = mk { deg := N, num := ⟨s, hs⟩, den := ⟨(fun x ↦ f ^ x) n, hn⟩, den_mem := ⋯ }

Tactic:
exact ⟨0, 0, zero_mem _, Subsingleton.elim _ _⟩

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

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

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

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

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
a : A
ha : a ∈ asIdeal f_deg hm q
j : ℕ
h : ¬i = j
⊢ HomogeneousLocalization.mk
      { deg := m * j, num := ⟨(proj 𝒜 j) ↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ j, ⋯⟩, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
simpa only [proj_apply, decompose_of_mem_ne 𝒜 (SetLike.coe_mem (decompose 𝒜 a i)) h,
      zero_pow hm.ne', map_zero] using carrier.zero_mem f_deg hm q j

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

Goal state before:
pp: K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
⊢ ∃ B, A ≤ B.toSubring ∧ ⇑A.subtype '' ↑I ⊆ ↑B.nonunits

Tactic:
have ⟨V, hV⟩ := (LocalSubring.ofPrime A M).exists_le_valuationSubring

Goal state after:
K : Type u_3
inst✝ : Field K
A : Subring K
I : Ideal ↥A
hI : I ≠ ⊤
M : Ideal ↥A
hM : M.IsMaximal
le : I ≤ M
V : ValuationSubring K
hV : LocalSubring.ofPrime A M ≤ V.toLocalSubring
⊢ ∃ B, A ≤ B.toSubring ∧ ⇑A.subtype '' ↑I ⊆ ↑B.nonunits
Module: Mathlib.RingTheory.Valuation.LocalSubring

Goal state before:
pp: K : Type u_3
inst✝ : Field K
s : Set K
⊢ ⨅ V, (↑V).toSubring = ⨅ V, (↑V).toSubring

Tactic:
iInf_subtype

Goal state after:
K : Type u_3
inst✝ : Field K
s : Set K
⊢ ⨅ i, ⨅ (_ : s ⊆ ↑i.toSubring), i.toSubring =
    ⨅ i, ⨅ (_ : (integralClosure (↥(Subring.closure s)) K).toSubring ≤ i.toSubring), i.toSubring
Module: Mathlib.AlgebraicGeometry.Sites.Small

Goal state before:
pp: case mp
P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) → ∃ Y h g, Presieve.ofArrows 𝒰.X 𝒰.f g ∧ h ≫ g = f

Tactic:
rintro ⟨U, h, g, ⟨k⟩, hcomp⟩
    exact ⟨𝒰.X k, h.left, 𝒰.f k, ⟨k⟩, congrArg CommaMorphism.left hcomp⟩

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

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝¹ : P.IsStableUnderBaseChange
X : Over S
𝒰 : Cover (precoverage P) X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.I₀
h : V ⟶ 𝒰.X k
hcomp : h ≫ 𝒰.f k = f
this : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S
⊢ h ≫ ((𝒰.X k).asOver S).hom = (CategoryTheory.Over.mk (f ≫ X.hom)).hom

Tactic:
by simp [← hcomp, this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case left
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
this : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop (l ≫ g)))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))

Tactic:
Scheme.Hom.comp_appTop

Goal state after:
case left
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
this✝ : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
this : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g ≫ Scheme.Hom.appTop l))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M : (Spec (CommRingCat.of ↑R)).Modules
h : SheafOfModules.IsQuasicoherent M
⊢ (tilde.functor R).essImage M

Tactic:
exact ⟨((modulesSpecToSheaf.obj M).presheaf.obj (.op ⊤)), ⟨asIso <| M.fromTildeΓ⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨F.imageSieve h₁.q ⊓ F.imageSieve h₂.q, ⋯⟩),
    res data G₀ h₁ ≫ G₀.obj.map I.f.op = res data G₀ h₂ ≫ G₀.obj.map I.f.op

Tactic:
rintro ⟨Z₀, a, ⟨b₁, w₁⟩, ⟨b₂, w₂⟩⟩

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₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ res data G₀ h₁ ≫ G₀.obj.map { Y := Z₀, f := a, hf := ⋯ }.f.op =
    res data G₀ h₂ ≫ G₀.obj.map { Y := Z₀, f := a, hf := ⋯ }.f.op
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : SetLike σ A
inst✝⁸ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝⁷ : GradedRing 𝒜
O : Type u_3
inst✝⁶ : CommRing O
inst✝⁵ : IsDomain O
inst✝⁴ : ValuationRing O
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra O K
inst✝¹ : IsFractionRing O K
φ₀ : ↥(𝒜 0) →+* O
ι : Type u_5
inst✝ : Finite ι
x : ι → A
h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤
j : ι
φ : Away 𝒜 (x j) →+* K
hcomm : (algebraMap O K).comp φ₀ = φ.comp (fromZeroRingHom 𝒜 (Submonoid.powers (x j)))
d : ι → ℕ
hdi : ∀ (i : ι), 0 < d i
hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)
val✝ : Fintype ι
ψ : ι → ValueGroup O K := fun i ↦ (valuation O K) (φ (Away.isLocalizationElem ⋯ ⋯) ^ ∏ k ∈ Finset.univ.erase i, d k)
this✝¹ : Nonempty ι
Kmax : ValueGroup O K := (Finset.image ψ Finset.univ).max' ⋯
i₀ : ι
hi1 : ψ i₀ = Kmax
hi₀ : ∀ (j : ι), ψ j ≤ ψ i₀
hKmax : 0 < Kmax
this✝ : Algebra (Away 𝒜 (x j)) (Away 𝒜 (x j * x i₀)) := (awayMap 𝒜 ⋯ ⋯).toAlgebra
this : IsLocalization.Away (Away.isLocalizationElem ⋯ ⋯) (Away 𝒜 (x j * x i₀))
hunit : IsUnit (φ (Away.isLocalizationElem ⋯ ⋯))
φ' : Away 𝒜 (x j * x i₀) →+* K := IsLocalization.Away.lift (Away.isLocalizationElem ⋯ ⋯) hunit
hφ'1 : ∀ (s : Away 𝒜 (x j)), φ' ((awayMap 𝒜 ⋯ ⋯) s) = φ s
sx : Away 𝒜 (x i₀)
a : ℕ
ai : ι → ℕ
hai✝ : ∑ i, ai i • d i = a • d i₀
hai : ∑ x, ai x * d x = a * d i₀
H : (∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1)) ∈ 𝒜 ((a * d i₀) • d j)
⊢ (valuation O K) (φ (Away.mk 𝒜 ⋯ (a * d i₀) ((∏ i, x i ^ ai i) * x i₀ ^ (a * (d j - 1))) H)) ^ (d j * ∏ i, d i) =
    (∏ i, ψ i ^ (d i * ai i)) * ψ i₀ ^ (d i₀ * a * (d j - 1))

Tactic:
by
          simp only [ψ, ← map_pow, ← map_prod, ← map_mul]
          congr 2
          apply (show Function.Injective (algebraMap (Away 𝒜 (x j)) (Localization.Away (x j)))
            from val_injective _)
          simp only [map_pow, map_prod, map_mul]
          simp only [HomogeneousLocalization.algebraMap_apply, Away.val_mk, Localization.mk_pow,
            Localization.mk_prod, Localization.mk_mul]
          rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
          use 1
          simp only [OneMemClass.coe_one, ← pow_mul, Submonoid.coe_mul,
            SubmonoidClass.coe_finsetProd, one_mul]
          simp_rw [← mul_assoc, Finset.prod_erase_mul _ d (h := Finset.mem_univ _), mul_assoc,
            ← mul_assoc (Finset.prod ..), Finset.prod_erase_mul _ d (h := Finset.mem_univ _),
            SubmonoidClass.coe_pow, ← pow_mul, Finset.prod_pow_eq_pow_sum,
            ← pow_add, mul_pow, ← Finset.prod_pow, ← pow_mul]
          congr 3
          · simp only [mul_comm _ (∏ i, d i), mul_assoc, mul_left_comm _ (∏ i, d i),
              mul_comm (d _) (ai _), ← Finset.mul_sum, hai]
            cases h : d j
            · cases (hdi j).ne' h
            · simp; ring
          · ext i; congr 1; ring
          · ring

Goal state after: