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

Goal state before:
pp: n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
⊢ f = g

Tactic:
ext x

Goal state after:
case hC
n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : ULift.{u_1, 0} ℤ
⊢ ((CommRingCat.Hom.hom f).comp C) x = ((CommRingCat.Hom.hom g).comp C) x

case hX
n : Type u
R : CommRingCat
f g : ℤ[n] ⟶ R
h : ∀ (i : n), (ConcreteCategory.hom f) (X i) = (ConcreteCategory.hom g) (X i)
this :
  (CommRingCat.Hom.hom f).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom =
    (CommRingCat.Hom.hom g).comp (mapEquiv n ULift.ringEquiv.symm).toRingHom
x : n
⊢ (CommRingCat.Hom.hom f) (X x) = (CommRingCat.Hom.hom g) (X x)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
R S : CommRingCat
φ : R ⟶ S
⊢ ((SpecIso n S).inv ≫ map n (Spec.map φ)) ≫ 𝔸(n; Spec R) ↘ Spec R =
    (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv) ≫
      𝔸(n; Spec R) ↘ Spec R

pp: case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ)))) (coord (Spec R) i✝) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)))
      (coord (Spec R) i✝)

Tactic:
· simp only [map_over, Category.assoc, SpecIso_inv_over, SpecIso_inv_over_assoc,
      ← Spec.map_comp, ← CommRingCat.ofHom_comp]
    rw [map_comp_C, CommRingCat.ofHom_comp, CommRingCat.ofHom_hom]

Goal state after:
case h₂
n : Type u
R S : CommRingCat
φ : R ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((SpecIso n S).inv ≫ map n (Spec.map φ)))) (coord (Spec R) i✝) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop
          (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))) ≫ (SpecIso n R).inv)))
      (coord (Spec R) i✝)
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
⊢ support f = U \ {x | f x = 0 x}

Tactic:
ext x

Goal state after:
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
x : X
⊢ x ∈ support f ↔ x ∈ U \ {x | f x = 0 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
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
⊢ D.support = U \ {x | D x = 0 x}

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
⊢ x ∈ D.support ↔ x ∈ U \ {x | D x = 0 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
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
⊢ D.support = {x | D x = 0}ᶜ ∩ U

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
⊢ x ∈ D.support ↔ x ∈ {x | D x = 0}ᶜ ∩ U
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
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
⊢ D.support = U \ {x | (fun x ↦ D x = 0 x) x}

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
⊢ x ∈ D.support ↔ x ∈ U \ {x | (fun x ↦ D x = 0 x) x}
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
⊢ 0 ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}

Tactic:
simp only [support_subset_iff, ne_eq, mem_ofPred_eq, Pi.zero_apply, not_true_eq_false,
      IsEmpty.forall_iff, implies_true, support_zero, inter_empty, finite_empty, and_true,
      true_and]
    exact fun _ _ ↦ ⟨⊤, univ_mem⟩

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✝¹ : Lattice Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
h₁₂ : D₁ ≤ D₂
h₂₁ : D₂ ≤ D₁
⊢ D₁ = D₂

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Lattice Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
h₁₂ : D₁ ≤ D₂
h₂₁ : D₂ ≤ D₁
x : X
⊢ D₁ x = D₂ x
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
⊢ (n • f)⁺ = n • f⁺

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ (n • f)⁺ x = (n • 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✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
⊢ (n • f)⁻ = n • f⁻

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
n : ℕ
f : locallyFinsuppWithin U Y
x : X
⊢ (n • f)⁻ x = (n • 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✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
⊢ restrict 0 h = 0

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
x : X
⊢ (restrict 0 h) x = 0 x
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ + D₂).restrict h = D₁.restrict h + D₂.restrict h

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ ((D₁ + D₂).restrict h) x = (D₁.restrict h + D₂.restrict h) x
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : AddCommGroup Y
inst✝ : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ ⊔ D₂).restrict h = D₁.restrict h ⊔ D₂.restrict h

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : AddCommGroup Y
inst✝ : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ ((D₁ ⊔ D₂).restrict h) x = (D₁.restrict h ⊔ D₂.restrict h) x
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : AddCommGroup Y
inst✝ : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ ⊓ D₂).restrict h = D₁.restrict h ⊓ D₂.restrict h

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : AddCommGroup Y
inst✝ : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ ((D₁ ⊓ D₂).restrict h) x = (D₁.restrict h ⊓ D₂.restrict h) x
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
⊢ D⁺.restrict h = (D.restrict h)⁺

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ (D⁺.restrict h) x = (D.restrict h)⁺ x
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
⊢ D⁻.restrict h = (D.restrict h)⁻

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ (D⁻.restrict h) x = (D.restrict h)⁻ x
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case inr
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')
j : 𝒰.I₀
H : ∀ {i' : I} (f : i' ⟶ i), Nonempty ↥((Precoverage.ZeroHypercover.pullback₁ (D.map f) 𝒰).X j)
F : Over i ⥤ Scheme := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget (𝒰.X j)
this✝³ : ∀ (i' : Over i), IsAffine (F.obj i')
this✝² : ∀ (i' : Over i), Nonempty ↥(F.obj i')
e : F ⟶ (F ⋙ Γ.rightOp) ⋙ Scheme.Spec := F.whiskerLeft ΓSpec.adjunction.unit
this✝¹ : ∀ (i_1 : Over i), IsIso (e.app i_1)
this✝ : IsIso e
c' : LimitCone F :=
  { cone := (Cone.postcompose (asIso e).inv).obj (Scheme.Spec.mapCone (limit.cone (F ⋙ Γ.rightOp))),
    isLimit :=
      (IsLimit.postcomposeInvEquiv (asIso e) (Scheme.Spec.mapCone (limit.cone (F ⋙ Γ.rightOp)))).symm
        (isLimitOfPreserves Scheme.Spec (limit.isLimit (F ⋙ Γ.rightOp))) }
this : Nonempty ↥c'.cone.pt
α : F ⟶ Over.forget i ⋙ D :=
  Functor.whiskerRight ((Over.post D).whiskerLeft (Over.mapPullbackAdj (𝒰.f j)).counit) (Over.forget (D.obj i))
⊢ Nonempty ↥c.pt

Tactic:
exact this.map (((Functor.Initial.isLimitWhiskerEquiv (Over.forget i) c).symm hc).lift
        ((Cone.postcompose α).obj c'.1))

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

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f₁ f₂ : X.PartialMap Y
inst✝¹ : IsDominant f₁.hom
inst✝ : IsDominant f₂.hom
g : Y.PartialMap Z
W : X.Opens
hW : Dense ↑W
hW₁ : W ≤ f₁.domain
hW₂ : W ≤ f₂.domain
e : (f₁.restrict W hW hW₁).comp g = (f₂.restrict W hW hW₂).comp g
⊢ (f₁.comp g).equiv (f₂.comp g)

Tactic:
rw [comp_restrict_left, comp_restrict_left] at e

Goal state after:
X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f₁ f₂ : X.PartialMap Y
inst✝¹ : IsDominant f₁.hom
inst✝ : IsDominant f₂.hom
g : Y.PartialMap Z
W : X.Opens
hW : Dense ↑W
hW₁ : W ≤ f₁.domain
hW₂ : W ≤ f₂.domain
e :
  (f₁.comp g).restrict (f₁.domain.ι ''ᵁ f₁.hom ⁻¹ᵁ g.domain ⊓ W) ⋯ ⋯ =
    (f₂.comp g).restrict (f₂.domain.ι ''ᵁ f₂.hom ⁻¹ᵁ g.domain ⊓ W) ⋯ ⋯
⊢ (f₁.comp g).equiv (f₂.comp g)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
⊢ (opensDiagram D i U).map f ⁻¹ᵁ V = (D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V

Tactic:
ext x

Goal state after:
case e'_2
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
⊢ x ∈ ↑((opensDiagram D i U).map f ⁻¹ᵁ V) ↔
    x ∈ ↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_1
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 : Set (TopologicalSpace.Opens ↥c.pt)
hs : s ⊆ {x | ∃ i V, ∃ (_ : IsAffineOpen V), c.π.app i ⁻¹ᵁ V = x}
hsf : s.Finite
hU : IsCompact ↑(sSup s)
this : Finite ↑s
i : ↑s → I
V : (x : ↑s) → (D.obj (i x)).Opens
hV : ∀ (x : ↑s), IsAffineOpen (V x)
hVi : ∀ (x : ↑s), c.π.app (i x) ⁻¹ᵁ V x = ↑x
j : I
fj : (b : ↑s) → j ⟶ i b
⊢ IsCompact (⋃ i_1, ⇑(D.map (fj i_1)) ⁻¹' ↑(V i_1))

Tactic:
exact isCompact_iUnion fun i ↦ ((hV i).preimage _).isCompact

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
⊢ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i) = Set.range ⇑(colimit.ι d.functor i)

Tactic:
ext x

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
x : ↥d.glued
⊢ x ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i) ↔ x ∈ Set.range ⇑(colimit.ι d.functor i)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂.refine_1
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
⊢ comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) =
    ConstructibleSetData.toSet
      (Finset.image
        (fun j ↦
          { f := (LinearMap.charpoly ((Algebra.lmul R M) ((Ideal.Quotient.mk (Ideal.span {g.val i})) f))).coeff j,
            n := 0, g := 0 })
        (Finset.range (Module.finrank R M)))

Tactic:
ext x

Goal state after:
case hP₂.refine_1
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝ : Module.Free R M
this : Module.Finite R M
x : PrimeSpectrum R
⊢ x ∈ comap Polynomial.C '' (zeroLocus (Set.range g.val) \ zeroLocus {f}) ↔
    x ∈
      ConstructibleSetData.toSet
        (Finset.image
          (fun j ↦
            { f := (LinearMap.charpoly ((Algebra.lmul R M) ((Ideal.Quotient.mk (Ideal.span {g.val i})) f))).coeff j,
              n := 0, g := 0 })
          (Finset.range (Module.finrank R M)))
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⟩ ↦ ?_⟩

Goal state after:
case refine_1
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
⊢ ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U

case refine_2
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✝ : ∃ V, IsCompact V.carrier ∧ f default '' V.carrier = U
V : Opens (X default)
hc : IsCompact V.carrier
h : f default '' V.carrier = U
⊢ IsCompactOpenCovered f U
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: 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_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app a ≫
      (MorphismProperty.Over.map ⊤ ⋯).map iso1.hom ≫
        (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    ((MorphismProperty.Over.map ⊤ ⋯).mapCocone (d.cocone i)).ι.app a ≫ d.transitionMap hij

Tactic:
dsimp only [Functor.comp_obj, Functor.id_obj, Functor.mapCocone_pt, Functor.const_obj_obj,
      Functor.mapCocone_ι_app, Iso.trans_hom, Functor.isoWhiskerLeft_hom, Iso.symm_hom]

Goal state after:
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_2} 𝒰.I₀
inst✝¹ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone i).pt ≅ ((MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)).mapCocone (d.cocone j)).pt :=
  (d.isColimit i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij)) (d.isColimit j))
    (D.isoWhiskerLeft (MorphismProperty.Over.pullbackComp (Cover.trans 𝒰 hij) (𝒰.f j) (𝒰.f i) ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))).symm)
a : J
⊢ (MorphismProperty.Over.map ⊤ ⋯).map ((d.cocone i).ι.app a) ≫
      (MorphismProperty.Over.map ⊤ ⋯).map iso1.hom ≫
        (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans 𝒰 hij) ⋯ trivial).counit.app (d.cocone j).pt =
    (MorphismProperty.Over.map ⊤ ⋯).map ((d.cocone i).ι.app a) ≫ d.transitionMap hij
Module: Mathlib.Topology.Sets.CompactOpenCovered

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

Tactic:
ext x

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

Goal state before:
pp: 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.266} 𝒰.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.266} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : (a : J) → (D.obj a).left.OpenCover := fun a ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).hom 𝒰
a b : J
f : a ⟶ b
i : (𝒱 a).I₀
⊢ (𝒱 a).f i ≫ (D.map f).left = ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f).left ≫ (𝒱 b).f i

Tactic:
simp [𝒱]

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

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
⊢ numBound k D 0 = k

Tactic:
rw [numBound]

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

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound k D (n + 1) = numBound k D n * degBound k D n * D n

Tactic:
rw [numBound]

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
⊢ W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)

Tactic:
nonsingular_iff',

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0

Tactic:
nonsingular_iff',

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔
    (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ ↑1⁻¹ ^ 6 * (W.a₆ + x * W.a₄ + x ^ 2 * W.a₂ + x ^ 3 - y * W.a₃ - y ^ 2 - x * y * W.a₁) = 0 ∧
      (2 * y + W.a₁ * x + W.a₃ ≠ 0 ∨ -(W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)) ≠ 0) ↔
    ↑1⁻¹ ^ 6 * (W.a₆ + x * W.a₄ + x ^ 2 * W.a₂ + x ^ 3 - y * W.a₃ - y ^ 2 - x * y * W.a₁) = 0 ∧
      (1 ^ 3 * (W.a₃ + x * W.a₁ + 2 * y) ≠ 0 ∨
        1 ^ 4 * (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * x ^ 2 - 2 * 0 * y) ≠ 0)

Tactic:
congr! 3 <;> ring1

Goal state after: