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

Goal state before:
pp: case smul
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
a : R[X]
x : S
hx : x ∈ Submodule.span R[X] ↑s
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ a • p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range

Tactic:
Algebra.smul_def

Goal state after:
case smul
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
a : R[X]
x : S
hx : x ∈ Submodule.span R[X] ↑s
IH : p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
⊢ (algebraMap R[X] S) a * p.leadingCoeff ^ s.sup n • (t * x) ∈ φ.range
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case neg
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∉ p
⊢ ZariskisMainProperty R p

Tactic:
refine zariskisMainProperty_iff_exists_saturation_eq_top.mpr ⟨_, Hfp, isIntegral_algebraMap, ?_⟩

Goal state after:
case neg
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∉ p
⊢ (integralClosure R S).saturation (Submonoid.powers ((algebraMap R S) f.leadingCoeff)) ⋯ = ⊤
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
this : ↑(ker (toNormalization f)).support = ↑⊥.support
⊢ IsDominant (toNormalization f)

Tactic:
rw [IdealSheafData.support_bot, Scheme.Hom.support_ker, TopologicalSpace.Closeds.coe_top] at this

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
this : closure (Set.range ⇑(toNormalization f)) = Set.univ
⊢ IsDominant (toNormalization f)
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 S n
f : { f // f.comp (universalFactorizationMap R n m k hn) = (mapEquivMonic R S n).symm p }
⊢ ↑((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
            (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)).1 *
      ↑((mapEquivMonic R S m) ((↑f).comp Algebra.TensorProduct.includeLeft),
            (mapEquivMonic R S k) ((↑f).comp Algebra.TensorProduct.includeRight)).2 =
    ↑p

Tactic:
conv_rhs => rw [← (Equiv.eq_symm_apply _).mp f.2]
      simp [MvPolynomial.coe_mapEquivMonic_comp, MvPolynomial.universalFactorizationMap]

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

Goal state before:
pp: case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R SatisfiesM : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing SatisfiesM
φ : R →+* SatisfiesM
hφ : Function.Injective ⇑φ
f : R[X]
IH :
  ∀ (g₁ g₂ : SatisfiesM[X]),
    (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
      (map φ f).resultant g₁ * (map φ f).resultant g₂
g₁ g₂ : R[X]
⊢ φ (f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree)) = φ (f.resultant g₁ * f.resultant g₂)

Tactic:
have := IH (g₁.map φ) (g₂.map φ)

Goal state after:
case injective
R✝ : Type u_1
inst✝² : CommRing R✝
R SatisfiesM : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing SatisfiesM
φ : R →+* SatisfiesM
hφ : Function.Injective ⇑φ
f : R[X]
IH :
  ∀ (g₁ g₂ : SatisfiesM[X]),
    (map φ f).resultant (g₁ * g₂) (map φ f).natDegree (g₁.natDegree + g₂.natDegree) =
      (map φ f).resultant g₁ * (map φ f).resultant g₂
g₁ g₂ : R[X]
this :
  (map φ f).resultant (map φ g₁ * map φ g₂) (map φ f).natDegree ((map φ g₁).natDegree + (map φ g₂).natDegree) =
    (map φ f).resultant (map φ g₁) * (map φ f).resultant (map φ g₂)
⊢ φ (f.resultant (g₁ * g₂) f.natDegree (g₁.natDegree + g₂.natDegree)) = φ (f.resultant g₁ * f.resultant g₂)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g₁ g₂ : R[X]
m : ℕ
hm : f.natDegree ≤ m
⊢ f.resultant (g₁ * g₂) m (g₁.natDegree + g₂.natDegree) = f.resultant g₁ m * f.resultant g₂ m

Tactic:
by
  wlog hgn : m = f.natDegree
  · obtain ⟨c, rfl⟩ := le_iff_exists_add.mp hm
    simp [resultant_add_left_deg, this f g₁ g₂, coeff_mul_degree_add_degree]
    ring_nf
  subst hgn; clear hm
  induction f using induction_of_Splits_of_injective_of_surjective with
  | Splits R f hff =>
    simp [resultant_eq_prod_eval, natDegree_mul_le, hff]
    ring_nf
  | injective R SatisfiesM φ hφ f IH =>
    apply hφ
    have := IH (g₁.map φ) (g₂.map φ)
    rw [← Polynomial.map_mul] at this
    simpa only [resultant_map_map, ← map_mul, natDegree_map_eq_of_injective hφ] using this
  | surjective R S φ hφ f IH =>
    obtain ⟨f', hf', e⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ f)
    obtain ⟨g₁', hg₁, e₁⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₁)
    obtain ⟨g₂', hg₂, e₂⟩ := exists_degree_eq_of_mem_lifts (Polynomial.map_surjective φ hφ g₂)
    rw [← hg₁, ← hg₂, ← hf', ← Polynomial.map_mul]
    simp_rw [resultant_map_map, hg₁, hg₂, hf', ← natDegree_eq_natDegree e₁,
      ← natDegree_eq_natDegree e₂, ← natDegree_eq_natDegree e, IH, map_mul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
⊢ W = pullback.fst (fromNormalization f) g ⁻¹ᵁ fromNormalization f ⁻¹ᵁ U ⊓ pullback.snd (fromNormalization f) g ⁻¹ᵁ V

Tactic:
by simp_rw [W, ← Scheme.Hom.comp_preimage, pullback.condition, Scheme.Hom.comp_preimage,
      ← Scheme.Hom.preimage_inf, inf_eq_right.mpr hVU]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
have ⟨a, b, e⟩ := H

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

Tactic:
← resultant_add_mul_right _ _ a _ _ _ le_rfl,

Goal state after:
case inr.inr.inr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g + f * a) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ ∃ n, f.resultant g ∣ f.leadingCoeff ^ n

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
hf : f ≠ 0
hg : g ≠ 0
a b : R[X]
e : a * f + b * g = 1
ha : a ≠ 0
hb : b ≠ 0
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ ((algebraMap R R[X]) f.leadingCoeff * X ^ f.natDegree).resultant (g.leadingCoeff • X ^ g.natDegree) f.natDegree
      g.natDegree =
    0 ^ (f.natDegree * g.natDegree) * f.resultant g

Tactic:
Algebra.smul_def

Goal state after:
case neg.inl
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
hf : f ≠ 0
hg : g ≠ 0
hf0 : ¬f.natDegree = 0
hg0 : ¬g.natDegree = 0
⊢ ((algebraMap R R[X]) f.leadingCoeff * X ^ f.natDegree).resultant
      ((algebraMap R R[X]) g.leadingCoeff * X ^ g.natDegree) f.natDegree g.natDegree =
    0 ^ (f.natDegree * g.natDegree) * f.resultant g
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ (↑((homEquiv T m k hn p) (g.comp f))).1 = (↑((homEquiv S m k hn p) f)).1.map ↑g

Tactic:
by
  ext1
  simp [homEquiv, UniversalFactorizationRing.homEquiv, Polynomial.map_map]
  rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
T : Type u_4
inst✝¹ : CommRing T
inst✝ : Algebra R T
f : 𝓡' →ₐ[R] S
g : S →ₐ[R] T
⊢ (↑((homEquiv T m k hn p) (g.comp f))).2 = (↑((homEquiv S m k hn p) f)).2.map ↑g

Tactic:
by
  ext1
  simp [homEquiv, UniversalFactorizationRing.homEquiv, Polynomial.map_map]
  rfl

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

Goal state before:
pp: case neg.refine_2.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g

Tactic:
← resultant_add_mul_right _ _ a _ _ _ le_rfl,

Goal state after:
case neg.refine_2.inr
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g + f * a) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ 1 = f.resultant b * f.resultant g

R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.Monic
hf0 : ¬f.natDegree = 0
a b : R[X]
e : a * f + b * g = 1
this : f.resultant (b * g) f.natDegree (b.natDegree + g.natDegree) = f.resultant b * f.resultant g
hb0 : a ≠ 0
⊢ a.natDegree + f.natDegree ≤ b.natDegree + g.natDegree
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl.inr
K : Type u_2
inst✝ : Field K
g : K[X]
hg : g ≠ 0
⊢ resultant 0 g = 0 ↔ (0 ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime 0 g

Tactic:
simpa [isCoprime_zero_left, isUnit_iff, hg, natDegree_eq_zero] using
      show (∀ x, C x ≠ g) ↔ ∀ x ≠ 0, C x ≠ g by aesop

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X G : C
inst✝ : GrpObj G
f₁ f₂ : X ⟶ G
⊢ lift f₁ f₂ ≫ commutator G = f₁ * f₂ * f₁⁻¹ * f₂⁻¹

Tactic:
by
  simp [commutator, comp_mul, comp_inv]

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)
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
x✝ : ↥(G ⊗ G).left
⊢ x✝ ∈ ⇑(Over.Hom.left (fst G G)) ⁻¹' {(Over.Hom.left (fst G G)) y} →
    x✝ ∈
      ⇑(Over.Hom.left γ) ⁻¹'
        (⇑(pullback.fst G.hom G.hom) ⁻¹' {↑⟨(Over.Hom.left (fst G G)) y, hyU⟩} ∩ Set.range ⇑(Over.Hom.left γ))

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

Goal state after:
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'
⊢ V' ≤ V y

Tactic:
simp_rw [V', ← Category.assoc, opensRange_comp]

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)
𝒰 : (↑(⨆ 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'
⊢ (V y).ι ''ᵁ (toNormalization f ∣_ V y) ''ᵁ opensRange (X.homOfLE hWV) ≤ V y
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: case e'_2.e_a
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ (pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map (Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) ≫ (pullbackSpecIso ↑R ↑A ↑A).inv

Tactic:
← Iso.inv_comp_eq

Goal state after:
case e'_2.e_a
R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
this :
  (pullbackSpecIso ↑R ↑A ↑A).hom ≫
      Spec.map
        (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder ≫
          Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) =
    (pullbackSpecIso ↑R ↑A ↑A).hom ≫ Spec.map (Under.Hom.right (↑(Bialgebra.comulBialgHom ↑R ↑A)).toUnder)
h₁ :
  ↑Algebra.TensorProduct.includeRight =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp Algebra.TensorProduct.includeLeftRingHom
h₂ :
  Algebra.TensorProduct.includeLeftRingHom =
    (↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).comp ↑Algebra.TensorProduct.includeRight
e_1✝ :
  (pullback (Spec A ↘ Spec R) (Spec A ↘ Spec R) ⟶ Spec A) =
    (pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) ⟶
      ((algSpec R).obj (op (CommAlgCat.of ↑R ↑A))).left)
⊢ (pullbackSpecIso ↑R ↑A ↑A).inv ≫ (pullbackSymmetry (Spec A ↘ Spec R) (Spec A ↘ Spec R)).hom =
    Spec.map (Under.Hom.right (↑↑(Bialgebra.TensorProduct.comm ↑R ↑A ↑A)).toUnder) ≫ (pullbackSpecIso ↑R ↑A ↑A).inv
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom =
    (pullbackSpecIso' R T S).hom ≫ Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv

Tactic:
← Iso.inv_comp_eq

Goal state after:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSpecIso' R T S).inv ≫ (pullbackSymmetry (Spec (of T) ↘ Spec (of R)) (Spec (of S) ↘ Spec (of R))).hom =
    Spec.map (ofHom ↑(Algebra.TensorProduct.comm R S T)) ≫ (pullbackSpecIso' R S T).inv
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₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
by
  calc
    _ = 𝟙 _ ⊗≫
          (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
            g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫
              adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          g₂ ◁ (rightZigzag adj₁.unit adj₁.counit) ⊗≫
            (rightZigzag adj₂.unit adj₂.counit) ▷ g₁ ⊗≫ 𝟙 _ := by
      rw [whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [right_triangle]; bicategory

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp α β) =
    rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) α) ((mateEquiv adj₂ adj₃) β)

Tactic:
simp only [leftAdjointSquare.vcomp, mateEquiv_apply', rightAdjointSquare.vcomp]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d e f : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    (α_ r₁ g₁ g₂).inv ≫
      (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
        (α_ h₁ r₂ g₂).hom ≫
          h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
            (α_ h₁ h₂ r₃).inv
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_3
inst✝ : Finite σ
⊢ ringKrullDim R + ↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
induction σ using Finite.induction_empty_option with
  | of_equiv e H =>
    convert! ← H using 1
    · rw [Nat.card_congr e]
    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
  | h_empty => simp
  | h_option IH =>
    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    grw [IH, ringKrullDim_succ_le_ringKrullDim_polynomial]
    exact (ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv).ge

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⇑(Infinite.natEmbedding σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
⊢ ↑n ≤ ringKrullDim (MvPolynomial σ R)

Tactic:
refine le_trans ?_ (ringKrullDim_le_of_surjective
      (rename (R := R) _).toRingHom (rename_surjective _ this))

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
a✝ : Nontrivial R
h✝ : Infinite σ
n : ℕ
ι : Fin (n + 1) → σ := ⇑(Infinite.natEmbedding σ) ∘ Fin.val
this : Function.Surjective (Function.invFun ι)
⊢ ↑n ≤ ringKrullDim (MvPolynomial (Fin (n + 1)) R)
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: 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
⊢ ord f x ≤ ord (a • f) x

Tactic:
by_cases! hx : coheight x ≠ 1
  · simp [hx]
  by_cases hf : f = 0
  · simp [hf]
  have : a • f ≠ 0 := by simp [ha, Algebra.smul_def, hf, germToFunctionField_injective,
    RingHom.algebraMap_toAlgebra, map_ne_zero_iff]
  rw [ord_le_ord_iff hx hx hf this]
  algebraize [(X.presheaf.germ U x hxU).hom]
  have : Ring.KrullDimLE 1 ↑(X.presheaf.stalk x) := krullDimLE_of_coheight_le hx.le
  have : IsScalarTower ↑Γ(X, U) ↑(X.presheaf.stalk x) ↑X.functionField :=
    functionField_isScalarTower X U ⟨x, hxU⟩
  simp [ordHom, Ring.ordFrac_le_smul, RingHom.algebraMap_toAlgebra, map_ne_zero_iff,
    germ_injective_of_isIntegral, ha]

Goal state after: