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

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ IsIntegral R (coeff (Finsupp.mapDomain Subtype.val n) f)

Tactic:
simp_rw [← hg, coeff_rename_mapDomain _ Subtype.val_injective]

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
f : MvPolynomial σ S
H : (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f
this :
  ∀ {σ : Type w} {f : MvPolynomial σ S},
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).IsIntegralElem f →
      ∀ (n : σ →₀ ℕ), Finite σ → IsIntegral R (coeff n f)
hσ : ¬Finite σ
g : MvPolynomial (↥f.vars) S
hg : (rename Subtype.val) g = f
n : ↥f.vars →₀ ℕ
⊢ IsIntegral R (coeff n g)
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case e'_6
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Type w
hσ : Finite σ
f : MvPolynomial PEmpty.{w + 1} S
H : (algebraMap (MvPolynomial PEmpty.{w + 1} R) (MvPolynomial PEmpty.{w + 1} S)).IsIntegralElem f
n : PEmpty.{w + 1} →₀ ℕ
⊢ (isEmptyAlgEquiv S PEmpty.{w + 1}).symm.toRingEquiv.toRingHom (coeff n f) = f

Tactic:
· obtain rfl := Subsingleton.elim n 0
      have : constantCoeff = (isEmptyAlgEquiv S PEmpty).toRingHom := by aesop
      simpa [-EmbeddingLike.apply_eq_iff_eq, -isEmptyAlgEquiv_apply] using!
        congr((isEmptyAlgEquiv S PEmpty.{w + 1}).symm ($this f))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
⊢ U.presieveOfSections s = Presieve.ofArrows (fun i ↦ U.basicOpen ↑i) fun i ↦ homOfLE ⋯

Tactic:
by
  refine funext₂ fun ⟨V, hV⟩ ⟨f, hf⟩ ↦ eq_iff_iff.mpr ⟨?_, ?_⟩
  · rintro ⟨f, hfs, rfl⟩
    exact .mk (ι := s) ⟨f, hfs⟩
  · rintro ⟨⟨f, hfs⟩⟩
    exact ⟨f, hfs, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.f i)

Tactic:
obtain ⟨U, hxU⟩ := TopologicalSpace.Opens.mem_iSup.mp
      ((iSup_affineOpens_eq_top X).ge (Set.mem_univ x))

Goal state after:
X : Scheme
x : ↥X
U : ↑X.affineOpens
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := X.AffineZariskiSite, X := fun U ↦ ↑↑U, f := fun U ↦ (↑U).ι }.f i)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) p ≠ 0

Tactic:
exact algebraMap_ne_zero hp

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_5
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
P : StandardEtalePair R
⊢ ((Ideal.Quotient.liftₐ (Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})
            (IsLocalization.Away.liftAlgHom P.g ⋯) ⋯).comp
        (P.lift
          ((algebraMap R[X] (Localization.Away P.g ⧸ Ideal.span {(algebraMap R[X] (Localization.Away P.g)) P.f})) X) ⋯))
      P.X =
    (AlgHom.id R P.Ring) P.X

Tactic:
simp [IsScalarTower.algebraMap_apply R[X] (Localization.Away P.g) (_ ⧸ _),
      -Ideal.Quotient.mk_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
x : Localization.Away ((AdjoinRoot.mk P.f) P.g)
p : AdjoinRoot P.f
n : ℕ
e :
  x *
      (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
        ↑(p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).2 =
    (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
      (p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).1
⊢ ∃ p n, (P.equivRing.trans P.equivAwayAdjoinRoot).symm x * (aeval P.x) P.g ^ n = (aeval P.x) p

Tactic:
obtain ⟨p, rfl⟩ := AdjoinRoot.mk_surjective p

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePresentation R S
x : Localization.Away ((AdjoinRoot.mk P.f) P.g)
n : ℕ
p : R[X]
e :
  x *
      (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
        ↑((AdjoinRoot.mk P.f) p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).2 =
    (algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g)))
      ((AdjoinRoot.mk P.f) p, ⟨(fun x ↦ (AdjoinRoot.mk P.f) P.g ^ x) n, ⋯⟩).1
⊢ ∃ p n, (P.equivRing.trans P.equivAwayAdjoinRoot).symm x * (aeval P.x) P.g ^ n = (aeval P.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
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := ⋯
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := ⋯
this✝³ : SMul p.ResidueField (p.Fiber S) := ⋯
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := ⋯
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := ⋯
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := ⋯
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField := ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this : Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯ = AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField)
⊢ (TensorProduct.lift (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))
          (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯)
        r =
      0 ↔
    r ∈ (α ⟨Q, ⋯⟩).asIdeal

Tactic:
← SetLike.mem_coe,

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Q : Ideal S
inst✝⁴ : Q.IsPrime
inst✝³ : Module.Finite R S
inst✝² : IsUnramifiedAt R Q
inst✝¹ : Algebra (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (Ideal.under R Q) Q
p : Ideal R := Ideal.under R Q
this✝⁵ : p.IsPrime
this✝⁴ : Module p.ResidueField (p.Fiber S) := leftModule
this✝³ : SMul p.ResidueField (p.Fiber S) := this✝⁴.toSMul
this✝² : IsScalarTower p.ResidueField (p.Fiber S) (p.Fiber S) := IsScalarTower.right
this✝¹ : Module.Finite p.ResidueField (p.Fiber S) := Module.Finite.base_change R p.ResidueField S
this✝ : IsArtinianRing (p.Fiber S)
α : ↑(p.primesOver S) ≃o PrimeSpectrum (p.Fiber S) := PrimeSpectrum.primesOverOrderIsoFiber R S p
x : p.ResidueField ⊗[R] S
φ : p.Fiber S →ₐ[p.ResidueField] Q.ResidueField :=
  TensorProduct.lift (ofId p.ResidueField Q.ResidueField) (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯
hx0 : φ x ≠ 0
hx : p.ResidueField[φ x] = ⊤
r : p.Fiber S
hrQ : r ∉ (α ⟨Q, ⋯⟩).asIdeal
hrid : IsIdempotentElem r
hr : ∀ (q : Ideal (p.Fiber S)), q.IsPrime → q ≠ (α ⟨Q, ⋯⟩).asIdeal → r ∈ q
s : R
hsQ : s ∉ p
t : S
e : s • (r * x) = 1 ⊗ₜ[R] t
this : Ideal.ResidueField.mapₐ p Q (ofId R S) ⋯ = AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField)
⊢ (TensorProduct.lift (AlgHom.restrictScalars R (ofId p.ResidueField Q.ResidueField))
          (IsScalarTower.toAlgHom R S Q.ResidueField) ⋯)
        r =
      0 ↔
    r ∈ ↑(α ⟨Q, ⋯⟩).asIdeal
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
this : (M i).updateCol ⟨i, ⋯⟩ (r • fun j ↦ M i j ⟨i, ⋯⟩) = M (i + 1)
⊢ (M (i + 1)).det = r ^ (i + 1) * M₂.det

Tactic:
pow_succ',

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
m n : ℕ
r : R
M₁ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester (C r * g) m n
M₂ : Matrix (Fin (m + n)) (Fin (m + n)) R := f.sylvester g m n
M : ℕ → Matrix (Fin (m + n)) (Fin (m + n)) R := fun i ↦ Matrix.of fun j₁ j₂ ↦ if ↑j₂ < i then M₁ j₁ j₂ else M₂ j₁ j₂
i : ℕ
IH : i ≤ m → (M i).det = r ^ i * M₂.det
hi : i + 1 ≤ m
this : (M i).updateCol ⟨i, ⋯⟩ (r • fun j ↦ M i j ⟨i, ⋯⟩) = M (i + 1)
⊢ (M (i + 1)).det = r * r ^ i * M₂.det
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsReduced X
i : (normalizationOpenCover f).I₀
this : _root_.IsReduced ↑((normalizationDiagram f).obj (Opposite.op ↑i))
⊢ IsReduced ((normalizationOpenCover f).X i)

Tactic:
dsimp [normalizationOpenCover, normalizationGlueData, relativeGluingData]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsReduced X
i : (normalizationOpenCover f).I₀
this : _root_.IsReduced ↑((normalizationDiagram f).obj (Opposite.op ↑i))
⊢ IsReduced (Spec ((normalizationDiagram f).obj (Opposite.op (toOpens i))))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
this : (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) i (Sum.inl j) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n) i (Sum.inl j)

Tactic:
simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']

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

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
this : (if ↑j ≤ ↑i then f.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + m then f.coeff (↑i - ↑j) else 0
⊢ (LinearMap.toMatrix ((degreeLT.basis R m).prod (degreeLT.basis R n)) (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) i (Sum.inr j) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n) i (Sum.inr j)

Tactic:
simpa [LinearMap.toMatrix_apply, sylvester, coeff_mul_X_pow']

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
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✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hs⟩ ∈ q'

Tactic:
obtain ⟨s₃, hs₃⟩ := hs₂.2 (algebraMap _ _ s₁)

Goal state after:
R : Type u_2
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✝¹ : FiniteType R S
inst✝ : QuasiFiniteAt R q
s₁ : S
hs₁q : s₁ ∉ q
hs₁ : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s₁ ∈ q'
s₂ : ↥(integralClosure R S)
hs₂q : ↑s₂ ∉ q
hs₂ : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom s₂)
s₃ : Localization.Away s₂
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂) s₃ =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
⊢ ∃ s ∉ q,
    ∃ (hs : IsIntegral R s),
      (∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q') ∧
        ∀ (q' : Ideal ↥(integralClosure R S)),
          q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hs⟩ ∈ q'
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FiniteType R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
inst✝¹ : q.LiesOver p
inst✝ : QuasiFiniteAt R q
R' : Type u
w✝⁶ : CommRing R'
w✝⁵ : Algebra R R'
w✝⁴ : Etale R R'
P : Ideal R'
w✝³ : P.IsPrime
w✝² : P.LiesOver p
e : R' ⊗[R] S
he : IsIdempotentElem e
e₀ : R' ⊗[R] ↥(integralClosure R S)
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val) e₀ = e
P' : Ideal (R' ⊗[R] S)
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
heP' : e ∉ P'
hpP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
H' :
  ∀ (P'' : Ideal (R' ⊗[R] ↥(integralClosure R S))),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val).toRingHom P'
H : ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
g : ↥(integralClosure R S)
hgq : ↑g ∉ q
hg : Function.Bijective ⇑(Localization.awayMap (integralClosure R S).val.toRingHom g)
f : R'
hfP : f ∉ P
hf :
  Module.Finite (Localization.Away f)
    (Localization.Away ((TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)) e))
Pf : Ideal (Localization.Away f) := Ideal.map (algebraMap R' (Localization.Away f)) P
this : Pf.IsPrime
⊢ Disjoint ↑(Submonoid.powers f) ↑P

Tactic:
by
    rwa [Ideal.disjoint_powers_iff_notMem _ (Ideal.IsPrime.isRadical ‹_›)]

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

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
G : Scheme
f : G ⟶ Spec (CommRingCat.of K)
inst✝³ : LocallyOfFiniteType f
inst✝² : GrpObj (Over.mk f)
inst✝¹ : IsReduced G
inst✝ : IsAlgClosed K
this✝ : JacobsonSpace ↥G
this : Nonempty ↥G
H : (↑(Scheme.Hom.smoothLocus f))ᶜ.Nonempty
x : ↥G
hx : x ∈ (↑(Scheme.Hom.smoothLocus f))ᶜ
hxc : x ∈ closedPoints ↥G
y : ↥G
hyc : y ∈ closedPoints ↥G
x' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨x, hxc⟩) ⋯
y' : 𝟙_ (Over (Spec (CommRingCat.of K))) ⟶ Over.mk f := Over.homMk ↑((pointEquivClosedPoint f).symm ⟨y, hyc⟩) ⋯
α : Over.mk f ≅ Over.mk f := (GrpObj.mulRight x').symm ≪≫ GrpObj.mulRight y'
hα : x' ≫ α.hom = y'
hα' : (Over.Hom.left α.hom) x = y
hy : x ∈ Scheme.Hom.smoothLocus f
⊢ False

Tactic:
exact hx hy

Goal state after:
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
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)

Tactic:
rw [Iso.inv_hom_id]

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ 𝟙 (f ≫ g) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
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
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv

Tactic:
rw [Iso.inv_hom_id]

Goal state after:
B : Type u₁
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ 𝟙 (𝟙 b) = (λ_ f).hom ≫ (ρ_ f).inv
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
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
this : Submodule.span R ↑s ≤ f.toLinearMap.range
⊢ Function.Surjective ⇑f

Tactic:
rwa [hs, top_le_iff, LinearMap.range_eq_top] at this

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

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ (Spec.map φ) x ∈ Set.range (PrimeSpectrum.comap (algebraMap ↑R ↑S))

Tactic:
use x

Goal state after:
case h
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom φ).Flat
inst✝ : (CommRingCat.Hom.hom φ).Finite
algInst✝ : Algebra ↑R ↑S := ⋯
algebraizeInst✝¹ : Module.Flat ↑R ↑S
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ PrimeSpectrum.comap (algebraMap ↑R ↑S) x = (Spec.map φ) x
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
⊢ Function.Surjective ⇑(quotOfMul a I)

Tactic:
simp only [Ideal.quotOfMul]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
⊢ Function.Surjective ⇑(Submodule.factor ⋯)
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
I : Ideal R
this : (quotOfMul a I).ker = a • ⊤
⊢ (quotOfMul a I).ker = (mulQuot a I).range

Tactic:
simp [this, Ideal.mulQuot, Submodule.mapQ.eq_1, Submodule.range_liftQ,
    range_comp, Ideal.Quotient.smul_top, ← Ideal.submodule_span_eq, LinearMap.map_span]

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))
⊢ ∃ a, pointsPi R X a = f

Tactic:
let e : (Π i, R i) ≃+* Π j₀, R' j₀ :=
  { toFun f _ i := f i
    invFun f i := f _ ⟨i, rfl⟩
    right_inv _ := funext₂ fun j₀ i ↦ by rcases i with ⟨i, rfl⟩; rfl
    map_mul' _ _ := rfl
    map_add' _ _ := rfl }

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' := ⋯ }
⊢ ∃ a, pointsPi R X a = f
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 𝒜)
f : A
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal

Tactic:
← SetLike.mem_coe,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ ↑(vanishingIdeal t) ↔ ∀ x ∈ t, f ∈ 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 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
⊢ ⋂₀ Zs ∈ Set.range (zeroLocus 𝒜)

Tactic:
Set.sInter_eq_iInter

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
⊢ ⋂ i, ↑i ∈ Set.range (zeroLocus 𝒜)
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
⊢ (decompose ℬ) (∑ x_1 ∈ DFinsupp.support ((decompose 𝒜) x), f ↑(((decompose 𝒜) x) x_1)) =
    (map (↑f).gradedAddHom) ((decompose 𝒜) (∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i)))

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

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