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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
inst✝ : LocallyQuasiFinite g
⊢ (CommRingCat.Hom.hom (stalkMap g (f x) ≫ stalkMap f x)).QuasiFinite ↔ (CommRingCat.Hom.hom (stalkMap f x)).QuasiFinite

Tactic:
exact RingHom.QuasiFinite.comp_iff (g.quasiFiniteAt _)

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inl
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1
⊢ (map φ hφ) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) 0) =
    (algebraMap R[X] R⟮X⟯) (φ p) / (algebraMap R[X] R⟮X⟯) (φ 0)

Tactic:
rw [map_zero, map_zero, map_zero, div_zero, div_zero, this, map_apply_div_ne_zero, map_one,
      map_one, div_one, map_zero, map_zero]

Goal state after:
case inl.hq
K : Type u
inst✝⁵ : CommRing K
inst✝⁴ : IsDomain K
R : Type u_1
F : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : FunLike F K[X] R[X]
inst✝ : MonoidWithZeroHomClass F K[X] R[X]
φ : F
hφ : K[X]⁰ ≤ Submonoid.comap φ R[X]⁰
p : K[X]
this : 0 = (algebraMap K[X] K⟮X⟯) 0 / (algebraMap K[X] K⟮X⟯) 1
⊢ 1 ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) p) / (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] K⟮X⟯) q) =
    φ p / φ q

Tactic:
rw [← map_div₀, liftMonoidWithZeroHom_apply_div]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) x.denom ↔
    (algebraMap K[X] K⟮X⟯) x.num * (((algebraMap K[X] K⟮X⟯) x.denom)⁻¹ * (algebraMap K[X] K⟮X⟯) q) =
      (algebraMap K[X] K⟮X⟯) p

Tactic:
mul_comm (Inv.inv _),

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) x.denom ↔
    (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q * ((algebraMap K[X] K⟮X⟯) x.denom)⁻¹ =
      (algebraMap K[X] K⟮X⟯) p

Tactic:
← div_eq_mul_inv,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) x.denom ↔
    (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q / (algebraMap K[X] K⟮X⟯) x.denom = (algebraMap K[X] K⟮X⟯) p
Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
⊢ minpoly P.ResidueField ((algebraMap S Q.ResidueField) x) =
    minpoly P.ResidueField ((algebraMap (P.Fiber S) Q'.ResidueField) (1 ⊗ₜ[R] x))

Tactic:
← minpoly.algHom_eq _
    (IsScalarTower.toAlgHom P.ResidueField Q.ResidueField Q'.ResidueField).injective

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Ideal R
inst✝⁵ : P.IsPrime
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Q.LiesOver P
inst✝² : IsUnramifiedAt R Q
x : S
p : R[X]
inst✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker (aeval (1 ⊗ₜ[R] x)).toRingHom
hp₂ : R[x] = ⊤
Q' : Ideal (P.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S P) ⟨Q, ⋯⟩).asIdeal
this✝⁴ : Q'.LiesOver Q
this✝³ : Q'.LiesOver P
this✝² : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver Q Q'
this✝¹ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') := Localization.AtPrime.algebraOfLiesOver P Q'
this✝ : IsUnramifiedAt P.ResidueField Q'
this : Function.Surjective ⇑(aeval (1 ⊗ₜ[R] x))
⊢ minpoly P.ResidueField
      ((IsScalarTower.toAlgHom P.ResidueField Q.ResidueField Q'.ResidueField) ((algebraMap S Q.ResidueField) x)) =
    minpoly P.ResidueField ((algebraMap (P.Fiber S) Q'.ResidueField) (1 ⊗ₜ[R] x))
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal S
⊢ ZariskisMainProperty R p ↔ ∃ r ∉ p, IsIntegral R r ∧ ∀ (x : S), ∃ m, IsIntegral R (r ^ m * x)

Tactic:
simp only [ZariskisMainProperty, Subtype.exists, ← exists_prop, @exists_comm (_ ∉ p)]
  refine exists₃_congr fun r hr hrp ↦ ?_
  rw [Function.Bijective, and_iff_right
    (by exact IsLocalization.map_injective_of_injective _ _ _ Subtype.val_injective),
    Localization.awayMap_surjective_iff]
  simp [mem_integralClosure_iff]

Goal state after:
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
⊢ IsIntegral R[X] ((algebraMap S[X] S'[X]) (derivative f * y %ₘ f))

Tactic:
simp only [algebraMap_def, coe_mapRingHom, H]

Goal state after:
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
⊢ IsIntegral R[X] (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
Module: Mathlib.RingTheory.Polynomial.DegreeLT

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
Q : ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n) Q)) = ↑Q * X ^ m

Tactic:
rw [← (basis ..).sum_repr Q]

Goal state after:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
Q : ↥R[X]_n
⊢ ↑((addLinearEquiv R m n).symm ((LinearMap.inr R (↥R[X]_m) ↥R[X]_n) (∑ i, ((basis R n).repr Q) i • (basis R n) i))) =
    ↑(∑ i, ((basis R n).repr Q) i • (basis R n) i) * X ^ m
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)

Tactic:
rw! (castMode := .all) [f.preimage_basicOpen r]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : QuasiSeparated f
U : Y.AffineZariskiSite
r : ↑Γ(Y, ↑U)
this✝³ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝² : Algebra ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (app f ↑(U.basicOpen r))).toAlgebra
this✝¹ : Algebra ↥(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U))
  ↥(integralClosure ↑Γ(Y, Y.basicOpen r) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this : Algebra ↑Γ(X, f ⁻¹ᵁ ↑U) ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away ((algebraMap ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (app f ↑U)) r))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
hn : ¬f.natDegree = 0
j : ℕ
hj : j < f.natDegree - 1 + f.natDegree
hi : 2 * f.natDegree - 2 < f.natDegree - 1 + f.natDegree
h✝³ : ¬j = f.natDegree - 2
h✝² : j = 2 * f.natDegree - 2
h✝¹ : ¬j < f.natDegree - 1
h✝ : j ≤ 2 * f.natDegree - 2 + (f.natDegree - 1) ∧ 2 * f.natDegree ≤ j - (f.natDegree - 1) + (f.natDegree - 1) + 2
⊢ f.coeff f.natDegree * ↑f.natDegree =
    f.coeff (2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1) * (↑(2 * f.natDegree - 2 - (j - (f.natDegree - 1))) + 1)

Tactic:
rw [← Nat.cast_one (R := R), ← Nat.cast_add]
      #adaptation_note
      /--
      Prior to nightly-2025-09-09,
      these two steps were not needed (i.e. `grind` just finished from here)
      -/
      have : 2 * f.natDegree - 2 - (j - (f.natDegree - 1)) + 1 = f.natDegree := by grind
      simp [this]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
H : IsCoprime f g
⊢ f.resultant g ≠ 0

Tactic:
obtain rfl | hf := eq_or_ne f 0
  · simp only [isCoprime_zero_left, isUnit_iff] at H
    aesop
  intro e
  simpa [e, hf] using resultant_dvd_leadingCoeff_pow f g H

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := ⋯
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := ⋯
⊢ V ≤ toNormalization (pullback.snd f fT) ⁻¹ᵁ e.hom ⁻¹ᵁ opensRange ι

Tactic:
rw [← Scheme.Hom.inv_image, ← SetLike.coe_subset_coe]

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
⊢ ↑V ⊆ ↑(toNormalization (pullback.snd f fT) ⁻¹ᵁ e.inv ''ᵁ opensRange ι)
Module: Mathlib.AlgebraicGeometry.Group.Abelian

Goal state before:
pp: case refine_2
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
⊢ ∀ x ∈ ↑(Over.Hom.left (fst G G) ⁻¹ᵁ U),
    IsClosed {x} → (Over.Hom.left (GrpObj.commutator G)) x = (Over.Hom.left (toUnit (G ⊗ G) ≫ η)) x

Tactic:
intro y hyU hy

Goal state after:
case refine_2
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}
⊢ (Over.Hom.left (GrpObj.commutator G)) y = (Over.Hom.left (toUnit (G ⊗ G) ≫ η)) y
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Goal state before:
pp: B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η ε ⊗≫ rightZigzag η ε = rightZigzag η ε

Tactic:
dsimp only [rightZigzag]
  calc
    _ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory

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.Finite R S
inst✝ : Algebra.FinitePresentation R S
⊢ FinitePresentation R S

Tactic:
by
  obtain ⟨R', _, _, _, _, _, f, hf⟩ := Module.Finite.exists_free_surjective R S
  let := f.toRingHom.toAlgebra
  have : IsScalarTower R R' S := .of_algebraMap_eq' f.comp_algebraMap.symm
  have : Module.FinitePresentation R R' :=
    Module.finitePresentation_of_projective R R'
  have : Module.FinitePresentation R' S :=
    Module.finitePresentation_of_surjective (Algebra.linearMap R' S) hf
      (Algebra.FinitePresentation.ker_fG_of_surjective f hf)
  exact .trans R S R'

Goal state after:
Module: Mathlib.RingTheory.Flat.Rank

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
⊢ (∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p) ↔ Function.Surjective (comap (algebraMap R S))

Tactic:
rankAtStalk_pos_iff_mem_range_comap,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Flat R S
inst✝ : Module.Finite R S
⊢ (∀ (p : PrimeSpectrum R), p ∈ Set.range (comap (algebraMap R S))) ↔ Function.Surjective (comap (algebraMap R S))
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X S Y T : Scheme
f : X ⟶ S
inst✝³ : IsAffine S
inst✝² : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst✝¹ : Flat f
inst✝ : IsFinite f
s : ↥S
t : ↥T
hs : g t = s
⊢ finrank f' t = finrank f s

Tactic:
by
  subst hs
  have : IsAffine X := isAffine_of_isAffineHom f
  have : IsPushout f.appTop g.appTop g'.appTop f'.appTop := isPushout_appTop_of_isPullback h
  dsimp [finrank]
  rw [CommRingCat.finrank_eq_of_isPushout this f.flat_appTop f.finite_appTop (T.isoSpec.hom t),
    ← Scheme.Hom.comp_apply, ← Scheme.isoSpec_hom_naturality]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↥X
f g : Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X
e : pointsPi R X f = pointsPi R X g
⊢ sigmaSpec R ≫ f = sigmaSpec R ≫ g

Tactic:
ext1 i; simpa using! congr_fun e i

Goal state after:
Module: Mathlib.Data.FunLike.Graded

Goal state before:
pp: E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x✝ : ↥(𝒜 i)
⊢ ↑((fun y ↦ ⟨EquivLike.inv e ↑y, ⋯⟩) (subtypeMap e i x✝)) = ↑x✝

Tactic:
exact EquivLike.inv_apply_apply e _

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
⊢ (pullbackComp (𝟙 X) f).inv ≫ (pullback f).whiskerLeft (pullbackId X).hom ≫ (pullback f).rightUnitor.hom = eqToHom ⋯

Tactic:
let e₃ := (pullback f).rightUnitor

Goal state after:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
⊢ (pullbackComp (𝟙 X) f).inv ≫ (pullback f).whiskerLeft (pullbackId X).hom ≫ (pullback f).rightUnitor.hom = eqToHom ⋯
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✝ : GradedRing 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
⊢ e • d = d • e

Tactic:
exact mul_comm _ _

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

Goal state before:
pp: case neg.mem
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a✝ : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
a : A
ha' : a ∈ ↑(Submonoid.closure (Set.range v))
⊢ mk { deg := n, num := ((decompose 𝒜) a) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
obtain ⟨ai, rfl⟩ := Submonoid.exists_of_mem_closure_range _ _ ha'

Goal state after:
case neg.mem
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ι
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ι
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
ha' : ∏ i, v i ^ ai i ∈ ↑(Submonoid.closure (Set.range v))
⊢ mk { deg := n, num := ((decompose 𝒜) (∏ i, v i ^ ai i)) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ Localization.mk 0 ⟨f ^ i, ⋯⟩ = 0

Tactic:
exact Localization.mk_zero (S := Submonoid.powers f) _

Goal state after: