mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
⊢ f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support f).Finite

Tactic:
by
  have : f.support = (U \ {x | f x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_sdiff, mem_ofPred_eq, iff_and_self]
    exact (h ·)
  rw [EventuallyEq, Filter.Eventually, codiscreteWithin_iff_locallyFiniteComplementWithin, this]

Goal state after:
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
⊢ (∀ (x : X), ∃ t ∈ 𝓝 x, {i | ({↑i} ∩ t).Nonempty}.Finite) ↔ LocallyFiniteSupport f

Tactic:
peel with z t ht

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
⊢ {i | ({↑i} ∩ t).Nonempty}.Finite ↔ (t ∩ support f).Finite
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
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 ⋯ ⋯)
i j : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
by clear hV; aesop

Goal state after:
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
x : X
hx : x ∈ V ∧ ¬D x = 0
⊢ x ∈ V

Tactic:
exact hx.1

Goal state after:
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))
⊢ ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0

Tactic:
have hJ (x) : x ∈ J ↔ ∃ y : I.primeCompl, y * x = 0 :=
    IsLocalization.map_eq_zero_iff I.primeCompl _ x

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 ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
φ' : ↑A →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : ↑Γ(X, s.inf W ⊓ U) →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
⊢ ⇑φ' '' ↑s ⊆ ↑ψ.range

Tactic:
rintro _ ⟨i, hi, rfl : φ i = _⟩

Goal state after:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝² : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this✝¹ : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
this✝ : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
this : Algebra ↑R ↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) :=
  (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (homOfLE ⋯).op)).toAlgebra
φ' : ↑A →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : ↑Γ(X, s.inf W ⊓ U) →ₐ[↑R] ↑(X.presheaf.stalk x) :=
  let __src := CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
i : ↑A
hi : i ∈ ↑s
⊢ (ConcreteCategory.hom φ) i ∈ ↑ψ.range
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ closure (⇑f '' Set.univ) = Set.univ

Tactic:
← Set.univ_subset_iff

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ Set.univ ⊆ closure (⇑f '' Set.univ)
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense ↑W₁
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : (f.restrict W₁ hW₁ hW₁l).hom = (g.restrict W₁ hW₁ hW₁r).hom
W₂ : X.Opens
hW₂ : Dense ↑W₂
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : (g.restrict W₂ hW₂ hW₂l).hom = (h.restrict W₂ hW₂ hW₂r).hom
⊢ (f.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom = (h.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom

Tactic:
dsimp at e₁ e₂

Goal state after:
X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense ↑W₁
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : X.homOfLE hW₁l ≫ f.hom = X.homOfLE hW₁r ≫ g.hom
W₂ : X.Opens
hW₂ : Dense ↑W₂
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : X.homOfLE hW₂l ≫ g.hom = X.homOfLE hW₂r ≫ h.hom
⊢ (f.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom = (h.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom
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)
this : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰).X j)
⊢ False

Tactic:
obtain ⟨x, -⟩ :=
        Cover.covers (𝒰.pullback₁ (D.map (g i (by simp)))) (Nonempty.some inferInstance)

Goal state after:
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)
this : ∀ (j : 𝒰.I₀), IsEmpty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰).X j)
x :
  ↥((Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰).X
      (Cover.idx (Precoverage.ZeroHypercover.pullback₁ (D.map (g i ⋯)) 𝒰) ⋯.some))
⊢ False
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.PartialMap Z
inst✝ : IsDominant g.hom
⊢ IsDominant ((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ≫ f.hom ∣_ g.domain ≫ g.hom)

Tactic:
have := IsZariskiLocalAtTarget.restrict ‹IsDominant f.hom› g.domain

Goal state after:
X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f : X.PartialMap Y
inst✝¹ : IsDominant f.hom
g : Y.PartialMap Z
inst✝ : IsDominant g.hom
this : IsDominant (f.hom ∣_ g.domain)
⊢ IsDominant ((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ≫ f.hom ∣_ g.domain ≫ g.hom)
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.34} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.34} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
⊢ ∃ k hki hkj y, (pullback.lift (d.functor.map hki) (d.functor.map hkj) ⋯) y = x

Tactic:
let xi := pullback.fst (d.cover.f i) _ x
    let xj := pullback.snd (d.cover.f i) _ x
    obtain ⟨k, fi, fj, uk, h1, h2⟩ :=
        𝒰.exists_of_f_eq_f (d.natTrans.app i xi) (d.natTrans.app j xj) <| by
      dsimp [functorOfLocallyDirected_obj, xi, xj]
      rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, ← ι_toBase, pullback.condition_assoc]
      simp
    use k, fi, fj
    obtain ⟨xk, h1, h2⟩ := exists_preimage_of_isPullback (d.equifibered fj) xj uk <| by
      apply (𝒰.f j).injective
      dsimp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
      rw [← Scheme.Hom.comp_apply]
      simp [xj, h2]
    use xk
    apply (pullback.snd (d.cover.f i) _).injective
    rw [← Scheme.Hom.comp_apply]
    simp [h1, xj]

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

Goal state before:
pp: case e'_2.e_a
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ zeroLocus (Set.range 0) = Set.univ

Tactic:
← Set.univ_subset_iff

Goal state after:
case e'_2.e_a
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
⊢ Set.univ ⊆ zeroLocus (Set.range 0)
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
hU : IsCompactOpenCovered f U
⊢ ∃ κ,
    ∃ (_ : Finite κ),
      ∃ a V, (∀ (i : κ), V i ∈ B (a i)) ∧ (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ i, f (a i) '' ↑(V i) = U

Tactic:
obtain ⟨s, hs, V, hc, hunion⟩ := hU

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
⊢ ∃ κ,
    ∃ (_ : Finite κ),
      ∃ a V, (∀ (i : κ), V i ∈ B (a i)) ∧ (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ i, f (a i) '' ↑(V i) = U
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
this : f x ∈ ↑U
⊢ x ∈
    ⋃ i,
      ⋃ (h : i ∈ s),
        (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) i ''
          ↑((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i h)

Tactic:
simp_rw [← heq, Set.mem_iUnion] at this

Goal state after:
case refine_2
S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : QuasiCompactCover 𝒰
T : Scheme
f : T ⟶ S
U' : T.Opens
hU' : IsAffineOpen U'
U : S.Opens
hU : IsAffineOpen U
hsub : ⇑f '' ↑U' ⊆ ↑U
s : Set 𝒰.I₀
hf : s.Finite
V : (i : 𝒰.I₀) → i ∈ s → TopologicalSpace.Opens ((fun x ↦ ↥(𝒰.X x)) i)
hc : ∀ (i : 𝒰.I₀) (h : i ∈ s), IsCompact (V i h).carrier
heq : ⋃ i, ⋃ (h : i ∈ s), (fun x ↦ ⇑(𝒰.f x)) i '' ↑(V i h) = ↑U
x : ↥T
hx : x ∈ ↑U'
this : ∃ i, ∃ (i_1 : i ∈ s), f x ∈ (fun a ↦ (𝒰.f i) a) '' ↑(V i ⋯)
⊢ x ∈
    ⋃ i,
      ⋃ (h : i ∈ s),
        (fun x ↦ ⇑((PreZeroHypercover.pullback₁ f 𝒰).f x)) i ''
          ↑((fun i hi ↦ pullback.fst f (𝒰.f i) ⁻¹ᵁ U' ⊓ pullback.snd f (𝒰.f i) ⁻¹ᵁ V i hi) i h)
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case refine_1.refine_3
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
i : 𝒱.I₀
this :
  ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.snd s.pt.hom (𝒰.f i) =
    (d.cocone i).pt.hom
⊢ ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.snd s.pt.hom (𝒰.f i) ≫ 𝒰.f i =
    d.relativeGluingData.cover.f i ≫ Over.hom (MorphismProperty.Over.mk ⊤ d.relativeGluingData.toBase ⋯).toComma

Tactic:
reassoc_of% this

Goal state after:
case refine_1.refine_3
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
i : 𝒱.I₀
this :
  ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.snd s.pt.hom (𝒰.f i) =
    (d.cocone i).pt.hom
⊢ (d.cocone i).pt.hom ≫ 𝒰.f i =
    d.relativeGluingData.cover.f i ≫ Over.hom (MorphismProperty.Over.mk ⊤ d.relativeGluingData.toBase ⋯).toComma
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.c₄ = W.a₁ ^ 4

Tactic:
rw [c₄, b₂_of_char_two]
  linear_combination -12 * W.b₄ * CharP.cast_eq_zero R 2

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 : I), IsAffine (D.obj i)
i : I
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
this : ∀ (i : Iᵒᵖ), IsAffine (Opposite.unop (D.op.obj i))
j : Iᵒᵖ
f : Opposite.op i ⟶ j
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) s =
    (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) 0
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) s = 0

Tactic:
by simpa using hj

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
⊢ 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

Tactic:
← neg_eq_zero,

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.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case right.inl
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
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
hs : zeroLocus s₀ = Set.range (comap g)
hg'' : ∀ (t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))), comap g '' t = comap σ ⁻¹' t ∩ zeroLocus s₀
hS' : comap g '' S.toSet = S'.toSet
x : BasicConstructibleSetData (MvPolynomial (Fin m) R)
hx : x ∈ S
j : Fin x.n
⊢ ((MvPolynomial.map MvPolynomial.C) (x.g j)).degrees ≤ d

Tactic:
exact degrees_map_le.trans (hS _ hx j)

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
p q r s : ℤ
⊢ f (rel W p q r s) = rel (⇑f ∘ W) p q r s

Tactic:
simp_rw [rel, map_add, map_sub, map_mul, Function.comp]

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

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : ¬x₁ = x₂
⊢ ∃ x,
    (∃ a a_1 a_2, a_2 * (Y - W.negPolynomial) = x + a * C (X - C x₁) + a_1 * C (X - C x₂)) ∧
      (AdjoinRoot.mk W.polynomial) x = 1

Tactic:
replace hx := sub_ne_zero_of_ne hx

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
⊢ ∃ x,
    (∃ a a_1 a_2, a_2 * (Y - W.negPolynomial) = x + a * C (X - C x₁) + a_1 * C (X - C x₂)) ∧
      (AdjoinRoot.mk W.polynomial) x = 1
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
P : ℕ → Sort u_4
zero : P 0
one : P 1
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) → P k) → P (2 * (m + 1))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) + 1 → P k) → P (2 * (m + 1) + 1)
n : ℕ
h : (k : ℕ) → k < 2 * 0 + 1 → P k
⊢ P (2 * 0 + 1)

pp: case succ
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
P : ℕ → Sort u_4
zero : P 0
one : P 1
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) → P k) → P (2 * (m + 1))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) + 1 → P k) → P (2 * (m + 1) + 1)
n n✝ : ℕ
h : (k : ℕ) → k < 2 * (n✝ + 1) + 1 → P k
⊢ P (2 * (n✝ + 1) + 1)

Tactic:
exacts [one, odd _ h]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case intro
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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
⊢ ∃ i V, IsOpenCover V ∧ ∀ (j : J), IsAffineOpen (V j) ∧ U j = c.π.app i ⁻¹ᵁ V j

Tactic:
obtain ⟨k, fkj, e⟩ := exists_map_eq_top D c hc (⨆ (k), D.map (fi k) ⁻¹ᵁ V k) (by
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, c.w, hVU]
    exact hU)

Goal state after:
case intro
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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
⊢ ∃ i V, IsOpenCover V ∧ ∀ (j : J), IsAffineOpen (V j) ∧ U j = c.π.app i ⁻¹ᵁ V j
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ (W.preΨ (2 * m) ^ 2 * if Even (2 * m) then W.Ψ₂Sq else 1) =
    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq

Tactic:
preΨ_even,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ ((W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 *
      if Even (2 * m) then W.Ψ₂Sq else 1) =
    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq