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

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (SpecIso n S).hom ≫ (Arrow.mk (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))).hom =
    (Arrow.mk (map n (Spec.map φ))).hom ≫ (SpecIso n R).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S T : Scheme
f : S ⟶ T
⊢ IsPullback (map n f) (𝔸(n; S) ↘ S) (𝔸(n; T) ↘ T) f

Tactic:
by

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 ι
φ : ↑Γ(T, UT) ⊗[↑Γ(S, US)] ((i : ι) → ↑Γ(X, VX i)) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  (RingHom.pi fun i ↦
        (CommRingCat.Hom.hom (pushoutSection H hUST ⋯ ⋯)).comp
          ((CommRingCat.Hom.hom ⋯.isoPushout.hom).comp
            (Pi.evalRingHom (fun i ↦ ↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, VX i)) i))).comp
    (Algebra.TensorProduct.piRight ↑Γ(S, US) ↑Γ(S, US) ↑Γ(T, UT) fun i ↦ ↑Γ(X, VX i)).toRingEquiv.toRingHom
hφ : Function.Injective ⇑φ
e : pushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≅
  CommRingCat.of (↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, UX)) :=
  ⋯.isoPushout.symm
this :
  (ψY.comp (CommRingCat.Hom.hom (pushoutSection H hUST hUSX hUY))).comp (CommRingCat.Hom.hom e.inv) =
    φ.comp (Algebra.TensorProduct.map (AlgHom.id ↑Γ(T, UT) ↑Γ(T, UT)) ψ).toRingHom
⊢ Function.Injective ⇑(ConcreteCategory.hom (pushoutSection H hUST hUSX hUY))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ reindex id S = 𝟙 𝔸(n; S)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (i ≫ j))) S =
    reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n₁ n₂ : Type u
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ map n₂ f ≫ reindex i T = reindex i S ≫ map n₁ f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type uᵒᵖ
⊢ { app := reindex ⇑(ConcreteCategory.hom (𝟙 n).unop), naturality := ⋯ } =
    𝟙 { obj := AffineSpace (Opposite.unop n), map := fun {X Y} ↦ map (Opposite.unop n), map_id := ⋯, map_comp := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { app := reindex ⇑(ConcreteCategory.hom (f ≫ g).unop), naturality := ⋯ } =
    { app := reindex ⇑(ConcreteCategory.hom f.unop), naturality := ⋯ } ≫
      { app := reindex ⇑(ConcreteCategory.hom g.unop), naturality := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ Surjective (terminal.from (Spec ℤ[n]))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : Finite n
⊢ LocallyOfFinitePresentation (terminal.from (Spec ℤ[n]))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
j j' : J
x : F.obj j
x' : F.obj j'
eq : c.ι j x = c.ι j' x'
⊢ c.ι (IsFiltered.max j j') ((ConcreteCategory.hom (F.map (leftToMax j j'))) x) =
    c.ι (IsFiltered.max j j') ((ConcreteCategory.hom (F.map (rightToMax j j'))) x')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
h :
  ∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'
j j' : J
x : F.obj j
x' : F.obj j'
eq✝ : c.ι j x = c.ι j' x'
k : J
g : IsFiltered.max j j' ⟶ k
eq :
  (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map (leftToMax j j'))) x) =
    (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map (rightToMax j j'))) x')
⊢ (ConcreteCategory.hom (F.map (leftToMax j j' ≫ g))) x = (ConcreteCategory.hom (F.map (rightToMax j j' ≫ g))) x'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ IsOpenMap ⇑(𝔸(n; S) ↘ S)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ GeometricallyIrreducible (𝔸(n; S) ↘ S)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ GeometricallyReduced (𝔸(n; S) ↘ S)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
h : IsReduced S
⊢ IsReduced 𝔸(n; S)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝ : IsEmpty n
⊢ isomorphisms Scheme (terminal.from (Spec ℤ[n]))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↥(Spec R)
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
p : Polynomial ↑R
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
⊢ ((rename fun x ↦ i).comp ↑(uniqueAlgEquiv (↑R) PUnit.{u + 1}).symm) p = 0

Tactic:
by

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 ι
φ : ↑Γ(T, UT) ⊗[↑Γ(S, US)] ((i : ι) → ↑Γ(X, VX i)) →+* (i : ι) → ↑Γ(Y, g ⁻¹ᵁ VX i ⊓ iY ⁻¹ᵁ UT) :=
  (RingHom.pi fun i ↦
        (CommRingCat.Hom.hom (pushoutSection H hUST ⋯ ⋯)).comp
          ((CommRingCat.Hom.hom ⋯.isoPushout.hom).comp
            (Pi.evalRingHom (fun i ↦ ↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, VX i)) i))).comp
    (Algebra.TensorProduct.piRight ↑Γ(S, US) ↑Γ(S, US) ↑Γ(T, UT) fun i ↦ ↑Γ(X, VX i)).toRingEquiv.toRingHom
hφ : Function.Injective ⇑φ
e : pushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≅
  CommRingCat.of (↑Γ(T, UT) ⊗[↑Γ(S, US)] ↑Γ(X, UX)) :=
  ⋯.isoPushout.symm
H₁ :
  (CommRingCat.Hom.hom e.inv).comp Algebra.TensorProduct.includeLeftRingHom =
    CommRingCat.Hom.hom (pushout.inr (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST))
x : ↑Γ(T, UT)
j : ι
⊢ VX j ≤ iX ⁻¹ᵁ US

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ IsIntegralHom (𝔸(n; S) ↘ S) ↔ IsEmpty ↥S ∨ IsEmpty n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
inst✝¹ : Nonempty ↥S
inst✝ : Nonempty n
⊢ ¬IsIntegralHom (𝔸(n; S) ↘ S)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: R : CommRingCat
p q : ↥(Spec R)
⊢ p ≤ q ↔ q.asIdeal ≤ p.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
R : CommRingCat
⊢ inferInstance = inferInstance

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
⊢ IsFinite (X.fromSpecResidueField x ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
⊢ IsIso (Spec.preimage (X.fromSpecResidueField x ≫ f))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
⊢ pointOfClosedPoint f x hx ≫ f = 𝟙 (Spec (CommRingCat.of K))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
a : ↥(Spec (CommRingCat.of K))
⊢ (pointOfClosedPoint f x hx) a = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ ↑p (IsLocalRing.closedPoint K) ∈ closedPoints ↥X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ (fun x ↦ ⟨pointOfClosedPoint f ↑x ⋯, ⋯⟩) ((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p) = p

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x✝ : ↥X
hx : IsClosed {x✝}
x : ↑(closedPoints ↥X)
⊢ (fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) ((fun x ↦ ⟨pointOfClosedPoint f ↑x ⋯, ⋯⟩) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
this : JacobsonSpace ↥X
x : ↥X
hxS : x ∈ S
hx : x ∈ closedPoints ↥X
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) (IsLocalRing.closedPoint K) =
    (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) (IsLocalRing.closedPoint K)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst✝³ : IsSeparated i
inst✝² : LocallyOfFiniteType i
inst✝¹ : IsReduced X
inst✝ : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed {x} → f x = g x
H' : f ≫ i = g ≫ i
⊢ f = g

Tactic:
by

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

Goal state before:
pp: 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 :
  ∀ (x : Fin n),
    (Polynomial.C (IsLocalization.Away.invSelf (e.val i).leadingCoeff) *
          Polynomial.map (algebraMap R (Away (e.val i).leadingCoeff)) (e.val x)).degree =
      (e.val x).degree
j : Fin n
hj :
  ¬Polynomial.C (IsLocalization.Away.invSelf (e.val i).leadingCoeff) *
        Polynomial.map (algebraMap R (Away (e.val i).leadingCoeff)) (e.val j) =
      0
H : e.val j = 0
⊢ False

Tactic:
by

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
⊢ (support fun x ↦ 0) ⊆ U

Tactic:
by

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
z : X
hz : z ∈ U
⊢ ∃ t ∈ 𝓝 z, (t ∩ support fun x ↦ 0).Finite

Tactic:
by

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✝¹ : T1Space X
inst✝ : Zero Y
f : X → Y
h : support f ⊆ U
⊢ support f = U \ {x | f x = 0 x}

Tactic:
by

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✝¹ : 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

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:
by

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:
by

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
⊢ (LocallyFinite fun s ↦ {↑s}) ↔ LocallyFiniteSupport f

Tactic:
by

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:
by

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
⊢ (W ∩ support f).Finite

Tactic:
by

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 : locallyFinsupp X Y
x✝ : X
⊢ x✝ ∈ univ

Tactic:
by

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
x✝¹ x✝ : locallyFinsuppWithin U Y
toFun✝¹ : X → Y
supportWithinDomain'✝¹ : support toFun✝¹ ⊆ U
supportLocallyFiniteWithinDomain'✝¹ : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support toFun✝¹).Finite
toFun✝ : X → Y
supportWithinDomain'✝ : support toFun✝ ⊆ U
supportLocallyFiniteWithinDomain'✝ : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ support toFun✝).Finite
⊢ (fun D ↦ D.toFun)
        { toFun := toFun✝¹, supportWithinDomain' := supportWithinDomain'✝¹,
          supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'✝¹ } =
      (fun D ↦ D.toFun)
        { toFun := toFun✝, supportWithinDomain' := supportWithinDomain'✝,
          supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'✝ } →
    { toFun := toFun✝¹, supportWithinDomain' := supportWithinDomain'✝¹,
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'✝¹ } =
      { toFun := toFun✝, supportWithinDomain' := supportWithinDomain'✝,
        supportLocallyFiniteWithinDomain' := supportLocallyFiniteWithinDomain'✝ }

Tactic:
by

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✝¹ : DecidableEq X
inst✝ : Zero Y
x : X
y : Y
z : X
hz : z ∈ Function.support (Pi.single x y)
⊢ z ∈ univ

Tactic:
by

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✝¹ : DecidableEq X
inst✝ : Zero Y
x : X
y : Y
x✝¹ : X
x✝ : x✝¹ ∈ univ
⊢ (univ ∩ Function.support (Pi.single x y)).Finite

Tactic:
by

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₂ : X
y : Y
⊢ (single x₁ y) x₂ = if x₂ = x₁ then y else 0

Tactic:
by

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:
by

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
y : Y
⊢ ⇑(single x y) = Pi.single x y

Tactic:
by

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

Tactic:
by

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
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
⊢ ⇑D =ᶠ[codiscreteWithin U] 0

Tactic:
by

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
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
hx : x ∈ D.support
⊢ x ∈ {x | D x = 0}ᶜ

Tactic:
by

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
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
⊢ D.support = {x | D x = 0}ᶜ ∩ U

Tactic:
by

Goal state after: