mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝¹ x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ⟨f * ↑(x✝¹ + x✝).2 + g * ↑(x✝¹ + x✝).1, ⋯⟩ = ⟨f * ↑x✝¹.2 + g * ↑x✝¹.1, ⋯⟩ + ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩

Tactic:
ext1

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x✝¹ x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ↑⟨f * ↑(x✝¹ + x✝).2 + g * ↑(x✝¹ + x✝).1, ⋯⟩ = ↑(⟨f * ↑x✝¹.2 + g * ↑x✝¹.1, ⋯⟩ + ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩)
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
x✝¹ : R
x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ⟨f * ↑(x✝¹ • x✝).2 + g * ↑(x✝¹ • x✝).1, ⋯⟩ = (RingHom.id R) x✝¹ • ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩

Tactic:
ext1

Goal state after:
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
x✝¹ : R
x✝ : ↥R[X]_m × ↥R[X]_n
⊢ ↑⟨f * ↑(x✝¹ • x✝).2 + g * ↑(x✝¹ • x✝).1, ⋯⟩ = ↑((RingHom.id R) x✝¹ • ⟨f * ↑x✝.2 + g * ↑x✝.1, ⋯⟩)
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝⁶ : p.IsPrime
inst✝⁵ : q.IsPrime
inst✝⁴ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
P₁ P₂ : Ideal (R' ⊗[R] S)
inst✝³ : P₁.IsPrime
inst✝² : P₂.IsPrime
inst✝¹ : P₁.LiesOver q
inst✝ : P₂.LiesOver q
H₂ : comap Algebra.TensorProduct.includeRight.toRingHom P₁ = comap Algebra.TensorProduct.includeRight.toRingHom P₂
⊢ (fiberIsoOfBijectiveResidueField H) ⟨P₁, ⋯⟩ = (fiberIsoOfBijectiveResidueField H) ⟨P₂, ⋯⟩

Tactic:
ext1

Goal state after:
R : Type u_1
R' : Type u_2
S : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing R'
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra R S
p : Ideal R
q : Ideal R'
inst✝⁶ : p.IsPrime
inst✝⁵ : q.IsPrime
inst✝⁴ : q.LiesOver p
H : Function.Bijective ⇑(ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)
P₁ P₂ : Ideal (R' ⊗[R] S)
inst✝³ : P₁.IsPrime
inst✝² : P₂.IsPrime
inst✝¹ : P₁.LiesOver q
inst✝ : P₂.LiesOver q
H₂ : comap Algebra.TensorProduct.includeRight.toRingHom P₁ = comap Algebra.TensorProduct.includeRight.toRingHom P₂
⊢ ↑((fiberIsoOfBijectiveResidueField H) ⟨P₁, ⋯⟩) = ↑((fiberIsoOfBijectiveResidueField H) ⟨P₂, ⋯⟩)
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₃ : ↥(integralClosure R S)
n : ℕ
hs₃ :
  (Localization.awayMap (integralClosure R S).val.toRingHom s₂)
      (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩) =
    (algebraMap S (Localization.Away ((integralClosure R S).val.toRingHom s₂))) s₁
m : ℕ
hm : ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n)
hm0 : 0 < m
hs₃q : ↑s₃ ∉ q
q' : Ideal ↥(integralClosure R S)
x✝¹ : q'.IsPrime
hq'q : q' ≠ Ideal.under (↥(integralClosure R S)) q
x✝ : q'.LiesOver p
this✝⁴ : Algebra (↥(integralClosure R S)) (Localization.Away ↑s₂) := OreLocalization.instAlgebra
e : Localization.Away s₂ ≃ₐ[↥(integralClosure R S)] Localization.Away ↑s₂ :=
  AlgEquiv.ofBijective (Localization.awayMapₐ (ofId (↥(integralClosure R S)) S) s₂) hs₂
q's : Ideal (Localization.Away s₂) := Ideal.map (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) q'
H : ¬⟨↑s₂ ^ m * ↑s₃, ⋯⟩ ∈ q'
hq's : Disjoint ↑(Submonoid.powers s₂) ↑q'
this✝³ : q's.IsPrime
this✝² : q's.LiesOver q'
this✝¹ : q's.LiesOver p
this✝ :
  s₁ ∈
    Ideal.comap ((↑e.symm).comp (IsScalarTower.toAlgHom (↥(integralClosure R S)) S (Localization.Away ↑s₂))).toRingHom
      q's
this :
  e.symm
      ((Localization.awayMap (integralClosure R S).val.toRingHom s₂)
        (IsLocalization.mk' (Localization.Away s₂) s₃ ⟨(fun x ↦ s₂ ^ x) n, ⋯⟩)) ∈
    q's
⊢ (algebraMap (↥(integralClosure R S)) (Localization.Away s₂)) s₂ ^ n ∉ q's

Tactic:
exact Ideal.notMem_of_isUnit _ (.pow _ (IsLocalization.Away.algebraMap_isUnit _))

Goal state after:
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
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⟨s, hRs⟩
⊢ (aeval s₀) f = 0

Tactic:
ext1

Goal state after:
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
s : S
hsq : s ∉ q
hRs : IsIntegral R s
hs : ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
hs₀ :
  ∀ (q' : Ideal ↥(integralClosure R S)),
    q'.IsPrime → q' ≠ Ideal.under (↥(integralClosure R S)) q → q'.LiesOver p → ⟨s, hRs⟩ ∈ q'
m : ℕ
f : R[X]
b : p.ResidueField[X]
hfm : f.Monic
hbm : b.Monic
hab : IsCoprime (X ^ (m + 1)) b
hfab : Polynomial.map (algebraMap R p.ResidueField) f = X ^ (m + 1) * b
hf : (aeval s) f = 0
R' : Type u
w✝⁴ : CommRing R'
w✝³ : Algebra R R'
w✝² : Etale R R'
P : Ideal R'
w✝¹ : P.IsPrime
w✝ : P.LiesOver p
a' b' : R'[X]
hP : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯)
ha'm : a'.Monic
hb'm : b'.Monic
hfab' : Polynomial.map (algebraMap R R') f = a' * b'
c d : R'[X]
hcd : c * a' + d * b' = 1
ha' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom (X ^ (m + 1)) =
    Polynomial.map (algebraMap R' P.ResidueField) a'
hb' :
  Polynomial.map (Ideal.ResidueField.mapₐ p P (ofId R R') ⋯).toRingHom b =
    Polynomial.map (algebraMap R' P.ResidueField) b'
s₀ : ↥(integralClosure R S) := ⋯
⊢ ↑((aeval s₀) f) = ↑0
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₂ ≫ conj G = f₁ * f₂ * f₁⁻¹

Tactic:
simp [conj, 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 γ)
⊢ GrpObj.commutator G = toUnit (G ⊗ G) ≫ η

Tactic:
ext1

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 := ⋯
point : ↥S := ⋯
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 := ⋯
this✝ : IsProper (Over.Hom.left γ ≫ Over.Hom.left (fst G G))
this : IsProper (Over.Hom.left γ)
⊢ Over.Hom.left (GrpObj.commutator G) = Over.Hom.left (toUnit (G ⊗ G) ≫ η)
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 (fst G G)) ⁻¹' {(Over.Hom.left η) point} \
      ⇑(Over.Hom.left γ) ⁻¹' {(Over.Hom.left (lift η η)) point}).Nonempty
⊢ IsClosed (⇑(Over.Hom.left (fst G G)) ⁻¹' ⇑(Over.Hom.left η) '' {point})

Tactic:
exact (η[G].left.isClosedMap _ hpoint).preimage (fst G G).left.continuous

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsProper f
inst✝ : LocallyQuasiFinite f
⊢ IsFinite f

Tactic:
by
  have : IsIso f.toNormalization :=
    (isIso_iff_isOpenImmersion_and_surjective _).mpr ⟨inferInstance, inferInstance⟩
  refine (IsFinite.iff_isIntegralHom_and_locallyOfFiniteType _).mpr ⟨?_, inferInstance⟩
  rw [← f.toNormalization_fromNormalization]
  infer_instance

Goal state after:
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
this✝⁷ : Pf.LiesOver P
φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S := TensorProduct.map (ofId R' (Localization.Away f)) (AlgHom.id R S)
this✝⁶ : Algebra (R' ⊗[R] S) (Localization.Away f ⊗[R] S) := φ.toAlgebra
this✝⁵ : IsScalarTower R' (R' ⊗[R] S) (Localization.Away f ⊗[R] S) :=
  IsScalarTower.of_algebraMap_eq' (Eq.symm (AlgHom.comp_algebraMap φ))
this✝⁴ : IsLocalization.Away (f ⊗ₜ[R] 1) (Localization.Away f ⊗[R] S)
P'f : Ideal (Localization.Away f ⊗[R] S) := Ideal.map (algebraMap (R' ⊗[R] S) (Localization.Away f ⊗[R] S)) P'
hP'f : Disjoint ↑(Submonoid.powers (f ⊗ₜ[R] 1)) ↑P'
this✝³ : P'f.IsPrime
this✝² : P'f.LiesOver P'
this✝¹ : P'f.LiesOver P
this✝ : P'f.LiesOver Pf
this : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Pf (IsScalarTower.toAlgHom R R' (Localization.Away f)) ⋯)
⊢ Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Pf (ofId R (Localization.Away f)) ⋯)

Tactic:
by
      convert! this.comp hpP; rw [← AlgHom.coe_comp]; congr; ext

Goal state after:
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:
simp [ih_η, ih_θ]

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

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f :
  (Spec (CommRingCat.of T)).asOver (Spec (CommRingCat.of R)) ⟶
    (Spec (CommRingCat.of S)).asOver (Spec (CommRingCat.of R))
⊢ (fun f ↦ Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R)))
      ((fun f ↦ WithConv.toConv { toRingHom := CommRingCat.Hom.hom (preimage (Over.Hom.left f)), commutes' := ⋯ }) f) =
    f

Tactic:
ext1

Goal state after:
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f :
  (Spec (CommRingCat.of T)).asOver (Spec (CommRingCat.of R)) ⟶
    (Spec (CommRingCat.of S)).asOver (Spec (CommRingCat.of R))
⊢ Over.Hom.left
      ((fun f ↦ Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R)))
        ((fun f ↦ WithConv.toConv { toRingHom := CommRingCat.Hom.hom (preimage (Over.Hom.left f)), commutes' := ⋯ })
          f)) =
    Over.Hom.left f
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ Hom.asOver (map (CommRingCat.ofHom (f * g).ofConv.toRingHom)) (Spec (CommRingCat.of R)) =
    Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R)) *
      Hom.asOver (map (CommRingCat.ofHom g.ofConv.toRingHom)) (Spec (CommRingCat.of R))

Tactic:
ext1

Goal state after:
R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f g : WithConv (S →ₐ[R] T)
⊢ Over.Hom.left (Hom.asOver (map (CommRingCat.ofHom (f * g).ofConv.toRingHom)) (Spec (CommRingCat.of R))) =
    Over.Hom.left
      (Hom.asOver (map (CommRingCat.ofHom f.ofConv.toRingHom)) (Spec (CommRingCat.of R)) *
        Hom.asOver (map (CommRingCat.ofHom g.ofConv.toRingHom)) (Spec (CommRingCat.of R)))
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsNoetherianRing R
inst✝⁴ : KrullDimLE 1 R
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : Nontrivial R
x : R
hx : x ≠ 0
⊢ (ordFrac R) ((algebraMap R K) x) = (ordMonoidWithZeroHom R) x

Tactic:
have := (FaithfulSMul.algebraMap_injective R K).isDomain
  refine (Submonoid.LocalizationMap.lift_eq ..).trans ?_
  simp [ordMonoidWithZeroHom, mem_nonZeroDivisors_iff_ne_zero.mpr hx]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OrderOfVanishing

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ n ≤ Multiplicative.toAdd (unzero ⋯) ↔ ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f

Tactic:
nth_rw 1 [← toAdd_ofAdd n]

Goal state after:
X : Scheme
inst✝¹ : IsIntegral X
inst✝ : IsLocallyNoetherian X
x : ↥X
hx : coheight x = 1
f : ↑X.functionField
hf : f ≠ 0
n : ℤ
⊢ Multiplicative.toAdd (Multiplicative.ofAdd n) ≤ Multiplicative.toAdd (unzero ⋯) ↔
    ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
⊢ I = ⊥

Tactic:
refine le_bot_iff.mp fun x hx ↦ ?_

Goal state after:
ι : Type u
R : ι → CommRingCat
I : Ideal ((i : ι) → ↑(R i))
f : (∐ fun i ↦ Spec (R i)) ⟶ Spec (CommRingCat.of (((i : ι) → ↑(R i)) ⧸ I))
hf : f ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)) = sigmaSpec R
x : (i : ι) → ↑(R i)
hx : x ∈ I
⊢ 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 = ⊤
⊢ IsClosedImmersion g

Tactic:
have : IsIso g.coborderRange.ι := by rw [this, ← Scheme.topIso_hom]; infer_instance

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 = ⊤
this : IsIso (Scheme.Hom.coborderRange g).ι
⊢ IsClosedImmersion g
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t'

Tactic:
ext1

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ (vanishingIdeal (t ∪ t')).toIdeal = (vanishingIdeal t ⊓ vanishingIdeal t').toIdeal
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 𝒜)
this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t))).toIdeal = (vanishingIdeal t).toIdeal
⊢ vanishingIdeal (closure t) = vanishingIdeal t

Tactic:
ext1

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : (vanishingIdeal (zeroLocus 𝒜 ↑(vanishingIdeal t))).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ Va ⊓ Vb
wa :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b : a_1 ∈ Va),
    a ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
wb :
  ∀ (a : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a ∈ Vb),
    b ⟨a, ⋯⟩ = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ (fun x ↦ (a + b) ((Va.infLELeft Vb ≫ ia) x)) ⟨y, hy⟩ =
    HomogeneousLocalization.mk { deg := ja + jb, num := ⟨sb * ra + sa * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }

Tactic:
simp [wa y hy.1, wb y hy.2, ext_iff_val, add_mk, add_comm (sa * rb)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
⊢ ↑((ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.map (homOfLE ⋯).op))
        (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ })) =
    ↑((ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.map i.op)) s)

Tactic:
ext ⟨t, ht⟩

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
t : ↑(ProjectiveSpectrum.top 𝒜)
ht : t ∈ unop (op V)
⊢ HomogeneousLocalization.val
      (↑((ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.map (homOfLE ⋯).op))
            (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }))
        ⟨t, ht⟩) =
    HomogeneousLocalization.val (↑((ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.map i.op)) s) ⟨t, ht⟩)
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

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

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

Goal state after:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback (𝟙 Y) ⋙ pullback f ≅ pullback (f ≫ 𝟙 Y) := pullbackComp f (𝟙 Y)
e₂ : pullback (𝟙 Y) ⋙ pullback f ≅ 𝟭 Y.Modules ⋙ pullback f := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
e₃ : 𝟭 Y.Modules ⋙ pullback f ≅ pullback f := (pullback f).leftUnitor
⊢ (pullbackComp f (𝟙 Y)).inv ≫ Functor.whiskerRight (pullbackId Y).hom (pullback f) ≫ (pullback f).leftUnitor.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
𝒜 : ι → σ
x : Submonoid A
f : HomogeneousLocalization 𝒜 x
⊢ IsLocalization.mk' (at x) (f.den * f.num) ⟨f.den, ⋯⟩ = (algebraMap A (at x)) f.num

Tactic:
exact IsLocalization.mk'_mul_cancel_left _ ⟨_, _⟩

Goal state after: