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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : IsAffineHom f₁
this✝ : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯ =
    (normalization f).presheaf.map (eqToHom h₂').op ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op
⊢ Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯) ≫ ⋯.fromSpec ≫ f₂ =
    Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₂

Tactic:
this,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝² : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝¹ : IsAffineHom f₁
this✝ : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯ =
    (normalization f).presheaf.map (eqToHom h₂').op ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op
⊢ Spec.map
        ((normalization f).presheaf.map (eqToHom h₂').op ≫
          app (toNormalization f) (fromNormalization f ⁻¹ᵁ ↑U) ≫ X.presheaf.map (eqToHom h₃).op) ≫
      ⋯.fromSpec ≫ f₂ =
    Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₂
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: 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
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod
⊢ (map (algebraMap R L) f).coeff f.natDegree ^ (n - g.natDegree) *
      (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    (algebraMap R L) (Multiset.map (fun x ↦ eval x g) f.roots).prod

Tactic:
this,

Goal state after:
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
hgm : g.Monic
inst : Field R := hR.toField
L : Type u_1 := g.SplittingField
this :
  (map (algebraMap R L) f).resultant (map (algebraMap R L) g) f.natDegree g.natDegree =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod
⊢ (map (algebraMap R L) f).coeff f.natDegree ^ (n - g.natDegree) *
      (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap R L) f).roots ×ˢ (map (algebraMap R L) g).roots)).prod =
    (algebraMap R L) (Multiset.map (fun x ↦ eval x g) f.roots).prod
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 *
      (f.scaleRoots g.leadingCoeff).resultant g.integralNormalization f.natDegree g.natDegree =
    g.leadingCoeff ^ f.natDegree * (g.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)

Tactic:
this,

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.leadingCoeff ^ (f.natDegree * (g.natDegree - 1)) * f.resultant g)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this : IsUnit ((C f.leadingCoeff⁻¹ * f).resultant g) ↔ IsCoprime (C f.leadingCoeff⁻¹ * f) g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
rw [resultant_C_mul_left, IsUnit.mul_iff, natDegree_C_mul (by simp [hf]),
    isCoprime_mul_unit_left_left (isUnit_C.mpr (by simp [hf]))] at this

Goal state after:
case inr
K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this : IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime f g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this✝ : MonObj X := ⋯
this : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
⊢ autoParam ((β_ X X).hom ≫ μ = μ) mul_comm._autoParam

Tactic:
this,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
F : Cᵒᵖ ⥤ CommMonCat
α : (F ⋙ forget CommMonCat).RepresentableBy X
this✝ : MonObj X := MonObj.ofRepresentableBy X (F ⋙ forget₂ CommMonCat MonCat) α
this : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))
⊢ autoParam
    ((β_ X X).hom ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)))
    mul_comm._autoParam
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
⊢ IsLocallyClosed
    (⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point})

Tactic:
rw [Set.sdiff_eq_compl_inter, ← Set.image_singleton, ← Set.image_singleton]

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
⊢ IsLocallyClosed
    ((⇑(Over.Hom.left γ) ⁻¹' ⇑(Over.Hom.left (lift η η)) '' {point})ᶜ ∩
      ⇑(Over.Hom.left (fst G G)) ⁻¹' ⇑(Over.Hom.left η) '' {point})
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: case refine_3.refine_1
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)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
hy : IsClosed {y}
hx : IsClosed {(Over.Hom.left (fst G G)) y}
x : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ G := Over.homMk (pointOfClosedPoint G.hom ((Over.Hom.left (fst G G)) y) hx) ⋯
xe : ↥(G ⊗ G).left := (Over.Hom.left (fst G G ≫ (ρ_ G).inv ≫ G ◁ η)) y
⊢ xe ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left (fst G G)) y}

Tactic:
simp [xe, ← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base]

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

Goal state before:
pp: case e'_3
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)
H : ∀ (x : ↥U), (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑x} ∩ Set.range ⇑(Over.Hom.left γ)).Finite
y : ↥(G ⊗ G).left
hyU : y ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U)
hy : IsClosed {y}
hx : IsClosed {(Over.Hom.left (fst G G)) y}
x : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ G := Over.homMk (pointOfClosedPoint G.hom ((Over.Hom.left (fst G G)) y) hx) ⋯
xe : ↥(G ⊗ G).left := (Over.Hom.left (fst G G ≫ (ρ_ G).inv ≫ G ◁ η)) y
this : (Over.Hom.left γ) y = xe
⊢ (Over.Hom.left (toUnit (G ⊗ G) ≫ η)) y = (Over.Hom.left (snd G G)) xe

Tactic:
simp [xe, ← Scheme.Hom.comp_apply, -Scheme.Hom.comp_base]

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

Goal state before:
pp: K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
⊢ IsCommMonObj G

Tactic:
let f := Spec.map (CommRingCat.ofHom <| algebraMap K (AlgebraicClosure K))

Goal state after:
K : Type u
inst✝³ : Field K
G : Over (Spec (CommRingCat.of K))
inst✝² : IsProper G.hom
inst✝¹ : GeometricallyIntegral G.hom
inst✝ : GrpObj G
f : Spec (CommRingCat.of (AlgebraicClosure K)) ⟶ Spec (CommRingCat.of K) :=
  Spec.map (CommRingCat.ofHom (algebraMap K (AlgebraicClosure K)))
⊢ IsCommMonObj G
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : adjoin T ↑s = ⊤
⊢ FiniteType R S

Tactic:
have (x : s) := TensorProduct.exists_sum_tmul_eq x.1

Goal state after:
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
inst✝¹ : Module.FaithfullyFlat R T
inst✝ : FiniteType T (T ⊗[R] S)
s : Finset (T ⊗[R] S)
hs : adjoin T ↑s = ⊤
this : ∀ (x : ↥s), ∃ k m n, ↑x = ∑ j, m j ⊗ₜ[R] n j
⊢ FiniteType R S
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
this : ∀ (x : ↥X), f x = y → Scheme.Hom.QuasiFiniteAt f x
⊢ y ∈ V

Tactic:
by simpa [V, not_imp_not]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this : IsProper f
⊢ UniversallyClosed (Scheme.Hom.imageι f ≫ g)

Tactic:
have : UniversallyClosed (f.toImage ≫ f.imageι ≫ g) := by
      rw [Scheme.Hom.toImage_imageι_assoc]; infer_instance

Goal state after:
X Y S : Scheme
f : X ⟶ Y
g : Y ⟶ S
s : ↥S
H : (⇑f '' ⇑(f ≫ g) ⁻¹' {s}).Finite
inst✝² : IsProper (f ≫ g)
inst✝¹ : IsSeparated g
inst✝ : LocallyOfFiniteType g
this✝ : IsProper f
this : UniversallyClosed (Scheme.Hom.toImage f ≫ Scheme.Hom.imageι f ≫ g)
⊢ UniversallyClosed (Scheme.Hom.imageι f ≫ g)
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
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective ⇑(f ∘ₗ tensorCotangentHom R T I)

Tactic:
this,

Goal state after:
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
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
this : f ∘ₗ tensorCotangentHom R T I = hₐ.toLinearMap ∘ₗ g
⊢ Function.Injective ⇑(hₐ.toLinearMap ∘ₗ g)
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes

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

Tactic:
by
  simp [ih_η, ih_θ]

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

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
dsimp only [compUnit, compCounit]; bicategory

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

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

Tactic:
dsimp only [compUnit, compCounit]; bicategory

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
this : Submodule.map ((mul R R) a) I = a • I
⊢ Submodule.map (Submodule.mkQ (a • I)) (Submodule.map ((mul R R) a) I) = ⊥

Tactic:
this,

Goal state after:
case a
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
ha : a ∈ nonZeroDivisors R
this : Submodule.map ((mul R R) a) I = a • I
⊢ Submodule.map (Submodule.mkQ (a • I)) (a • I) = ⊥
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]

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ Module.length R (R ⧸ span {0}) = Module.length R R
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a x : R
⊢ ord R x ≤ ord R (a * x)

Tactic:
simp only [ord]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a x : R
⊢ Module.length R (R ⧸ span {x}) ≤ Module.length R (R ⧸ span {a * x})
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso (Scheme.Hom.coborderRange g).ι

Tactic:
this,

Goal state after:
ι : Type u
R : ι → CommRingCat
V : Scheme
f : (∐ fun i ↦ Spec (R i)) ⟶ V
g : V ⟶ Spec (CommRingCat.of ((i : ι) → ↑(R i)))
inst✝¹ : IsImmersion g
inst✝ : CompactSpace ↥V
hU' : f ≫ g = sigmaSpec R
this : Scheme.Hom.coborderRange g = ⊤
⊢ IsIso ⊤.ι
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ 𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁ = 𝟙 r₁

Tactic:
by
      rw [adj₁.right_triangle]
      bicategory

Goal state after:
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' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ (Spec.map (CommRingCat.ofHom ((Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom)) ≫
      inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀) =
    f i

Tactic:
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₀) (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' := ⋯ }
i : ι
this :
  (Pi.evalRingHom (fun x ↦ ↑(R x)) i).comp e.symm.toRingHom =
    (Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i))
⊢ (Spec.map
        (CommRingCat.ofHom
          ((Pi.evalRingHom (fun i_1 ↦ ↑(R ↑i_1)) ⟨i, ⋯⟩).comp (Pi.evalRingHom (fun x ↦ ↑(R' x)) (j i)))) ≫
      inv (sigmaSpec R') ≫ Sigma.desc fun j₀ ↦ g j₀ ≫ 𝒰.f j₀) =
    f i
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h_open
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
r : A
⊢ IsOpen ((fun r ↦ ↑(basicOpen 𝒜 r)) r)

Tactic:
exact isOpen_basicOpen 𝒜

Goal state after: