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

Goal state before:
pp: X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
⊢ ↑(∏ x ∈ s.attach, f ↑x ⋯) * x = 0

Tactic:
mul_comm,

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
⊢ x * ↑(∏ x ∈ s.attach, f ↑x ⋯) = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
i : ↑R
hi : i ∈ ↑s
⊢ i * ↑(∏ x ∈ s.attach, f ↑x ⋯) = 0

Tactic:
mul_comm,

Goal state after:
X Y S : Scheme
f✝ : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R✝ A : CommRingCat
inst✝ : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing ↑R
I : Ideal ↑R
hI : I.IsPrime
J : Ideal ↑R := RingHom.ker (algebraMap (↑R) (Localization.AtPrime I))
hJ : ∀ (x : ↑R), x ∈ J ↔ ∃ y, ↑y * x = 0
f : (x : ↑R) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : ↑R) (a : x ∈ J), ↑(f x a) * x = 0
s : Finset ↑R
hs : Ideal.span ↑s = J
hs' : ↑s ⊆ ↑J
x y : ↑R
e : y * x = 0
hy : y ∉ I
i : ↑R
hi : i ∈ ↑s
⊢ ↑(∏ x ∈ s.attach, f ↑x ⋯) * i = 0
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g : X.PartialMap Y
⊢ f.equiv g → g.equiv f

Tactic:
intro ⟨W, hW, hWl, hWr, e⟩
  exact ⟨W, hW, hWr, hWl, e.symm⟩

Goal state after:
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✝³ : IsCofilteredOrEmpty I
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), Nonempty ↥(D.obj i)
inst✝ : ∀ (i : I), CompactSpace ↥(D.obj i)
h✝ : Nonempty I
i : I
this✝ : IsCofiltered I
𝒰 : (D.obj i).OpenCover := (D.obj i).affineCover.finiteSubcover
this : ∀ (i' : 𝒰.I₀), IsAffine (𝒰.X i')
i' : 𝒰.I₀ → I
f : (j : 𝒰.I₀) → i' j ⟶ i
hf : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (f j)) 𝒰).X j)
g : (j : I) →
  j ∈ insert i (Finset.image i' Finset.univ) →
    (IsCofiltered.inf (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ⟶
      j) :=
  fun j ↦
    IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
      (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ)
j : 𝒰.I₀
⊢ D.map (g i ⋯) ≫ 𝟙 (D.obj i) =
    D.map
      (IsCofiltered.infTo (insert i (Finset.image i' Finset.univ))
        (Finset.image (fun j ↦ ⟨i' j, ⟨i, ⟨⋯, ⟨⋯, f j⟩⟩⟩⟩) Finset.univ) ?mY)

Tactic:
simp [g]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this✝ : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
q : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ pullback f f := pullback.lift g₁ g₂ ⋯
q_fst : q ≫ pullback.fst f f = g₁
q_snd : q ≫ pullback.snd f f = g₂
u : ↥X
hu : (pullback.diagonal f) u = q (IsLocalRing.closedPoint ↑(CommRingCat.of (AlgebraicClosure ↑(X.residueField x))))
this :
  (pullback.fst f f) ((pullback.diagonal f) u) =
    (pullback.fst f f) (q (IsLocalRing.closedPoint ↑(CommRingCat.of (AlgebraicClosure ↑(X.residueField x)))))
⊢ u = x

Tactic:
rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply] at this

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this✝ : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
q : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ pullback f f := pullback.lift g₁ g₂ ⋯
q_fst : q ≫ pullback.fst f f = g₁
q_snd : q ≫ pullback.snd f f = g₂
u : ↥X
hu : (pullback.diagonal f) u = q (IsLocalRing.closedPoint ↑(CommRingCat.of (AlgebraicClosure ↑(X.residueField x))))
this :
  (pullback.diagonal f ≫ pullback.fst f f) u =
    (q ≫ pullback.fst f f) (IsLocalRing.closedPoint ↑(CommRingCat.of (AlgebraicClosure ↑(X.residueField x))))
⊢ u = x
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
I : Type u
inst✝⁷ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : IsAffine X
inst✝³ : ∀ (i : I), IsAffine (D.obj i)
inst✝² : IsAffine c.pt
i : I
a : D.obj i ⟶ X
j : I
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsAffine (Spec R)
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
this :
  ∀ {X : Scheme} [IsAffine X] (a : D.obj i ⟶ X) (b : D.obj j ⟶ X),
    c.π.app i ≫ a = c.π.app j ≫ b →
      ∀ (f : X ⟶ Spec R) [LocallyOfFiniteType f],
        t.app i = a ≫ f → t.app j = b ≫ f → (∃ S, X = Spec S) → ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
hX : ¬∃ S, X = Spec S
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

pp: I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
X : Scheme
inst✝¹ : IsAffine X
a : D.obj i ⟶ X
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hX : ∃ S, X = Spec S
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b

Tactic:
· simpa using! this (a ≫ X.isoSpec.hom) (b ≫ X.isoSpec.hom) (by simp [hab]) (X.isoSpec.inv ≫ f)
      (by simp [ha]) (by simp [hb]) ⟨_, rfl⟩

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝⁵ : IsCofiltered I
inst✝⁴ : ∀ (i : I), IsAffine (D.obj i)
inst✝³ : IsAffine c.pt
i j : I
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝² : IsAffine (Spec R)
X : Scheme
inst✝¹ : IsAffine X
a : D.obj i ⟶ X
b : D.obj j ⟶ X
hab : c.π.app i ≫ a = c.π.app j ≫ b
f : X ⟶ Spec R
inst✝ : LocallyOfFiniteType f
ha : t.app i = a ≫ f
hb : t.app j = b ≫ f
hX : ∃ S, X = Spec S
⊢ ∃ k hik hjk, D.map hik ≫ a = D.map hjk ≫ b
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)
U : Set S
inst✝ : Unique ι
⊢ IsCompactOpenCovered f U ↔ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U

Tactic:
refine ⟨fun ⟨s, hs, V, hc, hcov⟩ ↦ ?_, fun ⟨V, hc, h⟩ ↦ ?_⟩
  · cases s.eq_empty_or_singleton_of_unique <;> aesop
  · refine ⟨{default}, Set.finite_singleton _, fun i h ↦ h ▸ V, fun i ↦ ?_, by simpa⟩
    rintro rfl
    simpa

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EffectiveEpi

Goal state before:
pp: B X : TopCat
π : X ⟶ B
hπ : IsQuotientMap ⇑(ConcreteCategory.hom π)
W✝ : TopCat
e : X ⟶ W✝
h : ∀ {Z : TopCat} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W✝
hm : π ≫ g = e
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
suffices g = ofHom (hπ.liftEquiv ⟨e.hom,
      fun a b hab ↦ CategoryTheory.congr_fun (h
          (ofHom ⟨fun _ ↦ a, continuous_const⟩)
          (ofHom ⟨fun _ ↦ b, continuous_const⟩)
          (by ext; exact hab))
        a⟩) by assumption
    apply hom_ext
    rw [hom_ofHom, ← Equiv.symm_apply_eq hπ.liftEquiv]
    ext
    simp only [IsQuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]
    rfl

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

Goal state before:
pp: C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ F.map c.fst ≫ F.map f = F.map c.snd ≫ F.map f

Tactic:
rw [← F.map_comp, c.condition]

Goal state after:
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ F.map (c.snd ≫ f) = F.map c.snd ≫ F.map f
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
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
⊢ ∃ U, ∃ (_ : IsAffineOpen U) (_ : x ∈ U), ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) ((s |_ U) ⋯) = 0

Tactic:
have (j : Over i) : IsAffine ((opensDiagram D i U).obj j) := hU.preimage (D.map _)

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
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
⊢ ∃ U, ∃ (_ : IsAffineOpen U) (_ : x ∈ U), ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) ((s |_ U) ⋯) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: 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
⊢ ∃ T,
    comap Polynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound

Tactic:
by
  choose f hf₁ hf₂ hf₃ using fun C : BasicConstructibleSetData R[X] ↦ statement (R₀ := ℤ) ⟨C.g⟩ C.f
  refine ⟨S.biUnion f, ?_, ?_⟩
  · simp only [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.image_iUnion,
      Finset.set_biUnion_biUnion, hf₁]
  · simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
    intro x y hy hx
    have H : degBound ⟨y.g⟩ ≤ S.degBound :=
      Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
    refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
    gcongr
    · simpa [Submodule.one_eq_span]
    · refine Submodule.span_le.mpr ?_
      simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]
    · delta powBound
      by_cases h : S.degBound = 0
      · have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]
      gcongr
      rwa [Nat.one_le_iff_ne_zero]

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

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ degBound k₀ (fun t ↦ Nat.casesOn t k D) (n + 1 + 1) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
rw [degBound_succ, numBound_casesOn_succ, degBound_casesOn_succ, numBound_succ, degBound_succ,
      numBound_succ]
    ring

Goal state after:
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
⊢ ∃ i U,
    ∃ (_ : IsAffineOpen U) (_ : (c.π.app i) x ∈ U),
      ∃ t, (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) t = (s |_ c.π.app i ⁻¹ᵁ U) ⋯

Tactic:
have (j : Over i) : IsAffine ((opensDiagram D i U).obj j) := hU.preimage (D.map _)

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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this✝ : CompactSpace ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
⊢ ∃ i U,
    ∃ (_ : IsAffineOpen U) (_ : (c.π.app i) x ∈ U),
      ∃ t, (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) t = (s |_ c.π.app i ⁻¹ᵁ U) ⋯
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ (C • W).IsElliptic

Tactic:
isElliptic_iff,

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ IsUnit (C • W).Δ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case u
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑{ u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.u = ↑{ u := 1, r := 0, s := 0, t := 0 }.u

Tactic:
simp only [map_one, Units.val_one, map_zero]

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

Goal state before:
pp: case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.r = { u := 1, r := 0, s := 0, t := 0 }.r

Tactic:
simp only [map_one, Units.val_one, map_zero]

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

Goal state before:
pp: case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.s = { u := 1, r := 0, s := 0, t := 0 }.s

Tactic:
simp only [map_one, Units.val_one, map_zero]

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

Goal state before:
pp: case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.t = { u := 1, r := 0, s := 0, t := 0 }.t

Tactic:
simp only [map_one, Units.val_one, map_zero]

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)
i : ι
⊢ smithCoeffs b (span {f}) ⋯ i • b' i =
    f * (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) ((selfBasis b (span {f}) hI) ((Equiv.refl ι) i))

Tactic:
mul_comm,

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)
i : ι
⊢ smithCoeffs b (span {f}) ⋯ i • b' i =
    (LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)) ((selfBasis b (span {f}) hI) ((Equiv.refl ι) i)) * f
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
j : ↥c.pt → ↥c.pt → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjx x y)) (U x))) (t x) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjy x y)) (U y))) (t y) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ U x).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ U (σi x)).carrier
S : Finset I := Finset.image i σ ∪ Finset.image₂ j σ σ
hiS : ∀ {x : ↥c.pt}, x ∈ σ → i x ∈ S
hjS : ∀ {x y : ↥c.pt}, x ∈ σ → y ∈ σ → j x y ∈ S
k : I
fk : {X : I} → X ∈ S → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ S) (mY : Y ∈ S) {f : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈
        Finset.image₂ (fun x y ↦ ⟨j ↑x ↑y, ⟨i ↑x, ⟨⋯, ⟨⋯, fjx ↑x ↑y⟩⟩⟩⟩) σ.attach σ.attach ∪
          Finset.image₂ (fun x y ↦ ⟨j ↑x ↑y, ⟨i ↑y, ⟨⋯, ⟨⋯, fjy ↑x ↑y⟩⟩⟩⟩) σ.attach σ.attach →
      fk mX ≫ f = fk mY
hk₁ : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), fk ⋯ ≫ fjx x y = fk ⋯
hk₂ : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), fk ⋯ ≫ fjy x y = fk ⋯
k' : I
fk'k : k' ⟶ k
hk' : D.map fk'k ⁻¹ᵁ ⨆ x, ⨆ (hx : x ∈ σ), D.map (fk ⋯) ⁻¹ᵁ U x = ⊤
x : ↥(D.obj k')
x✝ : x ∈ ⊤
⊢ ∃ ix, ∃ (h : ix ∈ σ), (D.map (fk'k ≫ fk ⋯)) x ∈ U ix

Tactic:
by
        simpa using hk'.ge (Set.mem_univ x)

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ span
      {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))),
        (mk W') (Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)))} =
    span {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))), (mk W') (C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y)}

Tactic:
← span_pair_add_left_mul _ _ <| mk W' <| C <| C <| W'.a₁ + ℓ,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ span
      {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))),
        (mk W') (Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃))) +
          (mk W') (C (X - C (W'.addX x₁ x₂ ℓ))) * (mk W') (C (C (W'.a₁ + ℓ)))} =
    span {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))), (mk W') (C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y)}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
⊢ span
      {(mk W) (C (X - C x)) * (mk W) (C (X - C x)), (mk W) (C (X - C x)) * (mk W) (Y - C (C y)),
        (mk W) (Y - C (C (W.negY x y))) * (mk W) (C (X - C x)),
        (mk W) (Y - C (C (W.negY x y))) * (mk W) (Y - C (C y))} =
    XIdeal W x

Tactic:
mul_comm,

Goal state after:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
⊢ span
      {(mk W) (C (X - C x)) * (mk W) (C (X - C x)), (mk W) (C (X - C x)) * (mk W) (Y - C (C y)),
        (mk W) (C (X - C x)) * (mk W) (Y - C (C (W.negY x y))),
        (mk W) (Y - C (C y)) * (mk W) (Y - C (C (W.negY x y)))} =
    XIdeal W x
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hC
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
x : R
⊢ ((g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))).comp MvPolynomial.C)
      x =
    ((↑f).comp MvPolynomial.C) x

Tactic:
simp [g]

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

Goal state before:
pp: case hX
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
x : Fin n
m✝ : Fin m →₀ ℕ
⊢ MvPolynomial.coeff m✝
      ((g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
        (MvPolynomial.X x)) =
    MvPolynomial.coeff m✝ (↑f (MvPolynomial.X x))

Tactic:
simp [g]

Goal state after: