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

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this✝ :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
this :
  (Multiset.map (fun x ↦ eval x f) g.roots).prod =
    (f %ₘ g).leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x r) g.roots).prod
⊢ (-1) ^ (g.natDegree * (f.natDegree - r.natDegree)) *
      ((-1) ^ (r.natDegree * g.natDegree) *
        ((algebraMap K L) (f %ₘ g).leadingCoeff ^ g.natDegree *
          (Multiset.map (fun x ↦ (aeval ((algebraMap K L) x)) r) g.roots).prod)) =
    (-1) ^ (g.natDegree * f.natDegree) *
      ((algebraMap K L) (f %ₘ g).leadingCoeff ^ g.natDegree *
        (Multiset.map (fun x ↦ (algebraMap K L) (eval x r)) g.roots).prod)

Tactic:
simp only [← mul_assoc, ← pow_add, ← add_mul, Nat.sub_add_cancel (hrd.le.trans hfg),
      mul_comm g.natDegree]

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this✝ :
  (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (algebraMap K L) ((f %ₘ g).leadingCoeff ^ g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
this :
  (Multiset.map (fun x ↦ eval x f) g.roots).prod =
    (f %ₘ g).leadingCoeff ^ g.natDegree * (Multiset.map (fun x ↦ eval x r) g.roots).prod
⊢ (-1) ^ (f.natDegree * g.natDegree) * (algebraMap K L) (f %ₘ g).leadingCoeff ^ g.natDegree *
      (Multiset.map (fun x ↦ (aeval ((algebraMap K L) x)) r) g.roots).prod =
    (-1) ^ (f.natDegree * g.natDegree) * (algebraMap K L) (f %ₘ g).leadingCoeff ^ g.natDegree *
      (Multiset.map (fun x ↦ (algebraMap K L) (eval x r)) g.roots).prod
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  (g.leadingCoeff ^ f.natDegree)⁻¹ * f.resultant g f.natDegree n =
    (Multiset.map (fun x ↦ eval x (C g.leadingCoeff⁻¹ * g)) f.roots).prod
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
inv_mul_eq_iff_eq_mul₀ (by simp [hg0])

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
n : ℕ
hg : g.natDegree ≤ n
hf : f.Splits
hR : IsField R
hfm : f.Monic
hg0 : ¬g = 0
this✝ :
  ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : R[X]) (n : ℕ),
    g.natDegree ≤ n →
      f.Splits →
        IsField R →
          f.Monic → ¬g = 0 → g.Monic → f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
hgm : ¬g.Monic
inst : Field R := hR.toField
this :
  f.resultant g f.natDegree n =
    g.leadingCoeff ^ f.natDegree * (Multiset.map (fun x ↦ eval x (C g.leadingCoeff⁻¹ * g)) f.roots).prod
⊢ f.resultant g f.natDegree n = (Multiset.map (fun x ↦ eval x g) f.roots).prod
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑j < ↑i
⊢ ∀ (a b : ℕ),
    a + b = ↑j →
      (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0
        else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) =
        0

Tactic:
intro a b hab

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
i : Fin m
j : Fin n
h : ↑j < ↑i
a b : ℕ
hab : a + b = ↑j
⊢ (if h : b < k then if a < m ∧ a = ↑i then X (Sum.inr ⟨b, ⋯⟩) else 0 else if b = k ∧ a < m ∧ a = ↑i then 1 else 0) = 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

Tactic:
wlog hR : IsDomain R

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.natDegree ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] (f g : R[X]),
    g.natDegree ≠ 0 →
      IsDomain R →
        (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
          g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
hR : ¬IsDomain R
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g

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
⊢ (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

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
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p }
⊢ (fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩)
      ((fun q ↦
          Algebra.TensorProduct.lift (Algebra.ofId R S)
            (let __RingHom :=
              (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn (p.map (algebraMap R S))).symm
                    q)).toRingHom;
            { toRingHom := __RingHom, commutes' := ⋯ })
            ⋯)
        q) =
    q

Tactic:
let := (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
    let := ((MvPolynomial.mapEquivMonic R _ n).symm p).toAlgebra
    simp only [UniversalFactorizationRing, MvPolynomial.mapEquivMonic, AlgHom.toRingHom_eq_coe,
      Equiv.coe_fn_symm_mk, MvPolynomial.coe_aeval_eq_eval, factor₁,
      MvPolynomial.universalFactorizationMapLiftEquiv, Equiv.coe_fn_mk, fromTensor, factor₂]
    ext <;> simp +contextual [coeff_freeMonic, apply_dite, MonicDegreeEq.coeff_of_ge]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
M G H X Y : C
inst✝² : MonObj M
inst✝¹ : GrpObj G
inst✝ : GrpObj H
F : Cᵒᵖ ⥤ GrpCat
α : (F ⋙ forget GrpCat).RepresentableBy X
⊢ lift (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) (𝟙 X) ≫ μ = toUnit X ≫ η

Tactic:
change lift (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) (𝟙 X) ≫
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
        toUnit X ≫ α.homEquiv'.symm 1
    apply α.homEquiv'.injective
    simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul, map_one]
    simp only [← α.homEquiv'_comp, lift_fst, Equiv.apply_symm_apply, lift_snd]
    exact inv_mul_cancel (α.homEquiv (𝟙 X))

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 γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
          Scheme.Hom.imageι (Over.Hom.left γ)) ''
      ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
            Scheme.Hom.imageι (Over.Hom.left γ)) ⁻¹'
        ⇑(Over.Hom.left (fst G G)) ⁻¹' {↑x}

Tactic:
Set.image_preimage_eq_inter_range

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 γ) '' ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} ⊆ {(Over.Hom.left (lift η η)) point}
U : G.left.Opens
hηU : (Over.Hom.left η) point ∈ U
H : IsFinite ((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ∣_ U)
x : ↥U
this : ⇑U.ι ⁻¹' {↑x} = {x}
⊢ ⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ) ⊆
    ⇑(Over.Hom.left (fst G G)) ⁻¹' {↑x} ∩
      Set.range
        ⇑(((Scheme.Hom.imageι (Over.Hom.left γ) ≫ Over.Hom.left (fst G G)) ⁻¹ᵁ U).ι ≫
            Scheme.Hom.imageι (Over.Hom.left γ))
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
⊢ ∃ U, IsIso (toNormalization f ∣_ U) ∧ (toNormalization f ⁻¹ᵁ U).carrier = {x | QuasiFiniteAt f x}

Tactic:
choose V hxV hV using fun x : { x // f.QuasiFiniteAt x } ↦
    f.exists_mem_and_isIso_morphismRestrict_toNormalization x x.2

Goal state after:
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)
⊢ ∃ U, IsIso (toNormalization f ∣_ U) ∧ (toNormalization f ⁻¹ᵁ U).carrier = {x | QuasiFiniteAt f x}
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
W : TopologicalSpace.Opens ↥X
hW : W ∈ X.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ toNormalization f ⁻¹ᵁ V y
this : IsAffine ↑W
V' : (normalization f).Opens := opensRange (X.homOfLE hWV ≫ toNormalization f ∣_ V y ≫ (V y).ι)
hV' : IsAffineOpen V'
hV'V : V' ≤ V y
hV'W : toNormalization f ⁻¹ᵁ V' = W
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
f₁ : ↑Γ(normalization f, fromNormalization f ⁻¹ᵁ U)
f₂ : ↑Γ(normalization f, V')
e : (normalization f).basicOpen f₁ = (normalization f).basicOpen f₂
hxf : (toNormalization f) x ∈ (normalization f).basicOpen f₁
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (app (toNormalization f) V')) f₂))

Tactic:
exact IsAffineOpen.basicOpen (hV'W ▸ hW) _

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ F.comp (id C) = F

Tactic:
ext
  · simp
  all_goals
  · rw [heq_iff_eq]
    ext
    simp

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

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : StrictlyUnitaryLaxFunctor B C
⊢ (id B).comp F = F

Tactic:
ext
  · simp
  all_goals
  · rw [heq_iff_eq]
    ext
    simp

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

Goal state before:
pp: B : Type u₁
inst✝³ : Bicategory B
C : Type u₂
inst✝² : Bicategory C
D : Type u₃
inst✝¹ : Bicategory D
E : Type u₄
inst✝ : Bicategory E
F : StrictlyUnitaryLaxFunctor B C
G : StrictlyUnitaryLaxFunctor C D
H : StrictlyUnitaryLaxFunctor D E
⊢ (F.comp G).comp H = F.comp (G.comp H)

Tactic:
ext
  · simp
  all_goals
  · rw [heq_iff_eq]
    ext
    simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (α ≫ 𝟙 b).adj) (ρ_ α.l).hom = (λ_ α.r).symm.hom

Tactic:
by simpa using conjugateEquiv_comp_id_right_apply α.adj α.adj (𝟙 _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := lift U.ι f ⋯
heq : f = f' ≫ U.ι
⊢ Flat (f' ≫ U.ι)

Tactic:
rwa [← heq]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ ↑U := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
⊢ LocallyOfFinitePresentation (f' ≫ U.ι)

Tactic:
rwa [← heq]

Goal state after:
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

pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
hX : ∃ S, X = Spec S
⊢ Surjective f

Tactic:
· have _ : IsAffine X := isAffine_of_isAffineHom f
      rw [← MorphismProperty.cancel_left_of_respectsIso @Surjective X.isoSpec.inv]
      refine this _ _ (fun x ↦ ?_) ⟨_, rfl⟩
      rw [finrank_comp_left_of_isIso]
      exact h x

Goal state after:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
hX : ∃ S, X = Spec S
⊢ Surjective f
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : f = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x

Tactic:
· simp [hf]

Goal state after:
case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
inst✝ : IsDiscreteValuationRing ↑(X.presheaf.stalk x)
f g : ↑X.functionField
hfg : f + g ≠ 0
hf : ¬f = 0
⊢ min (ord f x) (ord g x) ≤ ord (f + g) x
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: case pos
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
hf : f = 0
⊢ ord f x ≤ ord (a • f) x

pp: case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
hf : ¬f = 0
⊢ ord f x ≤ ord (a • f) x

Tactic:
· simp [hf]

Goal state after:
case neg
X : Scheme
inst✝² : IsIntegral X
inst✝¹ : IsLocallyNoetherian X
x : ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
hxU : x ∈ U
a : ↑Γ(X, U)
ha : a ≠ 0
f : ↑X.functionField
hx : coheight x = 1
hf : ¬f = 0
⊢ ord f x ≤ ord (a • f) x
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 t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ r ∈ (vanishingIdeal t).toIdeal ⊔ (vanishingIdeal t').toIdeal → r ∈ vanishingIdeal (t ∩ t')

Tactic:
mem_vanishingIdeal,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
r : A
⊢ r ∈ (vanishingIdeal t).toIdeal ⊔ (vanishingIdeal t').toIdeal → ∀ x ∈ t ∩ t', r ∈ x.asHomogeneousIdeal
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 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s

Tactic:
by
  simp only [@eq_comm _ Uᶜ]; rfl

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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : x ∈ zeroLocus 𝒜 ↑(vanishingIdeal t)
t' : Set (ProjectiveSpectrum 𝒜)
ht' : IsClosed t'
ht : t ⊆ t'
⊢ ∃ s, t' = zeroLocus 𝒜 s

Tactic:
by rwa [isClosed_iff_zeroLocus] at ht'

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
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), (decompose ℬ) (f ↑(((decompose 𝒜) x) i)) =
    (map (↑f).gradedAddHom) (∑ i ∈ DFinsupp.support ((decompose 𝒜) x), (decompose 𝒜) ↑(((decompose 𝒜) x) i))

Tactic:
map_sum

Goal state after:
ι : 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
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), (decompose ℬ) (f ↑(((decompose 𝒜) x) i)) =
    ∑ x_1 ∈ DFinsupp.support ((decompose 𝒜) x), (map (↑f).gradedAddHom) ((decompose 𝒜) ↑(((decompose 𝒜) x) x_1))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case mp
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 : A
h :
  ∀ (i : ℕ),
    HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal
⊢ ∀ (i : ℕ),
    Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈ ⇑(algebraMap (A⁰_ f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}

Tactic:
i

Goal state after:
case mp
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 : A
h :
  ∀ (i : ℕ),
    HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal
i : ℕ
⊢ Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈ ⇑(algebraMap (A⁰_ f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: case mpr
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 : A
h :
  ∀ (i : ℕ),
    Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈ ⇑(algebraMap (A⁰_ f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}
⊢ ∀ (i : ℕ),
    HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal

Tactic:
i

Goal state after:
case mpr
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 : A
h :
  ∀ (i : ℕ),
    Localization.mk ((proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈ ⇑(algebraMap (A⁰_ f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}
i : ℕ
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal