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

Goal state before:
pp: case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ (∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)) → IsLocallyNoetherian X

Tactic:
intro hCNoeth
    let fS i : X.affineOpens := ⟨Scheme.Hom.opensRange (𝒰.f i), isAffineOpen_opensRange _⟩
    apply isLocallyNoetherian_of_affine_cover (S := fS)
    · rw [← Scheme.OpenCover.iSup_opensRange 𝒰]
    intro i
    apply isNoetherianRing_of_ringEquiv (R := Γ(𝒰.X i, ⊤))
    apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
    exact IsOpenImmersion.ΓIsoTop (𝒰.f i)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsNoetherianRing ↑R
⊢ NoetherianSpace ↥(Spec R)

Tactic:
by
  convert! PrimeSpectrum.instNoetherianSpace (R := R)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P Q : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ IsIntegral Y → Subsingleton ↥Y → (P ⊓ Q) X ↔
    ((fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X) ⊓ fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → Q X) f

Tactic:
exact ⟨fun H ↦ ⟨(H · · |>.1), (H · · |>.2)⟩, fun H a b ↦ ⟨H.1 a b, H.2 a b⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝ : CommRing R
f : X ⟶ Spec (of R)
⊢ geometrically P f ↔
    ∀ ⦃K : Type u⦄ [inst : Field K] [inst_1 : Algebra R K] ⦃Y : Scheme⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec (of K)),
      IsPullback fst snd f (Spec.map (ofHom (algebraMap R K))) → P Y

Tactic:
refine ⟨fun hs K _ _ Z fst snd h ↦ hs _ _ _ h, fun H K _ y Z fst snd h ↦ ?_⟩
  obtain ⟨φ, rfl⟩ := Spec.map_surjective y
  algebraize [φ.hom]
  exact H fst snd h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
⊢ IsSchemeTheoreticallyDominant g

Tactic:
isSchemeTheoreticallyDominant_iff_isDominant,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
⊢ IsDominant g
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : ↥S
hs : IsIrreducible {s}
⊢ IsIrreducible (⇑f ⁻¹' {s})

Tactic:
← f.range_fiberι,

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : ↥S
hs : IsIrreducible {s}
⊢ IsIrreducible (Set.range ⇑(fiberι f s))
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y✝ : Scheme
f✝ : X ⟶ Y✝
S : CommRingCat
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
f : Spec S ⟶ Y
hY : ∃ K, Y = Spec K ∧ IsField ↑K
⊢ UniversallyOpen f

Tactic:
obtain ⟨K, rfl, hK⟩ := hY

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
f : Spec S ⟶ Spec K
⊢ UniversallyOpen f
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this : Algebra R S := ⋯
⊢ ∀ (r_1 : ↑s), ∃ n, ↑r_1 ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
rintro ⟨t, ht⟩

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
⊢ (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom

Tactic:
ext1

Goal state after:
case hC
n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
⊢ ((CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom).comp C =
    ((CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom).comp C

case hX
n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
i✝ : n
⊢ ((CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom) (X i✝) =
    ((CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom) (X i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
⊢ f ≫ homOfVector g v = homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v)

Tactic:
ext1

Goal state after:
case h₁
n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
⊢ (f ≫ homOfVector g v) ≫ 𝔸(n; S) ↘ S =
    homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v) ≫ 𝔸(n; S) ↘ S

case h₂
n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (f ≫ homOfVector g v))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v))))
      (coord S i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (𝔸(n; S).toSpecΓ ≫
        Spec.map (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
      homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
        (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X) =
    𝟙 𝔸(n; S)

Tactic:
ext1

Goal state after:
case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ((𝔸(n; S).toSpecΓ ≫
          Spec.map (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
        homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
          (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X)) ≫
      𝔸(n; S) ↘ S =
    𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

case h₂
n : Type u
S : Scheme
inst✝ : IsAffine S
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ((𝔸(n; S).toSpecΓ ≫
              Spec.map
                (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
            homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ map n (𝟙 S) = 𝟙 𝔸(n; S)

Tactic:
ext1

Goal state after:
case h₁
n : Type u
S : Scheme
⊢ map n (𝟙 S) ≫ 𝔸(n; S) ↘ S = 𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

case h₂
n : Type u
S : Scheme
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (𝟙 S)))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) = map n f ≫ map n g

Tactic:
ext1

Goal state after:
case h₁
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) ≫ 𝔸(n; S'') ↘ S'' = (map n f ≫ map n g) ≫ 𝔸(n; S'') ↘ S''

case h₂
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (f ≫ g)))) (coord S'' i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n f ≫ map n g))) (coord S'' i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R S : CommRingCat
φ : R ⟶ S
⊢ (SpecIso n S).inv ≫ map n (Spec.map φ) =
    Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv

Tactic:
ext1

Goal state after:
case h₁
n : Type u
R S : CommRingCat
φ : R ⟶ S
⊢ ((SpecIso n S).inv ≫ map n (Spec.map φ)) ≫ 𝔸(n; Spec R) ↘ Spec R =
    (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv) ≫
      𝔸(n; Spec R) ↘ Spec R

case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ)))) (coord (Spec R) i✝) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)))
      (coord (Spec R) i✝)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ reindex id S = 𝟙 𝔸(n; S)

Tactic:
ext1

Goal state after:
case h₁
n : Type u
S : Scheme
⊢ reindex id S ≫ 𝔸(n; S) ↘ S = 𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

case h₂
n : Type u
S : Scheme
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex id S))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite

Tactic:
obtain ⟨t₁, ht₁⟩ := hf.2 z hz

Goal state after:
case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : Zero Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ ∀ z ∈ V, ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ if hz : z ∈ V then D z else 0).Finite

Tactic:
by
    intro z hz
    obtain ⟨t, ht⟩ := D.supportLocallyFiniteWithinDomain z (h hz)
    use t, ht.1
    apply Set.Finite.subset (s := t ∩ D.support) ht.2
    intro _ _
    simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
⊢ f.restrict f.domain ⋯ ⋯ = f

Tactic:
ext1

Goal state after:
case e
X Y : Scheme
f : X.PartialMap Y
⊢ (f.restrict f.domain ⋯ ⋯).domain = f.domain

case H
X Y : Scheme
f : X.PartialMap Y
⊢ (f.restrict f.domain ⋯ ⋯).hom = (X.isoOfEq ?e).hom ≫ f.hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
V : X.Opens
hV : Dense ↑V
hV' : V ≤ U
⊢ (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV ⋯

Tactic:
ext1

Goal state after:
case e
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
V : X.Opens
hV : Dense ↑V
hV' : V ≤ U
⊢ ((f.restrict U hU hU').restrict V hV hV').domain = (f.restrict V hV ⋯).domain

case H
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
V : X.Opens
hV : Dense ↑V
hV' : V ≤ U
⊢ ((f.restrict U hU hU').restrict V hV hV').hom = (X.isoOfEq ?e).hom ≫ (f.restrict V hV ⋯).hom
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ f.restrict W hW hWl = g.restrict W hW hWr

Tactic:
ext1

Goal state after:
case e
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ (f.restrict W hW hWl).domain = (g.restrict W hW hWr).domain

case H
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
⊢ (f.restrict W hW hWl).hom = (X.isoOfEq ?e).hom ≫ (g.restrict W hW hWr).hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ f.comp (Hom.toPartialMap g) = f.compHom g

Tactic:
ext1

Goal state after:
case e
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (f.comp (Hom.toPartialMap g)).domain = (f.compHom g).domain

case H
X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ (f.comp (Hom.toPartialMap g)).hom = (X.isoOfEq ?e).hom ≫ (f.compHom g).hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (PartialMap.id X).comp f = f

Tactic:
ext1

Goal state after:
case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).domain = f.domain

case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ((PartialMap.id X).comp f).hom = (X.isoOfEq ?e).hom ≫ f.hom
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i : 𝒰.I₀
⊢ IsOpenImmersion.lift (𝒰.f i) (𝒰.f i) ⋯ = 𝟙 (𝒰.X i)

Tactic:
by rw [← cancel_mono (𝒰.f i)]; simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case h.refine_1
J : Type u_1
inst✝² : Category.{u_2, u_1} J
F G : J ⥤ Scheme
s : F ⟶ G
inst✝¹ : Quiver.IsThin J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective ⇑(F.map hij)
inst✝ : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq : (ConcreteCategory.hom (↾⇑(F.map fi))) xi = (ConcreteCategory.hom (↾⇑(F.map fj))) xj
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi : (ConcreteCategory.hom ((G ⋙ forget).map fli)) x = (s.app i) xi
hj : (ConcreteCategory.hom ((G ⋙ forget).map flj)) x = (s.app j) xj
e : F.obj l ≅ pullback (s.app i) (G.map fli) := ⋯.isoPullback
z : ↥(pullback (s.app i) (G.map fli))
h1 : (pullback.fst (s.app i) (G.map fli)) z = xi
h2 : (pullback.snd (s.app i) (G.map fli)) z = x
⊢ (ConcreteCategory.hom ((F ⋙ forget).map fli)) (e.inv z) = xi

Tactic:
simp [← h1, ← Scheme.Hom.comp_apply, e]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : c.val i = 1
⊢ 0 i < (c.val i).degree.succ

Tactic:
simp [hi']

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
deg_bound₂ : c'.degBound < c.degBound
⊢ (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound * c.degBound ^ c'.degBound

Tactic:
gcongr
            delta InductionObj.degBound
            exact Finset.single_le_sum (f := fun i ↦ (c.val i).degree.succ)
              (by intros; positivity) (Finset.mem_univ _)

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ (g a ≫ f a) ≫ EffectiveEpiFamily.desc X f (fun a ↦ i a ≫ e a) ⋯ = e a

Tactic:
simp only [Category.assoc, EffectiveEpiFamily.fac]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ g a ≫ i a ≫ e a = e a
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.252} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.252} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
a : J
⊢ d.gluedCocone.ι.app a ≫
      {
        toCommaMorphism :=
          𝒱.glueMorphismsOverOfLocallyDirected
            (fun i ↦
              ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                pullback.fst s.pt.hom (𝒰.f i))
            ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } =
    s.ι.app a

Tactic:
let 𝒲 (a : J) : (D.obj a).left.OpenCover := 𝒰.pullback₁ (D.obj a).hom

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.397} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.397} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
a : J
𝒲 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
⊢ d.gluedCocone.ι.app a ≫
      {
        toCommaMorphism :=
          𝒱.glueMorphismsOverOfLocallyDirected
            (fun i ↦
              ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
                pullback.fst s.pt.hom (𝒰.f i))
            ⋯ ⋯,
        prop_hom_left := trivial, prop_hom_right := trivial } =
    s.ι.app a
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.polynomial =
    { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly

Tactic:
polynomial,

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
⊢ Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) =
    { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W.map f).polynomial = Polynomial.map (mapRingHom f) W.polynomial

Tactic:
simp only [polynomial]
  map_simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄B).polynomial = Polynomial.map (mapRingHom ↑f) (W⁄A).polynomial

Tactic:
rw [← map_polynomial, map_baseChange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.negY x (W'.negY x y) = y

Tactic:
simp only [negY]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ -(-y - W'.a₁ * x - W'.a₃) - W'.a₁ * x - W'.a₃ = y