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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU =
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f

Tactic:
← X.presheaf.germ_res (homOfLE hVU) x hxV,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (X.presheaf.map (homOfLE hVU).op ≫ X.presheaf.germ V x hxV) ≫
      Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU =
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ x ∈ (Opens.map f.base).obj ⊤

Tactic:
simp only [Opens.map_top]; trivial

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
a : ↑(Y.presheaf.obj (op ⊤))
⊢ x ∈ (Opens.map f.base).obj ⊤

Tactic:
simp only [Opens.map_top]; trivial

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case e_a
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : f (closedPoint ↑R) ∈ U
⊢ (Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint ↑R) hU =
    (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op).hom ≫ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Tactic:
simp only [Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
    TopCat.Presheaf.germ_res]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Set.range ⇑f ⊆ ↑(ker f).support

Tactic:
rintro _ ⟨x, rfl⟩
  obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
  refine ((coe_support_inter f.ker ⟨U, hU⟩).ge ⟨?_, hxU⟩).1
  simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]
  intro s hs hxs
  have : x ∈ f ⁻¹ᵁ Y.basicOpen s := hxs
  rwa [Scheme.preimage_basicOpen, RingHom.mem_ker.mp (f.ideal_ker_le _ hs),
    Scheme.basicOpen_zero] at this

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueData.ι U) = Set.range ⇑(I.gluedTo ⁻¹ᵁ ↑U).ι

Tactic:
by
    simp only [Scheme.Opens.range_ι, TopologicalSpace.Opens.map_coe, range_glueData_ι]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
t✝ : Set S
r : ↑↑s
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))

Tactic:
obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
    multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R))
      (Localization.Away (r : R)) (s₁ r : Set (Localization.Away r.val ⊗[R] S))
      (algebraMap S _ x) (by rw [s₂ r]; trivial)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
s₁ : (r : ↥s) → Finset (Localization.Away ↑r ⊗[R] S)
s₂ : ∀ (r : ↥s), adjoin (Localization.Away ↑r) ↑(s₁ r) = ⊤
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)
x : S
t✝ : Set S
r : ↑↑s
n₁ : ℕ
hn₁ : ⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ • (algebraMap S (Localization.Away ↑r ⊗[R] S)) x ∈ adjoin R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ Subalgebra.toSubmodule (⨆ x, adjoin R ↑(sf x))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ (∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))) → IsNoetherian X

Tactic:
intro h
    convert! IsNoetherian.mk
    · exact isLocallyNoetherian_of_affine_cover hS h
    · constructor
      rw [← Opens.coe_top, ← hS, Opens.iSup_mk]
      apply isCompact_iUnion
      intro i
      apply isCompact_iff_isCompact_univ.mpr
      convert! CompactSpace.isCompact_univ
      have : NoetherianSpace (S i) := by
        apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2
      apply NoetherianSpace.compactSpace (S i)

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)
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
⊢ geometrically P f

Tactic:
rw [geometrically_iff_of_isClosedUnderIsomorphisms]

Goal state after:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝¹ : CommRing R
f : X ⟶ Spec (of R)
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
⊢ ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Spec (of R)), P (pullback f y)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderComposition @UniversallyClosed

Tactic:
by
  rw [universallyClosed_eq]
  infer_instance

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]
    simp_rw [this, forall_and]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝¹ : Subsingleton ↥Y
inst✝ : IsIntegral Y
⊢ Flat (f ≫ Y.isoSpec.hom)

Tactic:
refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ ?_

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝¹ : Subsingleton ↥Y
inst✝ : IsIntegral Y
i : X.affineCover.I₀
⊢ Flat (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑f ∘ ⇑(pullback.snd (𝒰.f i) f) ⁻¹' s)

Tactic:
Set.preimage_comp

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(pullback.snd (𝒰.f i) f) ⁻¹' ⇑f ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
x✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ IsOpen (⇑f ∘ ⇑((∐ fun i ↦ 𝒰.X i).isoSpec.inv ≫ p) ⁻¹' s)

Tactic:
Set.preimage_comp

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R)),
    IsOpen (⇑f ⁻¹' s) → (∃ S, X = Spec S) → IsOpen s
hX : ¬∃ S, X = Spec S
x✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun i ↦ 𝒰.X i) ⟶ X := Sigma.desc fun i ↦ 𝒰.f i
⊢ IsOpen (⇑((∐ fun i ↦ 𝒰.X i).isoSpec.inv ≫ p) ⁻¹' ⇑f ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
⊢ (SpecIso n R).inv ≫ 𝔸(n; Spec R) ↘ Spec R = Spec.map (CommRingCat.ofHom C)

Tactic:
simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, Scheme.Spec_map,
    Quiver.Hom.unop_op, Category.assoc, isoOfIsAffine_inv_over, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]
  congr 1
  rw [Iso.inv_comp_eq]
  ext : 2
  exact map_C _ _

Goal state after:
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
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
have h : iSup D.obj = UX := by
    refine le_antisymm (iSup_le_iff.mpr ?_) ?_
    · subst hVU; rintro (i | ⟨i, j⟩); exacts [le_iSup VX _, inf_le_left.trans (le_iSup VX _)]
    · subst hVU; exact iSup_le_iff.mpr fun i ↦ le_iSup D.obj (.single i)

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
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
⊢ IsIso (pushoutSection H hUST hUSX hUY)
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ (f₁.representative.comp f₂.representative).equiv
    (f₁.representative.comp f₂.representative.toRationalMap.representative)

Tactic:
apply PartialMap.comp_equiv_of_equiv_right

Goal state after:
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ f₂.representative.equiv f₂.representative.toRationalMap.representative
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)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
⊢ ⋃ i, f ((fun i ↦ ↑i.fst) i) '' ↑((fun i ↦ ↑i.snd) i) = U

Tactic:
← hunion

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
σ : Type (max u_2 u_3) := (i : ↑s) × ↑(Us i)
this✝ : Finite ↑s
this : ∀ (i : ↑s), Finite ↑(Us i)
⊢ ⋃ i, f ((fun i ↦ ↑i.fst) i) '' ↑((fun i ↦ ↑i.snd) i) = ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_2
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
⊢ ∀ (C : BasicConstructibleSetData R),
    ∀ x ∈ S, C ∈ f x → C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound

Tactic:
intro x y hy hx

Goal state after:
case refine_2
R : Type u_6
inst✝ : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : BasicConstructibleSetData R[X] → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g }.val) \ zeroLocus {C.f}) = (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C, ∀ (i : Fin C_1.n), C_1.g i ∈ coeffSubmodule ℤ { val := C.g } ^ { val := C.g }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
⊢ x.n ≤ S.degBound ∧ ∀ (i : Fin x.n), x.g i ∈ M ^ S.degBound ^ S.degBound
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ W'.addPolynomial x y ℓ =
    -{ a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
          c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
          d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.toPoly

Tactic:
by
  rw [addPolynomial, linePolynomial, polynomial, Cubic.toPoly]
  eval_simp
  C_simp
  ring1

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
⊢ Associated ((Algebra.norm R) f) (LinearMap.det ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))))

Tactic:
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
⊢ ∀ (x : S),
    ((Matrix.toLin b' b') (Matrix.diagonal (smithCoeffs b (span {f}) ⋯))) x = (↑(Algebra.lmul R S).toRingHom f) (e x)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
p q r s : ℤ
⊢ W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
      W (q + r + s) * W (q - r) * W (p + s) * W p =
    W ((2 * p + 2 * q + (s + s)).tdiv 2) * W ((2 * p + s - (2 * q + s)).tdiv 2) *
          (W ((2 * r + s + s).tdiv 2) * W ((2 * r + s - s).tdiv 2)) -
        W ((2 * p + 2 * r + (s + s)).tdiv 2) * W ((2 * p + s - (2 * r + s)).tdiv 2) *
          (W ((2 * q + s + s).tdiv 2) * W ((2 * q + s - s).tdiv 2)) +
      W ((2 * p + s + s).tdiv 2) * W ((2 * p + s - s).tdiv 2) *
        (W ((2 * q + 2 * r + (s + s)).tdiv 2) * W ((2 * q + s - (2 * r + s)).tdiv 2))

Tactic:
add_assoc _ s,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
p q r s : ℤ
⊢ W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
      W (q + r + s) * W (q - r) * W (p + s) * W p =
    W ((2 * p + 2 * q + (s + s)).tdiv 2) * W ((2 * p + s - (2 * q + s)).tdiv 2) *
          (W ((2 * r + (s + s)).tdiv 2) * W ((2 * r + s - s).tdiv 2)) -
        W ((2 * p + 2 * r + (s + s)).tdiv 2) * W ((2 * p + s - (2 * r + s)).tdiv 2) *
          (W ((2 * q + (s + s)).tdiv 2) * W ((2 * q + s - s).tdiv 2)) +
      W ((2 * p + (s + s)).tdiv 2) * W ((2 * p + s - s).tdiv 2) *
        (W ((2 * q + 2 * r + (s + s)).tdiv 2) * W ((2 * q + s - (2 * r + s)).tdiv 2))
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_2
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)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : ReflectsFilteredColimits (forget CommRingCat)
⊢ ∀ (i : Iᵒᵖ) (x y : (fun X ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).ι.app i)) x =
        (ConcreteCategory.hom (((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).ι.app i)) y →
      ∃ k f,
        (ConcreteCategory.hom (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).map f)) x =
          (ConcreteCategory.hom (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).map f)) y

Tactic:
exact fun i s t e ↦ ⟨_, Quiver.Hom.op _,
      (exists_app_map_eq_map_of_isLimit _ _ hc isCompact_univ s t e).choose_spec.choose_spec⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.preΨ₄.natDegree ≤ 6

Tactic:
by
  rw [preΨ₄]
  compute_degree

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.Δ = -W.a₄ ^ 3

Tactic:
rw [Δ_of_isShortNF]
  linear_combination (-21 * W.a₄ ^ 3 - 144 * W.a₆ ^ 2) * CharP.cast_eq_zero R 3

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case even
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ (W.preΨ' (2 * (m + 3))).natDegree ≤ expDegree (2 * (m + 3)) ∧
    (W.preΨ' (2 * (m + 3))).coeff (expDegree (2 * (m + 3))) = ↑(expCoeff (2 * (m + 3)))

Tactic:
constructor
    · nth_rw 1 [preΨ'_even, ← max_self <| expDegree _, (expDegree_rec m).1.1, (expDegree_rec m).1.2]
      exact natDegree_sub_le_of_le (dm (dm (dp h₂.1) h₃.1) h₅.1) (dm (dm h₁.1 h₃.1) (dp h₄.1))
    · nth_rw 1 [preΨ'_even, coeff_sub, (expDegree_rec m).1.1, cm (dm (dp h₂.1) h₃.1) h₅.1,
        cm (dp h₂.1) h₃.1, cp h₂.1, h₂.2, h₃.2, h₅.2, (expDegree_rec m).1.2,
        cm (dm h₁.1 h₃.1) (dp h₄.1), cm h₁.1 h₃.1, h₁.2, cp h₄.1, h₃.2, h₄.2, (expCoeff_rec m).1]
      norm_cast

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P x * Q z ^ 2 = Q x * P z ^ 2

Tactic:
rcases h with ⟨u, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext]
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P y * Q z ^ 3 = Q y * P z ^ 3

Tactic:
rcases h with ⟨u, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext]
  ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : Nontrivial R
h : 3 * 1 ^ 2 = 0 ∧ 2 * 1 = 0 ∧ W'.a₁ * 1 * 1 = 0
⊢ 1 = 0

Tactic:
by linear_combination (norm := ring1) h.1 - h.2.1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
⊢ P y ≠ 0

Tactic:
intro hPy

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
hPx : P x ≠ 0
hPy : P y = 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, (-(P y / P x)) ^ 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]

Tactic:
Odd.neg_pow <| by decide,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, -(P y / P x) ^ 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A}, U ∈ {U | ∃ i, U = ↑(B i)} → ∃ V ∈ {U | ∃ i, U = ↑(B i)}, V ⊆ (fun x ↦ x₀ + x + -x₀) ⁻¹' U

Tactic:
by
    rintro x₀ _ ⟨i, rfl⟩
    use B i
    constructor
    · use i
    · simp

Goal state after: