mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝ : IsIso (pushoutSection H hUST hUSX hUY)
⊢ Scheme.Hom.appLE f US UT hUST ≫ (Iso.refl Γ(T, UT)).hom = (Iso.refl Γ(S, US)).hom ≫ Scheme.Hom.appLE f US UT hUST

Tactic:
simp

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
x✝ : IsIso (pushoutSection H hUST hUSX hUY)
⊢ pushout.inl (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≫
      (asIso (pushoutSection H hUST hUSX hUY)).hom =
    (Iso.refl Γ(X, UX)).hom ≫ Scheme.Hom.appLE g UX UY ⋯

Tactic:
simp

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
x✝ : IsIso (pushoutSection H hUST hUSX hUY)
⊢ pushout.inr (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≫
      (asIso (pushoutSection H hUST hUSX hUY)).hom =
    (Iso.refl Γ(T, UT)).hom ≫ Scheme.Hom.appLE iY UT UY ⋯

Tactic:
simp

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE iY UT UY ⋯ ≫ hUT.isoSpec.hom =
    hUY'.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app iY UT ≫ Y.presheaf.map (homOfLE ⋯).op))

Tactic:
simp

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE g UX UY ⋯ ≫ hUX.isoSpec.hom =
    hUY'.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app g UX ≫ Y.presheaf.map (homOfLE ⋯).op))

Tactic:
simp

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE f US UT hUST ≫ hUS.isoSpec.hom =
    hUT.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app f US ≫ T.presheaf.map (homOfLE hUST).op))

Tactic:
simp

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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this✝¹ : IsAffine ↑US
this✝ : IsAffine ↑UT
this : IsAffine ↑UX
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE iX US UX hUSX ≫ hUS.isoSpec.hom =
    hUX.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app iX US ≫ X.presheaf.map (homOfLE hUSX).op))

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
v : n → ↑Γ(X, ⊤)
x✝ : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
⊢ (f ≫ homOfVector g v) ≫ 𝔸(n; S) ↘ S =
    homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v) ≫ 𝔸(n; S) ↘ S

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
S X Y : Scheme
v : n → ↑Γ(Y, ⊤)
f : X ⟶ Y
g : Y ⟶ S
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (f ≫ homOfVector g v))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector (f ≫ g) (⇑(ConcreteCategory.hom (Scheme.Hom.appTop f)) ∘ v))))
      (coord S i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
⊢ s.π.app (Classical.arbitrary I) ≫ α.app (Classical.arbitrary I) =
    hcG.lift ((Cone.postcompose α).obj s) ≫ cG.π.app (Classical.arbitrary I)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j i : I
⊢ s.π.app i ≫ α.app i = hcG.lift ((Cone.postcompose α).obj s) ≫ cG.π.app i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
⊢ cF.ι.app (Classical.arbitrary I) ≫ hcF.desc ((Cocone.precompose α).obj s) =
    α.app (Classical.arbitrary I) ≫ s.ι.app (Classical.arbitrary I)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j i : I
⊢ cF.ι.app i ≫ hcF.desc ((Cocone.precompose α).obj s) = α.app i ≫ s.ι.app i

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
S : Scheme
inst✝ : IsAffine S
i✝ : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.appTop
          ((𝔸(n; S).toSpecΓ ≫
              Spec.map
                (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
            homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))))
      (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ Scheme.Hom.appTop (𝟙 S) ≫ CommRingCat.ofHom C =
    CommRingCat.ofHom C ≫
      (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv ≫
        (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom

Tactic:
simp

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

Goal state before:
pp: case left
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
j : Fin n
⊢ 0 + (e.val j).degree ≤ (e.val j).degree

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
⊢ map n (𝟙 S) ≫ 𝔸(n; S) ↘ S = 𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
S : Scheme
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (𝟙 S)))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
⊢ map n (f ≫ g) ≫ 𝔸(n; S'') ↘ S'' = (map n f ≫ map n g) ≫ 𝔸(n; S'') ↘ S''

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
S S' S'' : Scheme
f : S ⟶ S'
g : S' ⟶ S''
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (map n (f ≫ g)))) (coord S'' i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n f ≫ map n g))) (coord S'' i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
⊢ reindex id S ≫ 𝔸(n; S) ↘ S = 𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n : Type u
S : Scheme
i✝ : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex id S))) (coord S i✝) =
    (ConcreteCategory.hom (Scheme.Hom.appTop (𝟙 𝔸(n; S)))) (coord S i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (i ≫ j))) S ≫ 𝔸((fun X ↦ X) n₁; S) ↘ S =
    (reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S) ≫ 𝔸((fun X ↦ X) n₁; S) ↘ S

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n₁ n₂ n₃ : Type u
i : n₁ ⟶ n₂
j : n₂ ⟶ n₃
S : Scheme
k : (fun X ↦ X) n₁
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (reindex (⇑(ConcreteCategory.hom (i ≫ j))) S))) (coord S k) =
    (ConcreteCategory.hom
        (Scheme.Hom.appTop (reindex (⇑(ConcreteCategory.hom j)) S ≫ reindex (⇑(ConcreteCategory.hom i)) S)))
      (coord S k)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n₁ n₂ : Type u
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ (map n₂ f ≫ reindex i T) ≫ 𝔸(n₁; T) ↘ T = (reindex i S ≫ map n₁ f) ≫ 𝔸(n₁; T) ↘ T

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₂
n₁ n₂ : Type u
i : n₁ → n₂
S T : Scheme
f : S ⟶ T
⊢ ∀ (i_1 : n₁),
    (ConcreteCategory.hom (Scheme.Hom.appTop (map n₂ f ≫ reindex i T))) (coord T i_1) =
      (ConcreteCategory.hom (Scheme.Hom.appTop (reindex i S ≫ map n₁ f))) (coord T i_1)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
⊢ topologically (@IsOpenMap) (𝔸(n; Spec R) ↘ Spec R)

Tactic:
← MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)
    (SpecIso n R).inv,

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
⊢ topologically (@IsOpenMap) ((SpecIso n R).inv ≫ 𝔸(n; Spec R) ↘ Spec R)
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:
simp

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

Goal state before:
pp: case refine_1
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
⊢ Polynomial.degree ∘ { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff}))) ∘ e.val }.val ≤
    Polynomial.degree ∘ e.val

Tactic:
intro j

Goal state after:
case refine_1
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
j : Fin n
⊢ (Polynomial.degree ∘ { val := ⇑(mapRingHom (algebraMap R (R ⧸ Ideal.span {(e.val i).leadingCoeff}))) ∘ e.val }.val)
      j ≤
    (Polynomial.degree ∘ e.val) j
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:
simp

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

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
x : X
⊢ D₁ x ≤ (D₁ ⊔ D₂) x

Tactic:
simp

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
x : X
⊢ D₂ x ≤ (D₁ ⊔ D₂) x

Tactic:
simp

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
x : X
⊢ (D₁ ⊓ D₂) x ≤ D₁ x

Tactic:
simp

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
x : X
⊢ (D₁ ⊓ D₂) x ≤ D₂ x

Tactic:
simp

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
inst✝ : Finite ι
VX : ι → X.Opens
hVU : iSup VX = UX
hV : ∀ (i : ι), IsIso (pushoutSection H hUST ⋯ ⋯)
hV' : ∀ (i j : ι), Mono (pushoutSection H hUST ⋯ ⋯)
hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat
D : CategoryTheory.Pairwise ι ⥤ X.Opens := Pairwise.diagram VX
h : iSup D.obj = UX
c₀ : Cocone D := (colimit.cocone D).extend (eqToIso ⋯).hom
F : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ CommRingCat :=
  Under.lift (D.op ⋙ X.presheaf)
      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
        (Functor.mapCone X.presheaf c₀.op).π) ⋙
    Under.pushout (Scheme.Hom.appLE f US UT hUST) ⋙ Under.forget Γ(T, UT)
G : X.Opens ⥤ Y.Opens :=
  { obj := fun U ↦ g ⁻¹ᵁ U ⊓ iY ⁻¹ᵁ UT, map := fun {X_1 Y_1} h ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }
i : (CategoryTheory.Pairwise ι)ᵒᵖ
⊢ ((Under.lift (D.op ⋙ X.presheaf)
            ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).map (Scheme.Hom.appLE iX US UX hUSX) ≫
              (Functor.mapCone X.presheaf c₀.op).π)).obj
        i).hom =
    Scheme.Hom.appLE iX US (D.obj (unop i)) ?m.500

Tactic:
simp

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

Goal state before:
pp: R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i✝ : Fin n
e : InductionObj R n
hi : c = (e.val i✝).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₁span : ∀ x ∈ T₁, ∀ (i : Fin x.n), x.g i ∈ coeffSubmodule R₀ e₁ ^ e₁.powBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
hT₂span : ∀ x ∈ T₂, ∀ (i : Fin x.n), x.g i ∈ coeffSubmodule R₀ e₂ ^ e₂.powBound
x✝¹ : Invertible (q₁ c) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
i : Fin n
x✝ : Localization.Away c
⊢ x✝ ∈
      coeff(Polynomial.C (IsLocalization.Away.invSelf c) *
          Polynomial.map (algebraMap R (Localization.Away c)) (e.val i)) ↔
    x✝ ∈ Set.range fun i_1 ↦ IsLocalization.Away.invSelf c * (algebraMap R (Localization.Away c)) ((e.val i).coeff i_1)

Tactic:
simp

Goal state after: