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

Goal state before:
pp: case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap (algebraMap R A)
      (comap (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) { asIdeal := q, isPrime := hq }) =
    x

Tactic:
← comap_comp_apply,

Goal state after:
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)).comp (algebraMap R A))
      { asIdeal := q, isPrime := hq } =
    x
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ ∃ a, comap C a = x

Tactic:
refine ⟨comap (evalRingHom 0) x, ?_⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ comap C (comap (evalRingHom 0) x) = x
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ comap C (comap (evalRingHom 0) x) = x

Tactic:
← comap_comp_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ comap ((evalRingHom 0).comp C) x = x
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
⊢ IsArtinianRing ↑Γ(X, ↑U)

Tactic:
have _ : IsNoetherianRing Γ(X, U) := IsLocallyNoetherian.component_noetherian U
    rw [isArtinianRing_iff_krullDimLE_zero, Ring.KrullDimLE, Order.krullDimLE_iff, ← ringKrullDim,
      Nat.cast_zero, ← PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim Γ(X, U)]
    change topologicalKrullDim (Spec Γ(X, U)) ≤ 0
    rw [← IsHomeomorph.topologicalKrullDim_eq _ U.2.isoSpec.hom.homeomorph.isHomeomorph]
    exact (topologicalKrullDim_subspace_le X U).trans h

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right✝ : W.carrier ⊆ ↑⊤
this✝ : IsArtinianRing ↑Γ(X, W)
this : DiscreteTopology ↥(Spec Γ(X, W))
⊢ IsOpen {x}

Tactic:
have : DiscreteTopology W := hW1.isoSpec.hom.homeomorph.symm.discreteTopology

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right✝ : W.carrier ⊆ ↑⊤
this✝¹ : IsArtinianRing ↑Γ(X, W)
this✝ : DiscreteTopology ↥(Spec Γ(X, W))
this : DiscreteTopology ↥↑W
⊢ IsOpen {x}
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ comap C (comap (eval₂Hom (RingHom.id R) 0) x) = x

Tactic:
← comap_comp_apply,

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ comap ((eval₂Hom (RingHom.id R) 0).comp C) x = x
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Set.range ⇑(asFiberHom f x) = {asFiber f x}

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
⊢ DenseRange ⇑g

Tactic:
denseRange_iff_closure_range,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
⊢ closure (Set.range ⇑g) = Set.univ
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X S : Scheme
f : X ⟶ S
⊢ GeometricallyIrreducible f ↔ ∀ (s : ↥S), GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField f s)

Tactic:
simp only [GeometricallyIrreducible.eq_geometrically,
    ← geometrically_iff_forall_fiberToSpecResidueField]

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

Goal state before:
pp: case inr
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec R), (∃ S, X = Spec S) → IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ S, X = Spec S
H : IsIntegralHom f
inst : IsAffine X
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)

Tactic:
← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv

Goal state after:
case inr
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec R), (∃ S, X = Spec S) → IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ S, X = Spec S
inst : IsAffine X
H : IsIntegralHom (X.isoSpec.inv ≫ f)
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R},
    UniversallyClosed f → IsAffineHom f → (∃ S, X = Spec S) → IsIntegralHom f
hX : ¬∃ S, X = Spec S
inst : IsAffine X
⊢ IsIntegralHom f

Tactic:
← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R},
    UniversallyClosed f → IsAffineHom f → (∃ S, X = Spec S) → IsIntegralHom f
hX : ¬∃ S, X = Spec S
inst : IsAffine X
⊢ IsIntegralHom (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : ↑Γ(X, ⊤)
hxr :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) x ∈
    ↑(PrimeSpectrum.basicOpen r)
hrU :
  ↑(PrimeSpectrum.basicOpen r) ⊆
    ⇑(ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) '' ↑U
⊢ ∃ U' ∈ {x | ∃ r, ∃ (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}, x ∈ U' ∧ U' ≤ U

Tactic:
simp_rw [← toSpecΓ_preimage_basicOpen]

Goal state after:
X : Scheme
inst✝ : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : ↑Γ(X, ⊤)
hxr :
  (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) x ∈
    ↑(PrimeSpectrum.basicOpen r)
hrU :
  ↑(PrimeSpectrum.basicOpen r) ⊆
    ⇑(ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) '' ↑U
⊢ ∃
    U' ∈
      {x |
        ∃ r,
          ∃ (_ : IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)), X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = x},
    x ∈ U' ∧ U' ≤ U
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_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
i : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
aesop

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_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
i : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
aesop

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_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
i : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
aesop

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_1
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV✝ : ∀ (i : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
this✝ : ∀ (i : ι), VX i ≤ iX ⁻¹ᵁ US
algInst✝¹ : Algebra ↑Γ(S, US) ↑Γ(X, UX) := (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).toAlgebra
algInst✝ : Algebra ↑Γ(S, US) ↑Γ(T, UT) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).toAlgebra
algebraizeInst✝ : Module.Flat ↑Γ(S, US) ↑Γ(T, UT)
this : (i : ι) → Algebra ↑Γ(S, US) ↑Γ(X, VX i) :=
  fun i ↦ (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US (VX i) ⋯)).toAlgebra
ψY : ↑Γ(Y, UY) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  RingHom.pi fun i ↦ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)
ψ : ↑Γ(X, UX) →ₐ[↑Γ(S, US)] (i : ι) → ↑Γ(X, VX i) :=
  AlgHom.pi fun i ↦ { toRingHom := CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op), commutes' := ⋯ }
hψ : Function.Injective ⇑ψ
hψ' : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ)
hV : ∀ (i : ι), Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST ⋯ ⋯))
val✝ : Fintype ι
i : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
aesop

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
z : X
t : Set X
ht : t ∈ 𝓝 z
⊢ t ∩ support f = Subtype.val '' {i | ↑i ∈ t}

Tactic:
aesop

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
z : X
t : Set X
ht : t ∈ 𝓝 z
aux1 : t ∩ support f = Subtype.val '' {i | ↑i ∈ t}
⊢ InjOn Subtype.val {i | ↑i ∈ t}

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
W : Set X
inst✝ : Zero Y
f : X → Y
h : LocallyFiniteSupport f
hW : IsCompact W
this : {i | ({↑i} ∩ W).Nonempty}.Finite
α : Type u_1
s t : Set α
⊢ Subtype.val '' {i | ({↑i} ∩ t).Nonempty} = t ∩ s

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x : X
⊢ single x 0 = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite

Tactic:
obtain ⟨t₂, ht₂⟩ := hg.2 z hz

Goal state after:
case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
z : X
hz : z ∈ U
t₁ : Set X
ht₁ : t₁ ∈ 𝓝 z ∧ (t₁ ∩ Function.support f).Finite
t₂ : Set X
ht₂ : t₂ ∈ 𝓝 z ∧ (t₂ ∩ Function.support g).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).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
i : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
aesop

Goal state after:
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
i j : ι
⊢ VX i ≤ iX ⁻¹ᵁ US

Tactic:
aesop

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
U V : Set X
hV : V ⊆ U
a✝ : X
⊢ (if a✝ ∈ V then 0 a✝ else 0) = 0 a✝

Tactic:
aesop

Goal state after:
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✝ ∉ ↑h.toFinset → a✝ ∉ Function.support fun x ↦ restrict (single x (F x)) ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case pos
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
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz : z ∉ U
⊢ (∑ i ∈ h.toFinset, restrict (single i (F i)) ⋯) z = F z

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case pos
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
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz✝ : ¬z ∉ U
hz : z ∈ F.support
⊢ (if z ∈ U then if z ∈ h.toFinset then F z else 0 else 0) = F z

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case neg
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
this : (Function.support fun x ↦ restrict (single x (F x)) ⋯) ⊆ ↑h.toFinset
z : X
hz✝ : ¬z ∉ U
hz : z ∉ F.support
⊢ (if z ∈ U then if z ∈ h.toFinset then F z else 0 else 0) = F z

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ (if x ∈ V then (D x)⁺ else 0) = (if x ∈ V then D x else 0)⁺

Tactic:
aesop

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ (if x ∈ V then (D x)⁻ else 0) = (if x ∈ V then D x else 0)⁻

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝¹ : IrreducibleSpace ↥X
U : X.Opens
inst✝ : Nonempty ↥↑U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
⊢ (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f) =
    (ConcreteCategory.hom (X.germToFunctionField U)) f

Tactic:
by
  simp [RingHom.algebraMap_toAlgebra, ← ConcreteCategory.comp_apply]

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
⊢ f.equiv g

Tactic:
have hdense : Dense ((f.domain ⊓ g.domain) : Set X) :=
    f.dense_domain.inter_of_isOpen_left g.dense_domain f.domain.2
  have := (isGermInjectiveAt_iff_of_isOpenImmersion (f := (f.domain ⊓ g.domain).ι)
    (x := ⟨x, hxf, hxg⟩)).mp ‹_›
  have := spread_out_unique_of_isGermInjective' (X := (f.domain ⊓ g.domain).toScheme)
    (X.homOfLE inf_le_left ≫ f.hom) (X.homOfLE inf_le_right ≫ g.hom) (x := ⟨x, hxf, hxg⟩) ?_
  · obtain ⟨U, hxU, e⟩ := this
    refine ⟨(f.domain ⊓ g.domain).ι ''ᵁ U, ((f.domain ⊓ g.domain).ι ''ᵁ U).2.dense
      ⟨_, ⟨_, hxU, rfl⟩⟩,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
      ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩
    rw [← cancel_epi (Scheme.Hom.isoImage _ _).hom]
    simp only [restrict_hom, ← Category.assoc] at e ⊢
    convert! e using 2 <;> rw [← cancel_mono (Scheme.Opens.ι _)] <;> simp
  · rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,
      ← g.fromSpecStalkOfMem_restrict hdense inf_le_right ⟨hxf, hxg⟩] at H
    simpa only [fromSpecStalkOfMem, restrict_domain, Opens.fromSpecStalkOfMem, Spec.map_inv,
      restrict_hom, Category.assoc, IsIso.eq_inv_comp, IsIso.hom_inv_id_assoc] using H

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
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
I : Set ↑X.affineOpens
hI : I.Finite
e : UX = ⨆ i ∈ I, ↑i
i✝ : ↑I
i : ↥X
⊢ i ∈ ↑↑i✝ → i ∈ ⨆ i ∈ I, ↑i

Tactic:
aesop

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
inst✝ : Flat f
hUS : IsAffineOpen US
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
hUX : IsCompact ↑UX
hUX' : IsQuasiSeparated ↑UX
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set ↑T.affineOpens
hI : I.Finite
e : UT = ⨆ i ∈ I, ↑i
i✝ : ↑I
i : ↥T
⊢ i ∈ ↑↑i✝ → i ∈ ⨆ i ∈ I, ↑i

Tactic:
aesop

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)
⊢ TopologicalSpace.Opens.IsBasis {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}

Tactic:
refine TopologicalSpace.Opens.isBasis_iff_nbhd.mpr fun {U x} hxU ↦ ?_

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)
U : TopologicalSpace.Opens ↥c.pt
x : ↥c.pt
hxU : x ∈ U
⊢ ∃ U' ∈ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}, x ∈ U' ∧ U' ≤ U
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1.inl
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 ι
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hcov : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
h✝ : s = ∅
⊢ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U

Tactic:
aesop

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

Goal state before:
pp: case refine_1.inr
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 ι
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hcov : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
h✝ : s = {default}
⊢ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U

Tactic:
aesop

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

Goal state before:
pp: case refine_1.refine_3
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ (fun p ↦ f p.fst p.snd) '' { carrier := s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅, is_open' := ⋯ }.carrier = U

Tactic:
aesop

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

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : TopologicalSpace S
U : Set S
hU : IsCompact U
s : Set (Opens S)
hs : ⋃ t ∈ s, ↑t = U
H : ∀ t ∈ s, IsCompactOpenCovered f ↑t
t : Finset ↑s
ht : U ⊆ ⋃ i ∈ t, ↑↑i
x : S
h : x ∈ ⋃ t_1 ∈ SetLike.coe '' ↑(Finset.image Subtype.val t), t_1
⊢ x ∈ U

Tactic:
aesop

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

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
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)
x : S
x✝ : ∃ i, x ∈ (fun a ↦ f (↑i.fst) a) '' ↑↑i.snd
i : σ
hi : X ↑i.fst
o : hi ∈ ↑↑i.snd
ho : (fun a ↦ f (↑i.fst) a) hi = x
⊢ ∃ i, ∃ (i_1 : i ∈ s), x ∈ f i '' ↑(V i i_1)

Tactic:
aesop

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

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : Finite ι
inst✝ : TopologicalSpace S
hf : ∀ (i : ι), IsSpectralMap (f i)
U : Set S
hs : ∀ x ∈ U, ∃ i, x ∈ Set.range (f i)
hU : IsOpen U
hc : IsCompact U
⊢ IsCompactOpenCovered f U

Tactic:
by
  refine ⟨.univ, Set.finite_univ, fun i _ ↦ ⟨f i ⁻¹' U, hU.preimage (hf i).1⟩,
    fun i _ ↦ hc.preimage_of_isOpen (hf i) hU, subset_antisymm (by simp) fun x hx ↦ ?_⟩
  obtain ⟨i, y, rfl⟩ := hs x hx
  simpa using ⟨i, y, hx, rfl⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
⊢ ((g a ≫ i a) ≫ g a) ≫ f a = g a ≫ f a

Tactic:
aesop

Goal state after: