mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
this : ∃ n_1 i, (e.val i).degree = ↑n_1 ∧ e.val i ≠ 0
m : ℕ := Nat.find this
i : Fin n
hi : (e.val i).degree = ↑m
hi' : e.val i ≠ 0
⊢ ∃ i, e.val i ≠ 0 ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree

Tactic:
refine ⟨i, hi', fun j hj ↦ ?_⟩

Goal state after:
n : ℕ
P : (R : Type u) → [inst : CommRing R] → InductionObj R n → Prop
hP₁ : ∀ (R : Type u) [inst : CommRing R], P R { val := 0 }
hP₂ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic → (∀ (j : Fin n), j ≠ i → e.val j = 0) → P R e
hP₃ :
  ∀ (R : Type u) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree → i ≠ j → P R { val := Function.update e.val j (e.val j %ₘ e.val i) } → P R e
hP₄ :
  ∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        P (Away c)
            { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom (algebraMap R (Away c))) ∘ e.val } →
          P (R ⧸ Ideal.span {c}) { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘ e.val } → P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n), y = e.degree → P R e
R : Type u
inst✝ : CommRing R
e : InductionObj R n
hv : v = e.degree
h✝ : Nontrivial R
he0 : ∃ x, ¬e.val x = 0
H : ¬∃ i, (e.val i).Monic ∧ ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
this : ∃ n_1 i, (e.val i).degree = ↑n_1 ∧ e.val i ≠ 0
m : ℕ := Nat.find this
i : Fin n
hi : (e.val i).degree = ↑m
hi' : e.val i ≠ 0
j : Fin n
hj : e.val j ≠ 0
⊢ (e.val i).degree ≤ (e.val j).degree
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
let ψY : Γ(Y, UY) →+* Π i, Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) := RingHom.pi fun i ↦
      (Y.presheaf.map (homOfLE (by subst hUY hVU; gcongr; exact le_iSup _ _)).op).hom

Goal state after:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
ι : Type u_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
⊢ Mono (pushoutSection H hUST hUSX hUY)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
⊢ f (Classical.arbitrary I) ≫ cF.π.app j = s.π.app j

Tactic:
this _ j

Goal state after:
I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
⊢ f j ≫ cF.π.app j = s.π.app j
Module: Mathlib.AlgebraicGeometry.AffineSpace

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

Tactic:
apply ext_of_isAffine

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

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f✝ : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f✝.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : I → (cG.pt ⟶ s.pt) := fun i ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
⊢ cG.ι.app j ≫ f (Classical.arbitrary I) = s.ι.app j

Tactic:
this _ j

Goal state after:
I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f✝ : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f✝.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : I → (cG.pt ⟶ s.pt) := fun i ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
⊢ cG.ι.app j ≫ f j = s.ι.app j
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S T : Scheme
f : S ⟶ T
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n f))) (coord T i) = (toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i

Tactic:
map_appTop_coord,

Goal state after:
n : Type u
S T : Scheme
f : S ⟶ T
i : n
⊢ coord S i = (toSpecMvPolyIntEquiv n) (toSpecMvPoly n S) i
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
⊢ {i | ({↑i} ∩ t).Nonempty}.Finite ↔ (t ∩ support f).Finite

Tactic:
have aux1 : t ∩ f.support = {i : f.support | ↑i ∈ t} := by aesop

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
f : X → Y
z : X
t : Set X
ht : t ∈ 𝓝 z
aux1 : t ∩ support f = Subtype.val '' {i | ↑i ∈ t}
⊢ {i | ({↑i} ∩ t).Nonempty}.Finite ↔ (t ∩ support f).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z).Finite

Tactic:
obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeSup Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊔ D₂ z).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z).Finite

Tactic:
obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : SemilatticeInf Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ D₁.support).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ D₂.support).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support fun z ↦ D₁ z ⊓ D₂ z).Finite
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)

pp: case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))

Tactic:
· rw [← basicOpen_eq_of_affine]
    exact (isAffineOpen_top (Spec R)).basicOpen _

Goal state after:
case refine_2
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ Function.Injective ⇑(ConcreteCategory.hom ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf))
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case e_a
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this : Mono (X.presheaf.germ U x hxU)
⊢ Scheme.Hom.appLE f V U ⋯ = Scheme.Hom.appLE g V U ⋯

Tactic:
← cancel_mono (X.presheaf.germ U x hxU)

Goal state after:
case e_a
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : f x = g x
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : f x ∈ ↑V
hxV' : g x ∈ V
U : X.Opens
hxU : x ∈ U
left✝ : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hxU))
this✝ : IsAffine ↑V
this : Mono (X.presheaf.germ U x hxU)
⊢ Scheme.Hom.appLE f V U ⋯ ≫ X.presheaf.germ U x hxU = Scheme.Hom.appLE g V U ⋯ ≫ X.presheaf.germ U x hxU
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case e'_2.e'_4
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := Finset.image (fun x ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun x ↦ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }) T₂
⊢ comap (mapRingHom q₁.toRingHom) ⁻¹' (zeroLocus (Set.range e.val) \ zeroLocus {f}) =
    zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}

Tactic:
dsimp only [e₁]
        rw [Set.preimage_sdiff, preimage_comap_zeroLocus, preimage_comap_zeroLocus,
          Set.image_singleton, Pi.smul_def, ← Set.smul_set_range, Set.range_comp]
        congr 1
        refine (PrimeSpectrum.zeroLocus_smul_of_isUnit (.map _ ?_) _).symm
        exact isUnit_iff_exists_inv'.mpr ⟨_, IsLocalization.Away.mul_invSelf c⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (PartialMap.id X).compHom f = Hom.toPartialMap f

Tactic:
apply PartialMap.ext _ _ rfl
  simp

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

Goal state before:
pp: case e_a.e_a
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
x : ↥X
hx : x ∈ U
e : ⟨x, ⋯⟩ = (X.homOfLE hU') ⟨x, hx⟩
⊢ Hom.stalkMap f.domain.ι ⟨x, ⋯⟩ ≫ (↑f.domain).presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (X.homOfLE hU') ⟨x, hx⟩ =
    X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (X.homOfLE hU' ≫ f.domain.ι) ⟨x, hx⟩

Tactic:
rw [← Hom.stalkSpecializes_stalkMap_assoc, Hom.stalkMap_comp]

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

Goal state before:
pp: case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ ((f.comp g).comp h).hom = (X₁.isoOfEq ⋯).hom ≫ (f.comp (g.comp h)).hom

Tactic:
dsimp
    simp_rw [morphismRestrict_comp, morphismRestrict_ι_image_ι_isoImage_inv_assoc,
      Hom.comp_preimage, Category.assoc]
    conv_lhs => rw [← Category.assoc]
    conv_rhs => rw [← Category.assoc, ← Category.assoc, ← Category.assoc]
    congr 1
    simp [← cancel_mono (Opens.ι _)]

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
V : Opens (X i)
hV : IsCompact ↑V
⊢ IsCompactOpenCovered f (f i '' ↑V)

Tactic:
by
  refine ⟨{i}, Set.finite_singleton i, fun j hj ↦ hj ▸ V, by rintro i rfl; simpa, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.twoTorsionPolynomial.discr = 16 * W.Δ

Tactic:
by
  simp only [b₂, b₄, b₆, b₈, Δ, twoTorsionPolynomial, Cubic.discr]
  ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
h : W.c₄ = 0
⊢ W.j = 0

Tactic:
by
  rw [j_eq_zero_iff', h, zero_pow three_ne_zero]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆

Tactic:
equation_iff',

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ↔
    y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Equation 0 0

Tactic:
equation_iff',

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ↔
    (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Equation 0 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ∧ (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)

Tactic:
equation_iff',

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ∧
      (evalEval x y W.polynomialX ≠ 0 ∨ evalEval x y W.polynomialY ≠ 0) ↔
    y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ∧
      (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0

Tactic:
have H : (D.map (𝟙 _) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U := by simp

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
⊢ W.Nonsingular x₁ (W.slope x₁ x₂ y₁ y₂ * 0 + y₁)

Tactic:
mul_zero,

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
⊢ W.Nonsingular x₁ (0 + y₁)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field F
inst✝⁹ : Field K
W' : Affine R
inst✝⁸ : Algebra R S
inst✝⁷ : DecidableEq F
inst✝⁶ : DecidableEq K
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
x₁ x₂ y₁ y₂ : F
⊢ (W'⁄K).slope (↑f x₁) (↑f x₂) (↑f y₁) (↑f y₂) = ↑f ((W'⁄F).slope x₁ x₂ y₁ y₂)

Tactic:
← map_slope,

Goal state after:
R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field F
inst✝⁹ : Field K
W' : Affine R
inst✝⁸ : Algebra R S
inst✝⁷ : DecidableEq F
inst✝⁶ : DecidableEq K
inst✝⁵ : Algebra R F
inst✝⁴ : Algebra S F
inst✝³ : IsScalarTower R S F
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
x₁ x₂ y₁ y₂ : F
⊢ (W'⁄K).slope (↑f x₁) (↑f x₂) (↑f y₁) (↑f y₂) = ((W'⁄F).map ↑f).slope (↑f x₁) (↑f x₂) (↑f y₁) (↑f y₂)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ 1 + (mk W) (C (C (y⁻¹ * 4))) * 0 = 1

Tactic:
mul_zero,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ 1 + 0 = 1