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

Goal state before:
pp: case refine_1
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 R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝³ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this✝² : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
this✝¹ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this✝ : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : Fin m
⊢ ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars (MvPolynomial (Fin n) R)
                  ((fun q ↦
                      Algebra.TensorProduct.lift (Algebra.ofId R S)
                        (let __RingHom :=
                          (↑((MvPolynomial.universalFactorizationMapLiftEquiv R S n m k hn
                                    (p.map (algebraMap R S))).symm
                                q)).toRingHom;
                        { toRingHom := __RingHom, commutes' := ⋯ })
                        ⋯)
                    ((fun f ↦ ⟨((factor₁ m k hn p).map ↑f, (factor₂ m k hn p).map ↑f), ⋯⟩) f))).comp
              Algebra.TensorProduct.includeRight)).comp
        Algebra.TensorProduct.includeLeft)
      (MvPolynomial.X i✝) =
    ((AlgHom.restrictScalars R
            ((AlgHom.restrictScalars (MvPolynomial (Fin n) R) f).comp Algebra.TensorProduct.includeRight)).comp
        Algebra.TensorProduct.includeLeft)
      (MvPolynomial.X i✝)

Tactic:
simp [MvPolynomial.universalFactorizationMapLiftEquiv, MvPolynomial.mapEquivMonic,
        UniversalFactorizationRing.factor₁, coeff_freeMonic]

Goal state after:
case refine_1
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 R n
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this✝³ : Algebra (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) R ⊗[R] MvPolynomial (Fin k) R) :=
  (MvPolynomial.universalFactorizationMap R n m k hn).toAlgebra
this✝² : Algebra (MvPolynomial (Fin n) R) R := ((MvPolynomial.mapEquivMonic R R n).symm p).toAlgebra
this✝¹ : Algebra (MvPolynomial (Fin n) R) S := Algebra.compHom S ((MvPolynomial.mapEquivMonic R R n).symm p).toRingHom
this✝ : IsScalarTower (MvPolynomial (Fin n) R) R S
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : Fin m
⊢ f ((fromTensor m k hn p) (MvPolynomial.X i✝ ⊗ₜ[R] 1)) = f (1 ⊗ₜ[MvPolynomial (Fin n) R] (MvPolynomial.X i✝ ⊗ₜ[R] 1))
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case Splits
R✝ : Type u_1
inst✝¹ : CommRing R✝
R : Type u_1
inst✝ : Field R
f : R[X]
hf' : f.Splits
g : R[X]
r : R
⊢ ((taylor r) f).resultant ((taylor r) g) = f.resultant g

Tactic:
induction hf' using Submonoid.closure_induction with

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

Goal state before:
pp: case inr
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)
this :
  ∀ (m : ℕ),
    ↑s₂ ^ m * ↑s₃ = ↑s₂ ^ m * (s₁ * ↑s₂ ^ n) →
      0 < m →
        ∃ 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'
hm0 : ¬0 < m
⊢ ∃ 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:
refine this (m + 1) (by grind) (by simp)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
G : C
inst✝ : GrpObj G
⊢ ι = (𝟙 G)⁻¹

Tactic:
by simp [Hom.inv_def]

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

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

Tactic:
← α.homEquiv'_comp,

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

Goal state before:
pp: case refine_2
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⟩
hfs₀ : (aeval s₀) f = 0
s' : R' ⊗[R] S := 1 ⊗ₜ[R] s
hs'f : (aeval s') f = 0
hs₀'f : (aeval (1 ⊗ₜ[R] s₀)) f = 0
e₀ : R' ⊗[R] ↥(integralClosure R S) := (aeval (1 ⊗ₜ[R] s₀)) (c * a')
he₀ : IsIdempotentElem e₀
e : R' ⊗[R] S := (aeval s') (c * a')
φ : R' ⊗[R] ↥(integralClosure R S) →ₐ[R'] R' ⊗[R] S := TensorProduct.map (AlgHom.id R' R') (integralClosure R S).val
he₀e : φ e₀ = e
he : IsIdempotentElem e
P' : ↑(P.primesOver (R' ⊗[R] S)) := (Ideal.fiberIsoOfBijectiveResidueField hP).symm ⟨q, ⋯⟩
this : Algebra (Localization.AtPrime P) (Localization.AtPrime ↑P') := Localization.AtPrime.algebraOfLiesOver P ↑P'
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom ↑P' = q
hs'P' : s' ∉ ↑P'
ha'P' : (aeval s') a' ∉ ↑P'
hb'P' : (aeval s') b' ∈ ↑P'
heP' : e ∉ ↑P'
P'' : Ideal (R' ⊗[R] S)
x✝¹ : P''.IsPrime
x✝ : P''.LiesOver P
H : e ∉ P''
⊢ P'' = ↑P'

Tactic:
· apply Ideal.eq_of_comap_eq_comap_of_bijective_residueFieldMap hP
    rw [hP'q]
    contrapose! H
    have : s' ∈ P'' := hs _ inferInstance H (by simp [Ideal.liesOver_iff, Ideal.under,
      Ideal.comap_comap, Ideal.over_def P p, Ideal.over_def P'' P, ← IsScalarTower.algebraMap_eq])
    rw [← Ideal.algebraMap_residueField_eq_zero, ← aeval_algebraMap_apply,
      Ideal.algebraMap_residueField_eq_zero.mpr this, ← eval_map_algebraMap, Polynomial.map_mul,
      mul_comm, ← (Ideal.ResidueField.mapₐ P P'' (Algebra.ofId _ _)
      (P''.over_def P)).comp_algebraMap, ← Polynomial.map_map, ← ha']
    simp

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
⊢ (∃ i, (toNormalization f) x ∈ V i) → QuasiFiniteAt f x

Tactic:
rintro ⟨y, hxVy⟩

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
⊢ QuasiFiniteAt f x
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this : Algebra.IsIntegral R' (Localization.Away e₀)
⊢ Function.Surjective
    ⇑(Localization.awayMapₐ
        (Localization.awayMapₐ (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀)
        ((algebraMap (R' ⊗[R] R'') (Localization.Away e₀)) (1 ⊗ₜ[R] g)))

Tactic:
apply Localization.awayMap_awayMap_surjective
    refine Localization.awayMap_surjective_iff.mpr fun a ↦ ?_
    induction a with
    | zero => use 0; simp
    | tmul a b =>
      obtain ⟨b', m, e : _ = _⟩ := Localization.awayMap_surjective_iff.mp hg b
      refine ⟨e₀ ^ m * a ⊗ₜ b', m, ?_⟩
      simp [e, mul_pow, mul_assoc]
    | add a b ha hb =>
      obtain ⟨xa, ma, ea⟩ := ha
      obtain ⟨xb, mb, eb⟩ := hb
      refine ⟨(e₀ * 1 ⊗ₜ[R] g) ^ mb * xa + (e₀ * 1 ⊗ₜ[R] g) ^ ma * xb, ma + mb, ?_⟩
      dsimp at ea eb ⊢
      simp only [map_add, map_mul, map_pow, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
        ea, eb, pow_add]
      ring

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: ⊢ CodescendsAlong (fun {R S} [CommRing R] [CommRing S] ↦ Finite) fun {R S} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk _ finite_respectsIso fun R S T _ _ _ _ _ h h' ↦ ?_
  rw [finite_algebraMap] at h' ⊢
  rw [faithfullyFlat_algebraMap_iff] at h
  exact .of_finite_tensorProduct_of_faithfullyFlat S

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

Goal state before:
pp: R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ Over.Hom.left (Over.homMk (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ⋯) =
    Over.Hom.left (OplaxMonoidal.δ (algSpec R) X Y)

Tactic:
Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory,

Goal state after:
R : CommRingCat
X Y : (CommAlgCat ↑R)ᵒᵖ
⊢ Over.Hom.left (Over.homMk (pullbackSpecIso ↑R ↑(unop X) ↑(unop Y)).inv ⋯) =
    Over.Hom.left (prodComparison (algSpec R) X Y)
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case neg
R : Type u
S : Type (max u v)
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra R S
p : Ideal R
inst✝¹⁶ : p.IsPrime
q : Ideal S
R' : Type u
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : Algebra R R'
inst✝¹³ : Etale R R'
P : Ideal R'
inst✝¹² : P.IsPrime
inst✝¹¹ : P.LiesOver p
e : R' ⊗[R] S
P' : Ideal (R' ⊗[R] S)
inst✝¹⁰ : P'.IsPrime
inst✝⁹ : 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] S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P'
R'' : Type u
inst✝⁸ : CommRing R''
inst✝⁷ : Algebra R' R''
inst✝⁶ : Algebra R R''
inst✝⁵ : IsScalarTower R R' R''
inst✝⁴ : Etale R' R''
Q : Ideal R''
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
n : ℕ
e' : Fin (n + 1 + 1) → R'' ⊗[R] S
he' : CompleteOrthogonalIdempotents e'
he'0 : e' 0 = (TensorProduct.map (ofId R' R'') (AlgHom.id R S)) e
Q' : Fin n → Ideal (R'' ⊗[R] S)
inst✝¹ : ∀ (i : Fin n), (Q' i).IsPrime
inst✝ : ∀ (i : Fin n), (Q' i).LiesOver Q
hPQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (ofId R' R'') ⋯)
hQ' : ∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i
H' :
  ∀ (P'' : Ideal (R'' ⊗[R] S)),
    e' 0 ∈ P'' →
      P''.IsPrime → P''.LiesOver Q → e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i
φ : R' ⊗[R] S →ₐ[R'] R'' ⊗[R] S := TensorProduct.map (ofId R' R'') (AlgHom.id R S)
this✝¹ : Q.LiesOver p
hpQ : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p Q (ofId R R'') ⋯)
P'φ : ↑(Q.primesOver (R'' ⊗[R] S)) :=
  (Ideal.fiberIsoOfBijectiveResidueField hpQ).symm ((Ideal.fiberIsoOfBijectiveResidueField hpP) ⟨P', ⋯⟩)
this✝ : (↑P'φ).LiesOver P
this : (Ideal.comap φ.toRingHom ↑P'φ).LiesOver P
hP'φ : Ideal.comap φ.toRingHom ↑P'φ = P'
P'' : Ideal (R'' ⊗[R] S)
a✝¹ : P''.IsPrime
a✝ : P''.LiesOver Q
heP'' : e ∉ Ideal.comap φ P''
⊢ e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin (n + 1)), e' i.castSucc ∉ P'' → P'' = Fin.cons (↑P'φ) Q' i

Tactic:
have : P''.LiesOver P := .trans _ Q _
      obtain rfl := H _ inferInstance inferInstance heP''
      have : ∀ i ≠ 0, e' i ∈ P'' := by
        intro j hj
        rw [← Ideal.IsPrime.mul_mem_left_iff (I := P'') heP'']
        simp [φ, ← he'0, he'.ortho hj.symm]
      refine ⟨by simp [this], Fin.cases (fun _ ↦ ?_) (by simp [this])⟩
      simp only [Fin.cons_zero]
      apply Ideal.eq_of_comap_eq_comap_of_bijective_residueFieldMap hpQ
      have : (φ.restrictScalars _).comp Algebra.TensorProduct.includeRight =
          Algebra.TensorProduct.includeRight := by ext; simp [φ]
      rw [← this]
      exact congr(($hP'φ).comap Algebra.TensorProduct.includeRight).symm

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Bicategory.Normalize

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₁ : ((Iso.refl h).hom ≫ η ≫ (Iso.refl i).hom) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : (α ▷ᵢ k).hom ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp at e_η₁ e_η₅

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₁ : η ▷ k = η₁
e_η₅ : α.hom ▷ k ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
⊢ IsOpenImmersion f

Tactic:
have hU : IsOpenImmersion U.ι := U.instIsOpenImmersionι

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Mono f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f], Surjective f → IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
⊢ IsOpenImmersion f
Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ PrimeSpectrum.zeroLocus ↑(Ideal.span {r}) ≠ ∅

Tactic:
ne_eq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
r : R
hr : r ∈ R⁰
hr' : ¬Ideal.span {r} = ⊤
⊢ ¬PrimeSpectrum.zeroLocus ↑(Ideal.span {r}) = ∅
Module: Mathlib.AlgebraicGeometry.PointsPi

Goal state before:
pp: ι : Type u
R : ι → CommRingCat
X : Scheme
inst✝ : QuasiSeparatedSpace ↥X
⊢ Function.Injective (pointsPi R X)

Tactic:
rintro f g e
  have := isIso_of_comp_eq_sigmaSpec R (V := equalizer f g)
    (equalizer.lift (sigmaSpec R) (by ext1 i; simpa using! congr_fun e i))
    (equalizer.ι f g) (by simp)
  rw [← cancel_epi (equalizer.ι f g), equalizer.condition]

Goal state after:
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 𝒜
f g : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 {f * g} ↔ x ∈ zeroLocus 𝒜 {f} ∪ zeroLocus 𝒜 {g}

Tactic:
simpa using x.isPrime.mul_mem_iff_mem_or_mem

Goal state after:
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)).toIdeal = (vanishingIdeal t).toIdeal

Tactic:
zeroLocus_vanishingIdeal_eq_closure 𝒜 t

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 (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
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
c1 c2 : NumDenSameDeg 𝒜 x
hdeg : c1.deg = c2.deg
hnum : ↑c1.num = ↑c2.num
hden : ↑c1.den = ↑c2.den
⊢ c1 = c2

Tactic:
rcases c1 with ⟨i1, ⟨n1, hn1⟩, ⟨d1, hd1⟩, h1⟩
  rcases c2 with ⟨i2, ⟨n2, hn2⟩, ⟨d2, hd2⟩, h2⟩
  dsimp only [Subtype.coe_mk] at *
  subst hdeg hnum hden
  congr

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

Goal state before:
pp: X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ Hom.opensFunctor f ⊣ Opens.map f.base

Tactic:
exact f.isOpenEmbedding.isOpenMap.adjunction

Goal state after:
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✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ (Quotient.mk'' y ^ n).val = val (Quotient.mk'' y) ^ n

Tactic:
rw [← mk_pow, val_mk, val_mk, Localization.mk_pow]

Goal state after:
ι : 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 𝒜
x : Submonoid A
y : NumDenSameDeg 𝒜 x
n : ℕ
⊢ Localization.mk ↑(y ^ n).num ⟨↑(y ^ n).den, ⋯⟩ = Localization.mk (↑y.num ^ n) (⟨↑y.den, ⋯⟩ ^ n)
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✝¹⁰ : AddCommMonoid ι
inst✝⁹ : DecidableEq ι
𝒜 : ι → σ
inst✝⁸ : GradedRing 𝒜
B : Type u_4
τ : Type u_5
inst✝⁷ : CommRing B
inst✝⁶ : SetLike τ B
inst✝⁵ : AddSubgroupClass τ B
ℬ : ι → τ
inst✝⁴ : GradedRing ℬ
C : Type u_6
ψ : Type u_7
inst✝³ : CommRing C
inst✝² : SetLike ψ C
inst✝¹ : AddSubgroupClass ψ C
𝒞 : ι → ψ
inst✝ : GradedRing 𝒞
P : Submonoid A
Q : Submonoid B
g : 𝒜 →+*ᵍ ℬ
comap_le : P ≤ Submonoid.comap g Q
x y : NumDenSameDeg 𝒜 P
e : embedding 𝒜 P x = embedding 𝒜 P y
⊢ (Setoid.ker (embedding ℬ Q)) { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }
    { deg := y.deg, num := ⟨g ↑y.num, ⋯⟩, den := ⟨g ↑y.den, ⋯⟩, den_mem := ⋯ }

Tactic:
apply_fun IsLocalization.map (Localization Q) g.toRingHom comap_le at e
      simp_rw [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk',
        IsLocalization.map_mk', ← Localization.mk_eq_mk'] at e
      exact e

Goal state after: