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

Goal state before:
pp: case a.convert_2.add
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
p q : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R)
a✝¹ :
  p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f p)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
a✝ :
  q - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f q)) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
⊢ p + q - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f (p + q))) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
simp only [map_add, add_sub_add_comm]; exact add_mem ‹_› ‹_›

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

Goal state before:
pp: case a.convert_2.C.add
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
f : MvPolynomial (Fin m ⊕ Fin k) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  eval₂Hom (↑(universalFactorizationMap R n m k hn)) (Sum.elim (fun x ↦ X x ⊗ₜ[R] 1) fun x ↦ 1 ⊗ₜ[R] X x)
H : ∀ (i : Fin m ⊕ Fin k), (tensorEquivSum R (Fin m) (Fin k) R) (f (X i)) = X i
p q : MvPolynomial (Fin n) R
a✝¹ :
  C p - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f (C p))) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
a✝ :
  C q - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f (C q))) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))
⊢ C (p + q) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) (f (C (p + q)))) ∈
    Ideal.span
      (Set.range fun i ↦
        C (X i) - (map C) ((tensorEquivSum R (Fin m) (Fin k) R) ((universalFactorizationMap R n m k hn) (X i))))

Tactic:
simp only [map_add, add_sub_add_comm]; exact add_mem ‹_› ‹_›

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
⊢ (universalFactorizationMap R n m k hn).Finite

Tactic:
refine RingHom.IsIntegral.to_finite ?_
    (.of_finitePresentation (finitePresentation_universalFactorizationMap R n m k hn))

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
⊢ (universalFactorizationMap R n m k hn).IsIntegral
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case tmul.refine_1.C
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
this✝¹ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (universalFactorizationMap R n m k hn).toAlgebra
this✝ : IsDomain (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ)
this : Algebra (MvPolynomial (Fin n) ℤ) (MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ) :=
  (universalFactorizationMap ℤ n m k hn).toAlgebra
F : MvPolynomial (Fin m) ℤ ⊗[ℤ] MvPolynomial (Fin k) ℤ →ₐ[ℤ] MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R :=
  Algebra.TensorProduct.lift (Algebra.TensorProduct.includeLeft.comp (mapAlgHom (Algebra.ofId ℤ R)))
    ((AlgHom.restrictScalars ℤ Algebra.TensorProduct.includeRight).comp (mapAlgHom (Algebra.ofId ℤ R))) ⋯
H₁ : ∀ (i : Fin m), (universalFactorizationMap R n m k hn).IsIntegralElem (X i ⊗ₜ[R] 1)
H₂ : ∀ (i : Fin k), (universalFactorizationMap R n m k hn).IsIntegralElem (1 ⊗ₜ[R] X i)
y : MvPolynomial (Fin k) R
a : R
⊢ (universalFactorizationMap R n m k hn).IsIntegralElem (C a ⊗ₜ[R] 1)

Tactic:
simpa using! (universalFactorizationMap R n m k hn).isIntegralElem_map (x := .C a)

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

Goal state before:
pp: case Splits.mem
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
g : R[X]
r : R
x : R[X]
h : x ∈ {x | ∃ a, C a = x} ∪ {x | ∃ a, X + C a = x}
⊢ ((taylor r) x).resultant ((taylor r) g) = x.resultant g

Tactic:
obtain (⟨s, rfl⟩ | ⟨s, rfl⟩) := h
      · rw [taylor_C]; simp
      · nontriviality R
        rw [map_add, taylor_X, taylor_C, add_assoc, ← map_add]
        simp [-map_add, taylor_eval]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.degree = 2
⊢ f.discr = f.coeff 1 ^ 2 - 4 * f.coeff 0 * f.coeff 2

Tactic:
rw [← Nat.cast_two, degree_eq_iff_natDegree_eq_of_pos two_pos] at hf
  let e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 3 := finCongr (by lia)
  rw [discr, ← Matrix.det_reindex_self e]
  have : f.sylvesterDeriv.reindex e e =
    !![f.coeff 0,     f.coeff 1,         0;
        f.coeff 1, 2 * f.coeff 2, f.coeff 1;
        1,                     0,         2] := by
    ext i j
    fin_cases i <;> fin_cases j <;>
      simp [e, sylvesterDeriv, sylvester, coeff_derivative, mul_comm, Fin.addCases,
        one_add_one_eq_two, hf, Fin.cast]
  simp only [this, Matrix.det_fin_three, Matrix.of_apply, Matrix.cons_val', Matrix.cons_val_zero,
    Matrix.cons_val_fin_one, Matrix.cons_val_one, Matrix.cons_val, hf]
  ring_nf

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

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H :
  (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c₀ : ↥(G ⊗ G).left
hc₃ : c₀ ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c₀ ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c₀ ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
c : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left
hc : c ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K))
e : (pointEquivClosedPoint (G ⊗ G).hom) ⟨c, hc⟩ = ⟨c₀, hc₃⟩
⊢ False

Tactic:
obtain rfl : c point = c₀ := congr(($e).1)

Goal state after:
K : Type u
inst✝⁴ : Field K
inst✝³ : IsAlgClosed K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : IsIntegral (G ⊗ G).left
inst✝ : GrpObj G
S : Scheme := Spec (CommRingCat.of K)
point : ↥S := IsLocalRing.closedPoint K
hpoint : IsClosed {point}
this✝⁹ : Nonempty ↥G.left
this✝⁸ : IsProper (G ⊗ G).hom
this✝⁷ : JacobsonSpace ↥(G ⊗ G).left
this✝⁶ : Surjective G.hom
this✝⁵ : IsProper (Over.Hom.left (fst G G))
this✝⁴ : Surjective (Over.Hom.left (fst G G))
this✝³ : IsProper (Over.Hom.left (GrpObj.commutator G) ≫ G.hom)
this✝² : IsClosedImmersion (Over.Hom.left (lift η η) ≫ Over.Hom.left (fst G G))
this✝¹ : IsClosedImmersion (Over.Hom.left (lift η η))
γ : G ⊗ G ⟶ G ⊗ G := lift (fst G G) (GrpObj.commutator G)
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
H :
  (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
c : Spec (CommRingCat.of K) ⟶ (G ⊗ G).left
hc : c ≫ (G ⊗ G).hom = 𝟙 (Spec (CommRingCat.of K))
hc₃ : c point ∈ closedPoints ↥(G ⊗ G).left
hc₁ : c point ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point}
hc₂ : c point ∉ ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}
e : (pointEquivClosedPoint (G ⊗ G).hom) ⟨c, hc⟩ = ⟨c point, hc₃⟩
⊢ False
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV✝ : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
this✝¹ : IsIso (toNormalization f ∣_ ⨆ x, V x)
x : ↥X
y : ↑{x | QuasiFiniteAt f x}
hxVy : (toNormalization f) x ∈ V y
U : Y.Opens
r : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
hU : IsAffineOpen U
hr : IsAffineOpen (toNormalization f ⁻¹ᵁ (normalization f).basicOpen r)
hxV : x ∈ toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
hrV : (normalization f).basicOpen r ≤ V y
W : X.Opens := toNormalization f ⁻¹ᵁ (normalization f).basicOpen r
H : W ≤ f ⁻¹ᵁ U
H' :
  appLE (fromNormalization f) U ((normalization f).basicOpen r) ⋯ ≫
      app (toNormalization f) ((normalization f).basicOpen r) =
    appLE f U W H
this✝ : IsIso (app (toNormalization f) ((normalization f).basicOpen r))
this : (CommRingCat.Hom.hom (appLE f U W H)).QuasiFinite
⊢ f x = (fromNormalization f) ((toNormalization f) x)

Tactic:
rw [← Scheme.Hom.comp_apply, f.toNormalization_fromNormalization]

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

Goal state before:
pp: case e_a.h₀
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ ((map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
          map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
        (pullbackSpecIso R S S).inv) ≫
      pullback.fst (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))
        (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯ ≫
      pullback.fst (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))
        (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))

Tactic:
· simp only [specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
      ← AlgHom.comp_toRingHom, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd,
      limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
      congr 3
      ext; simp

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

Goal state before:
pp: case h₁
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ ((map (CommRingCat.ofHom ↑(Algebra.TensorProduct.lmul' R)) ≫
          map (CommRingCat.ofHom ↑(Algebra.TensorProduct.map f.ofConv g.ofConv))) ≫
        (pullbackSpecIso R S S).inv) ≫
      pullback.snd (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))
        (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R)) =
    pullback.lift (map (CommRingCat.ofHom ↑f.ofConv)) (map (CommRingCat.ofHom ↑g.ofConv)) ⋯ ≫
      pullback.snd (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))
        (Spec (CommRingCat.of S) ↘ Spec (CommRingCat.of R))

Tactic:
· simp only [specOverSpec_over, ← Spec.map_comp, ← CommRingCat.ofHom_comp,
      ← AlgHom.comp_toRingHom, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd,
      limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
      congr 3
      ext; simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FinitePresentation R S
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Module.Free R S'
w✝ : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ (RingHom.ker f.toRingHom).FG

Tactic:
apply Submodule.FG.of_restrictScalars R

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FinitePresentation R S
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Module.Free R S'
w✝ : FinitePresentation R S'
f : S' →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ (Submodule.restrictScalars R (RingHom.ker f.toRingHom)).FG
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (pullback.snd f g) y

Tactic:
rw [hzr.symm]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : IsFinite f
x : ↥X
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X), (∃ R, Y = Spec R) → 1 ≤ finrank f (f x)
hY : ¬∃ R, Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : g y = f x
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (pullback.snd f g) ((pullback.snd f g) z)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

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

Tactic:
have _ : IsAffine X := isAffine_of_isAffineHom f

Goal state after:
case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
this :
  ∀ {X : Scheme} (x : ↥X) (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    (∃ S, X = Spec S) → 1 ≤ finrank f (f x)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ 1 ≤ finrank f (f x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
⊢ Surjective f

Tactic:
have _ : IsAffine X := isAffine_of_isAffineHom f

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ Surjective f
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ S, X = Spec S) → IsLocallyConstant (finrank f)
hX : ¬∃ S, X = Spec S
⊢ IsLocallyConstant (finrank f)

Tactic:
have _ : IsAffine X := isAffine_of_isAffineHom f

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ S, X = Spec S) → IsLocallyConstant (finrank f)
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ IsLocallyConstant (finrank f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
⊢ IsIso f

Tactic:
have _ : IsAffine X := isAffine_of_isAffineHom f

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
x✝ : IsAffine X
⊢ IsIso f
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hb : b ∈ nonZeroDivisors R
this : Module.length R (R ⧸ b • span {a}) = Module.length R (R ⧸ span {a}) + Module.length R (R ⧸ span {b})
⊢ {b} • span {a} = span {b * a}

Tactic:
simp [← Ideal.submodule_span_eq, Submodule.set_smul_span]

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✝³ : AddSubgroupClass σ A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
c3 c4 : NumDenSameDeg 𝒜 x
h' : Localization.mk ↑c3.num ⟨↑c3.den, ⋯⟩ = Localization.mk ↑c4.num ⟨↑c4.den, ⋯⟩
⊢ c1 * c3 ≈ c2 * c4

Tactic:
change Localization.mk _ _ = Localization.mk _ _
      simp only [num_mul, den_mul]
      convert! congr_arg₂ (· * ·) h h' <;> rw [Localization.mk_mul] <;> rfl

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

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

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (∀ (x : ValuativeCommSq f), Nonempty ⋯.LiftStruct ∧ Subsingleton ⋯.LiftStruct) ↔
    ∀ (x : ValuativeCommSq f), ⋯.HasLift ∧ Subsingleton ⋯.LiftStruct

Tactic:
CommSq.HasLift.iff

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
K : ℕ
hK :
  ∀ (i j : ι),
    (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t i) =
      (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ K • t j)
i : ι
⊢ basicOpen (g i) ≤ V

Tactic:
by rw [hg]; exact le_iSup_of_le _ le_rfl

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

Goal state before:
pp: case neg
σ : 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
⊢ ∃ a_1,
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯) a_1 =
      HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }

Tactic:
have : n = j * (d + e) := by
    apply DirectSum.degree_eq_of_mem_mem 𝒜 hb'
    · convert! SetLike.pow_mem_graded _ _ using 2
      · infer_instance
      · exact hx ▸ SetLike.mul_mem_graded hf hg
    · exact hx ▸ hfg

Goal state after:
case neg
σ : 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
this : n = j * (d + e)
⊢ ∃ a_1,
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯) a_1 =
      HomogeneousLocalization.mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x_1 ↦ x ^ x_1) j, hb'⟩, den_mem := ⋯ }
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 𝒜
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
this : n = j * (d + e)
⊢ f ^ (j * (e + 1)) ∈ 𝒜 (j * (d * (e + 1)))

Tactic:
by convert SetLike.pow_mem_graded _ hf; ring

Goal state after:
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 𝒜
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
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)), num := ⟨a * g ^ (j * (d - 1)), ⋯⟩, den := ⟨f ^ (j * (e + 1)), ⋯⟩, den_mem := ⋯ }
⊢ f ^ (j * e) ∈ 𝒜 (j * (d * e))

Tactic:
by convert SetLike.pow_mem_graded _ hf; ring

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
⊢ Spec.map (CommRingCat.ofHom (algebraMap S'.R S'.K)) ≫ S.i₂ ≫ pullback.fst f f = S'.i₁

Tactic:
by simp [S', ← S.commSq.w_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
⊢ Spec.map (CommRingCat.ofHom (algebraMap S'.R S'.K)) ≫ S.i₂ ≫ pullback.snd f f = S'.i₁

Tactic:
by simp [S', ← S.commSq.w_assoc]

Goal state after: