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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit (↑f (UniversalFactorizationRing.presentation m k hn p).jacobian)

Tactic:
UniversalFactorizationRing.jacobian_resentation,

Goal state after:
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
q : { q // ↑q.1 * ↑q.2 = map (algebraMap R S) ↑p ∧ IsCoprime ↑q.1 ↑q.2 }
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) :=
  (UniversalFactorizationRing.homEquiv S m k hn p).symm ⟨↑q, ⋯⟩
a✝ : Nontrivial S
⊢ IsUnit
    (↑f
      ((-1) ^ n *
        (↑(UniversalFactorizationRing.factor₁ m k hn p)).resultant ↑(UniversalFactorizationRing.factor₂ m k hn p)))
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
⊢ IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩ =
    (Spec.map (Scheme.Hom.appLE f U V hUV)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩)

Tactic:
apply hU.isoSpec.inv.homeomorph.injective

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := ⋯
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
⊢ (Scheme.Hom.homeomorph (IsAffineOpen.isoSpec hU).inv) (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩) =
    (Scheme.Hom.homeomorph (IsAffineOpen.isoSpec hU).inv)
      ((Spec.map (Scheme.Hom.appLE f U V hUV)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩))
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsSeparated f
x : ↥X
s : ↥S
h : f x = s
hx : Scheme.Hom.QuasiFiniteAt f x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hUV : V ≤ f ⁻¹ᵁ U
this✝⁵ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FiniteType
algInst✝ : Algebra ↑Γ(S, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
algebraizeInst✝ : Algebra.FiniteType ↑Γ(S, U) ↑Γ(X, V)
this✝⁴ : (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
this✝³ : Algebra.QuasiFiniteAt (↑Γ(S, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
R : Type u
w✝⁷ : CommRing R
w✝⁶ : Algebra (↑Γ(S, U)) R
w✝⁵ : Algebra.Etale (↑Γ(S, U)) R
P : Ideal R
w✝⁴ : P.IsPrime
w✝³ : P.LiesOver (IsAffineOpen.primeIdealOf hU ⟨f x, hxU⟩).asIdeal
e : R ⊗[↑Γ(S, U)] ↑Γ(X, V)
w✝² : IsIdempotentElem e
P' : Ideal (R ⊗[↑Γ(S, U)] ↑Γ(X, V))
w✝¹ : P'.IsPrime
w✝ : P'.LiesOver P
hP' : Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
heP' : e ∉ P'
left✝ : Module.Finite R (Localization.Away e)
this✝² : (algebraMap R (Localization.Away e)).Finite
φ : Γ(S, U) ⟶ CommRingCat.of R := CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)
hφ : (CommRingCat.Hom.hom φ).Etale
this✝¹ : Etale (Spec.map φ)
e₁ : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ≅ pullback (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) :=
  (pullbackSpecIso (↑Γ(S, U)) R ↑Γ(X, V)).symm ≪≫
    pullbackSymmetry (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(S, U)) R)))
      (Spec.map (CommRingCat.ofHom (algebraMap ↑Γ(S, U) ↑Γ(X, V))))
he₁ :
  e₁.hom ≫ pullback.fst (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom)
g : Spec (CommRingCat.of (R ⊗[↑Γ(S, U)] ↑Γ(X, V))) ⟶ pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU) :=
  e₁.hom ≫
    pullback.map (Spec.map (Scheme.Hom.appLE f U V hUV)) (Spec.map φ) f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)
      (IsAffineOpen.fromSpec hV) (𝟙 (Spec (CommRingCat.of R))) (IsAffineOpen.fromSpec hU) ⋯ ⋯
W₁ : (pullback f (Spec.map φ ≫ IsAffineOpen.fromSpec hU)).Opens := g ''ᵁ PrimeSpectrum.basicOpen e
this✝ : IsFinite (W₁.ι ≫ pullback.snd f (Spec.map φ ≫ IsAffineOpen.fromSpec hU))
this : IsFinite W₁.ι
⊢ IsOpen (↑W₁)ᶜ

Tactic:
by simpa using W₁.ι.isClosedMap.isClosed_range

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 5 := finCongr ⋯
⊢ f.sylvesterDeriv.det * (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) =
    f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 -
        27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0

Tactic:
← Matrix.det_reindex_self e,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 3
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 5 := finCongr ⋯
⊢ ((Matrix.reindex e e) f.sylvesterDeriv).det * (-1) ^ (f.natDegree * (f.natDegree - 1) / 2) =
    f.coeff 2 ^ 2 * f.coeff 1 ^ 2 - 4 * f.coeff 3 * f.coeff 1 ^ 3 - 4 * f.coeff 2 ^ 3 * f.coeff 0 -
        27 * f.coeff 3 ^ 2 * f.coeff 0 ^ 2 +
      18 * f.coeff 3 * f.coeff 2 * f.coeff 1 * f.coeff 0
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: 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
b : ↥↑V
a : ↥W
h : ↑a ∉ V
this : W.ι ≫ (H.coconePointUniqueUpToIso (colimit.isColimit (pair ↑V ↑W))).hom = coprod.inr
hab :
  ι b =
    (W.ι ≫
        toNormalization (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)))).hom)
      a
⊢ ι b = (toNormalization (W.ι ≫ pullback.snd f fT) ≫ coprod.inr) a

Tactic:
simpa [-Scheme.Hom.comp_base, Scheme.Hom.normalizationCoprodIso,
            reassoc_of% this] using hab

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
⊢ IsOpen {x | QuasiFiniteAt f x}

Tactic:
isOpen_iff_forall_mem_open

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFiniteType f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f], IsAffineHom f → IsOpen {x | QuasiFiniteAt f x}
H : ¬IsAffineHom f
⊢ ∀ x ∈ {x | QuasiFiniteAt f x}, ∃ t ⊆ {x | QuasiFiniteAt f x}, IsOpen t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝¹ : IsNoetherian X
inst✝ : IrreducibleSpace ↥X
⊢ CategoryTheory.IsIso (X.irreducibleComponentι Z hZ)

Tactic:
have : CategoryTheory.IsIso (irreducibleComponentOpen X Z).ι := by
    rw [irreducibleComponentOpen_eq_top X Z hZ]
    exact X.topIso.isIso_hom
  rw [irreducibleComponentι, isIso_subschemeι_iff_eq_bot, irreducibleComponentIdeal_def,
    irreducibleComponentOpen_eq_top X Z hZ]
  exact X.topIso.hom.ker_eq_bot_of_isIso

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

Goal state before:
pp: R✝ R A : CommRingCat
inst✝¹ : Bialgebra ↑R ↑A
inst✝ : IsCocomm ↑R ↑A
⊢ (β_ ((Spec A).asOver (Spec R)) ((Spec A).asOver (Spec R))).hom ≫ μ = μ

Tactic:
ext
    have := congr((pullbackSpecIso R A A).hom ≫ ((bialgSpec R).map <| .op <| CommBialgCat.ofHom <|
      $(Bialgebra.comm_comp_comulBialgHom (R := R) (A := A))).hom.left)
    dsimp [commBialgCatEquivComonCommAlgCat] at this ⊢
    have h₁ : (Algebra.TensorProduct.includeRight : A →ₐ[R] A ⊗[R] A) =
      (RingHomClass.toRingHom (Bialgebra.TensorProduct.comm R A A)).comp
        Algebra.TensorProduct.includeLeftRingHom := rfl
    have h₂ : (Algebra.TensorProduct.includeLeftRingHom) =
      (RingHomClass.toRingHom (Bialgebra.TensorProduct.comm R A A)).comp
       (Algebra.TensorProduct.includeRight : A →ₐ[R] A ⊗[R] A) := rfl
    convert! this using 1
    simp only [mul_spec_asOver_spec_left, ← Category.assoc, algSpec, Equivalence.op_functor,
      comp_obj, op_obj, commAlgCatEquivUnder_functor_obj, Over.opEquivOpUnder_inverse_obj,
      CommRingCat.mkUnder_hom, Over.post_obj, Spec_obj, Over.mk_left, Over.mk_hom, Spec_map,
      Quiver.Hom.unop_op, Spec.map_comp]
    congr 1
    rw [← Iso.eq_comp_inv, Category.assoc, ← Iso.inv_comp_eq]
    ext
    · simp [AlgHom.toUnder, specOverSpec, over, OverClass.hom, h₁]; rfl
    · simp [AlgHom.toUnder, specOverSpec, over, OverClass.hom, h₂]; rfl

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

Goal state before:
pp: case hfst
X Y : Scheme
f : X ⟶ Y
inst✝³ : Flat f
inst✝² : QuasiCompact f
inst✝¹ : Surjective f
inst✝ : Mono f
⊢ isomorphisms Scheme (pullback.fst f f)

Tactic:
exact inferInstanceAs <| IsIso (pullback.fst f f)

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

Goal state before:
pp: X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
⊢ 1 ≤ finrank f (f x)

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
this :
  ∀ {X : Scheme} (x : ↥X) (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    (∃ S, X = Spec S) → 1 ≤ finrank f (f x)
hX : ¬∃ S, X = Spec S
⊢ 1 ≤ finrank f (f x)

X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
hX : ∃ S, X = Spec S
⊢ 1 ≤ finrank f (f x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
⊢ Surjective f

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f],
    1 ≤ finrank f → (∃ S, X = Spec S) → Surjective f
hX : ¬∃ S, X = Spec S
⊢ Surjective f

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : 1 ≤ finrank f
hX : ∃ S, X = Spec S
⊢ Surjective f
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
⊢ IsLocallyConstant (finrank f)

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    (∃ S, X = Spec S) → IsLocallyConstant (finrank f)
hX : ¬∃ S, X = Spec S
⊢ IsLocallyConstant (finrank f)

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : IsFinite f
inst✝ : LocallyOfFinitePresentation f
hX : ∃ S, X = Spec S
⊢ IsLocallyConstant (finrank f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
⊢ IsIso f

Tactic:
wlog hX : ∃ S, X = Spec S

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [IsFinite f], finrank f = 1 → (∃ S, X = Spec S) → IsIso f
hX : ¬∃ S, X = Spec S
⊢ IsIso f

X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝¹ : Flat f
inst✝ : IsFinite f
h : finrank f = 1
hX : ∃ S, X = Spec S
⊢ IsIso f
Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ @WeaklyEtale ≤ MorphismProperty.diagonal @WeaklyEtale

Tactic:
intro X

Goal state after:
W X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
⊢ ∀ ⦃Y : Scheme⦄ (f : X ⟶ Y), WeaklyEtale f → MorphismProperty.diagonal (@WeaklyEtale) f
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ Order.KrullDimLE 0 (PrimeSpectrum (R ⧸ span {x}))

Tactic:
Order.krullDimLE_iff,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ Order.krullDim (PrimeSpectrum (R ⧸ span {x})) ≤ ↑0
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ Submonoid.comap (valuation K (IsDiscreteValuationRing.maximalIdeal R)).toMonoidWithZeroHom ⊥ =
    Submonoid.map (algebraMap R K) (IsUnit.submonoid R)

Tactic:
exact IsDiscreteValuationRing.mker_valuation_eq_isUnitSubmonoid

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

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa only [Equiv.apply_symm_apply] using this

Goal state after:
B : Type u
inst✝¹ : Bicategory B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
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:
by
  ext1; exact (gc_ideal 𝒜).u_inf

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 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ ↑(basicOpen 𝒜 r) ↔ x ∈ (zeroLocus 𝒜 {r})ᶜ

Tactic:
by simp only [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]; rfl

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 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) ↑⟨c, ht'⟩ *
      (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑g.den * ↑f.num) =
    (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) ↑⟨c, ht'⟩ *
      (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑f.den * ↑g.num)

Tactic:
← map_mul,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑⟨c, ht'⟩ * (↑g.den * ↑f.num)) =
    (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) ↑⟨c, ht'⟩ *
      (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑f.den * ↑g.num)
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 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑⟨c, ht'⟩ * (↑g.den * ↑f.num)) =
    (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) ↑⟨c, ht'⟩ *
      (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑f.den * ↑g.num)

Tactic:
← map_mul,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑⟨c, ht'⟩ * (↑g.den * ↑f.num)) =
    (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑⟨c, ht'⟩ * (↑f.den * ↑g.num))
Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
⊢ (pullbackComp f (g ≫ h)).inv ≫
      Functor.whiskerRight (pullbackComp g h).inv (pullback f) ≫
        ((pullback h).associator (pullback g) (pullback f)).hom ≫
          (pullback h).whiskerLeft (pullbackComp f g).hom ≫ (pullbackComp (f ≫ g) h).hom =
    eqToHom ⋯

Tactic:
let e₄ := pullbackComp (f ≫ g) h

Goal state after:
X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
e₄ : pullback h ⋙ pullback (f ≫ g) ≅ pullback ((f ≫ g) ≫ h) := pullbackComp (f ≫ g) h
⊢ (pullbackComp f (g ≫ h)).inv ≫
      Functor.whiskerRight (pullbackComp g h).inv (pullback f) ≫
        ((pullback h).associator (pullback g) (pullback f)).hom ≫
          (pullback h).whiskerLeft (pullbackComp f g).hom ≫ (pullbackComp (f ≫ g) h).hom =
    eqToHom ⋯
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
this : (Hom.opensFunctor f ⋙ Opens.map f.base).IsContinuous (Opens.grothendieckTopology ↥X)
  (Opens.grothendieckTopology ↥X) :=
  Functor.isContinuous_comp (Hom.opensFunctor f) (Opens.map f.base) (Opens.grothendieckTopology ↥X)
    (Opens.grothendieckTopology ↥Y) (Opens.grothendieckTopology ↥X)
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
x : ↑(X.ringCatSheaf.obj.obj U)
⊢ (RingCat.Hom.hom
        ((({
                    hom :=
                      Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                        (forget₂ CommRingCat RingCat) } ≫
                  ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
                        (Opens.grothendieckTopology ↥Y)).map
                    (Hom.toRingCatSheafHom f)) ≫
                (Functor.sheafPushforwardContinuousNatTrans (NatIso.ofComponents (fun U ↦ eqToIso ⋯) ⋯).hom RingCat
                      (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X)).app
                  X.ringCatSheaf).hom.app
          U))
      x =
    (RingCat.Hom.hom ((𝟙 X.ringCatSheaf).hom.app U)) x

Tactic:
exact
      congr($(f.appIso_inv_app_presheafMap U.unop) x)

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

Goal state before:
pp: case refine_1
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
⊢ Functor.whiskerRight (NatTrans.op ⋯.adjunction.counit) Y.ringCatSheaf.obj =
    (Hom.toRingCatSheafHom f).hom ≫
      (Opens.map f.base).op.whiskerLeft
        {
            hom :=
              Functor.whiskerRight { app := fun U ↦ (Hom.appIso f (Opposite.unop U)).inv, naturality := ⋯ }
                (forget₂ CommRingCat RingCat) }.hom

Tactic:
ext U x; exact congr($((f.app_appIso_inv _).symm).hom x)

Goal state after: