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

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ IsDominant (Over.Hom.left (equalizer.ι f' g'))

Tactic:
apply +allowSynthFailures IsDominant.of_comp (equalizer.lift ι' ?_).left

Goal state after:
W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := ⋯
Y' : Over Z := ⋯
U' : Over Z := ⋯
f' : X' ⟶ Y' := ⋯
g' : X' ⟶ Y' := ⋯
ι' : U' ⟶ X' := ⋯
this : IsSeparated Y'.hom
⊢ IsDominant (Over.Hom.left (equalizer.lift ι' ?m.149) ≫ Over.Hom.left (equalizer.ι f' g'))

W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ ι' ≫ f' = ι' ≫ g'
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: case mpr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ (∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) → IsClosedImmersion f

Tactic:
rintro ⟨I, e, rfl⟩

Goal state after:
case mpr
X : Scheme
R : CommRingCat
I : Ideal ↑R
e : X ≅ Spec (CommRingCat.of (↑R ⧸ I))
⊢ IsClosedImmersion (e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
⊢ (Scheme.Hom.ker f).support = ⊤

Tactic:
← SetLike.coe_injective.eq_iff,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
⊢ ↑(Scheme.Hom.ker f).support = ↑⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mp
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
⊢ Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree →
    ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I

Tactic:
intro e i hi
    replace e := congr(($e).coeff i)
    simpa only [Algebra.coe_lmul_eq_mul, coeff_map, coeff_X_pow, hi.ne, ↓reduceIte,
      ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using e

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := ⋯
suitableN : R → Set ℕ := ⋯
minN : R → ℕ := ⋯
s : ↥S
⊢ (suitableN ↑s).Nonempty

Tactic:
let f : ℕ →o Ideal (Away (M := R) s) :=
      ⟨fun n ↦ Ideal.map (floc s) (I n), fun _ _ h ↦ Ideal.map_mono (I.monotone h)⟩

Goal state after:
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
s : ↥S
f : ℕ →o Ideal (Localization.Away ↑s) := { toFun := fun n ↦ Ideal.map (floc ↑s) (I n), monotone' := ⋯ }
⊢ (suitableN ↑s).Nonempty
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsLocallyNoetherian X

Tactic:
refine ⟨fun U => ?_⟩

Goal state after:
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
⊢ IsNoetherianRing ↑Γ(X, ↑U)
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Arrow.mk (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p) ≅
    Arrow.mk (map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))

Tactic:
by
  refine Arrow.isoMk' _ _
    (pullbackSymmetry _ _ ≪≫ ?_ ≪≫ pullbackSpecIso R p.asIdeal.ResidueField S) ?_ ?_
  · refine pullback.congrHom
      (Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField (.of R) p).symm rfl ≪≫ ?_
    refine asIso <| pullback.map _ _ _ _ (Spec.map <| (Scheme.Spec.residueFieldIso (.of R) _).inv)
      (𝟙 _) (𝟙 _) (by simp) (by simp)
  · exact Scheme.Spec.mapIso (Scheme.Spec.residueFieldIso (.of R) _).symm.op
  · cat_disch

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ (Scheme.Hom.ker f).support = ⊤

Tactic:
← SetLike.coe_injective.eq_iff,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ ↑(Scheme.Hom.ker f).support = ↑⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝³ : Subsingleton ↥X
inst✝² : IsReduced X
inst✝¹ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
inst✝ :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    Subsingleton ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
inst :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
have inst (i) := JacobsonSpace.of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝⁴ : Subsingleton ↥X
inst✝³ : IsReduced X
inst✝² : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
inst✝¹ :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    Subsingleton ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
inst✝ :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    IsReduced ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
inst : ∀ (i : Y.affineCover.I₀), JacobsonSpace ↥(Y.affineCover.X i)
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)
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 (⇑((∐ fun i ↦ 𝒰.X i).isoSpec.inv ≫ p) ⁻¹' ⇑f ⁻¹' s)

Tactic:
exact hs.preimage (_ ≫ p).continuous

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

Goal state before:
pp: case refine_2
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
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
h_eq :
  Polynomial.degree ∘ Polynomial.map (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff})) ∘ e.val =
    Polynomial.degree ∘ e.val
⊢ False

Tactic:
replace h_eq := congr_fun h_eq i

Goal state after:
case refine_2
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
i : Fin n
hi : e.val i ≠ 0
i_min : ∀ (j : Fin n), e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree
h_eq :
  (Polynomial.degree ∘ Polynomial.map (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff})) ∘ e.val) i =
    (Polynomial.degree ∘ e.val) i
⊢ False
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
x : X
⊢ (x ∈ Function.support fun z ↦ D₁ z ⊔ D₂ z) → x ∈ U

Tactic:
contrapose

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
x : X
⊢ x ∉ U → x ∉ Function.support fun z ↦ D₁ z ⊔ D₂ z
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
x : X
⊢ (x ∈ Function.support fun z ↦ D₁ z ⊓ D₂ z) → x ∈ U

Tactic:
contrapose

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
x : X
⊢ x ∉ U → x ∉ Function.support fun z ↦ D₁ z ⊓ D₂ z
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
U V : Set X
hV : V ⊆ U
a✝ : X
⊢ (restrict 0 hV) a✝ = 0 a✝

Tactic:
rw [restrict_apply]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
U V : Set X
hV : V ⊆ U
a✝ : X
⊢ (if a✝ ∈ V then 0 a✝ else 0) = 0 a✝
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
a✝ : X
⊢ (a✝ ∈ Function.support fun x ↦ restrict (single x (F x)) ⋯) → a✝ ∈ ↑h.toFinset

Tactic:
contrapose

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support.Finite
a✝ : X
⊢ a✝ ∉ ↑h.toFinset → a✝ ∉ Function.support fun x ↦ restrict (single x (F x)) ⋯
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
f : locallyFinsuppWithin U Y
p : X
hp : p ∈ U
⊢ Disjoint (𝓝[f.support] p) cofinite

Tactic:
rw [disjoint_cofinite_right]
  obtain ⟨t, h₁t, h₂t⟩ := f.supportLocallyFiniteWithinDomain p hp
  refine ⟨t ∩ f.support, ?_, h₂t⟩
  rw [mem_nhdsWithin_iff_exists_mem_nhds_inter]
  grind

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint ↑(X.presheaf.stalk x))) ≫ Scheme.stalkClosedPointTo φ =
    S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x

Tactic:
· apply Spec.map_injective
    rw [← cancel_mono (S.fromSpecStalk _)]
    simpa only [Spec.map_comp, Category.assoc, Scheme.SpecMap_stalkMap_fromSpecStalk,
      Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc,
      Scheme.SpecMap_stalkSpecializes_fromSpecStalk]

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

Goal state before:
pp: X Y : Scheme
f : X.PartialMap Y
⊢ f.toRationalMap.representative.equiv f

Tactic:
← PartialMap.toRationalMap_eq_iff,

Goal state after:
X Y : Scheme
f : X.PartialMap Y
⊢ f.toRationalMap.representative.toRationalMap = f.toRationalMap
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (g x).equiv (g y)

Tactic:
← PartialMap.toRationalMap_eq_iff,

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X ⤏ Y
x y : f.openCoverDomain.I₀
g : f.openCoverDomain.I₀ → X.PartialMap Y := fun x ↦ Exists.choose ⋯
hg₁ : ∀ (x : f.openCoverDomain.I₀), (g x).toRationalMap = f
hg₂ : ∀ (x : f.openCoverDomain.I₀), (g x).domain = ↑x
⊢ (g x).toRationalMap = (g y).toRationalMap
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
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
g : Y.PartialMap Z
⊢ (f.restrict U hU hU').comp g = (f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U) ⋯ ⋯

Tactic:
by
  ext
  · simp [ι_image_homOfLE_eq_ι_image_inf]
  · simp [morphismRestrict_comp, isoImage_ι_inv_morphismRestrict_homOfLE_assoc, isoOfEq_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

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

Tactic:
obtain ⟨b, rfl⟩ := Spec.map_surjective b

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
inst✝⁶ : IsCofiltered I
i j : I
R : CommRingCat
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝² : ∀ (i : I), CompactSpace ↥((D ⋙ Scheme.Spec).obj i)
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
inst✝ : IsAffine c.pt
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : S ⟶ Opposite.unop (D.obj i)
ha : t.app i = Spec.map a ≫ Spec.map φ
b : S ⟶ Opposite.unop (D.obj j)
hb : t.app j = Spec.map b ≫ Spec.map φ
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
⊢ ∃ k hik hjk, (D ⋙ Scheme.Spec).map hik ≫ Spec.map a = (D ⋙ Scheme.Spec).map hjk ≫ Spec.map b
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
inst✝⁶ : IsCofiltered I
i j : I
R : CommRingCat
inst✝⁵ : IsAffine (Spec R)
S : CommRingCat
inst✝⁴ : IsAffine (Spec S)
φ : R ⟶ S
inst✝³ : LocallyOfFiniteType (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝² : ∀ (i : I), CompactSpace ↥((D ⋙ Scheme.Spec).obj i)
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
inst✝ : IsAffine c.pt
a : S ⟶ Opposite.unop (D.obj i)
b : S ⟶ Opposite.unop (D.obj j)
hab : c.π.app i ≫ Spec.map a = c.π.app j ≫ Spec.map b
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
t : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp
ha : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i = Spec.map a ≫ Spec.map φ
hb : (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app j = Spec.map b ≫ Spec.map φ
this : CreatesLimitsOfSize.{u, u, u, u, u + 1, u + 1} Scheme.Spec
⊢ Spec.map (a ≫ (coconeLeftOpOfCone (liftLimit hc)).ι.app (Opposite.op i)) =
    Spec.map (b ≫ (coconeLeftOpOfCone (liftLimit hc)).ι.app (Opposite.op j))

Tactic:
by
      simp only [coconeLeftOpOfCone_pt, Functor.const_obj_obj,
        Functor.leftOp_obj, coconeLeftOpOfCone_ι_app, Spec.map_comp]
      simp only [← Scheme.Spec_map, ← liftedLimitMapsToOriginal_hom_π, Category.assoc, hab]

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

Goal state before:
pp: case refine_2.refine_2
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
⊢ (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
              (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left)) (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right))
              ⋯ ⋯).hom).obj
      (F.mapCone c) ≅
    PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯

Tactic:
exact Cone.ext (Iso.refl _) <| by rintro (_ | _ | _) <;> cat_disch

Goal state after:
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
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g }.degBound ≤ S.degBound
⊢ x.n ≤ S.degBound ∧ ∀ (i : Fin x.n), x.g i ∈ M ^ S.degBound ^ S.degBound

Tactic:
refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩

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
H : { val := y.g }.degBound ≤ S.degBound
i : Fin x.n
⊢ coeffSubmodule ℤ { val := y.g } ^ { val := y.g }.powBound ≤ M ^ S.degBound ^ S.degBound
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 2
⊢ W.j = 0 ↔ W.a₁ ^ 12 = 0

Tactic:
j_of_char_two,

Goal state after:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 2
⊢ ↑W.Δ'⁻¹ * W.a₁ ^ 12 = 0 ↔ W.a₁ ^ 12 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W.polynomial
⊢ False

Tactic:
rcases (monic_polynomial.not_irreducible_iff_exists_add_mul_eq_coeff natDegree_polynomial).mp h
    with ⟨f, g, h0, h1⟩

Goal state after:
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h : ¬Irreducible W.polynomial
f g : R[X]
h0 : W.polynomial.coeff 0 = f * g
h1 : W.polynomial.coeff 1 = f + g
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
h : (Units.map ↑φ) x✝¹.u = (Units.map ↑φ) x✝.u
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
⊢ x✝¹ = x✝

Tactic:
replace h := (Units.mk.inj h).left

Goal state after:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹ = x✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ C.map φ • W.map φ = (C • W).map φ

Tactic:
simp only [map, variableChange_def, VariableChange.map]
  ext <;> map_simp <;> simp only [Units.coe_map_inv, MonoidHom.coe_coe]

Goal state after: