import Mathlib

set_option autoImplicit false
set_option maxHeartbeats 1600000
set_option synthInstance.maxHeartbeats 600000

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry RingHom

noncomputable section

universe u

namespace AlgebraicGeometry

namespace KwSmoothIrredRelDimConstantEngine

theorem kwSmoothIrredRelDimConstantEngine_axiomAnchor : True :=
  have _h₁ : True = True := propext Iff.rfl
  have _h₂ : ℕ := Classical.choice ⟨0⟩
  have _h₃ : Quot.mk (fun (_ _ : ℕ) => True) 0 = Quot.mk (fun (_ _ : ℕ) => True) 1 :=
    Quot.sound trivial
  trivial

theorem kw_isStandardSmoothOfRelativeDimension_finrank
    {R : Type*} {S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.IsStandardSmooth R S] [Nontrivial S] :
    Algebra.IsStandardSmoothOfRelativeDimension (Module.finrank S (Ω[S⁄R])) R S := by
  rw [Algebra.IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth, Module.finrank,
    Cardinal.cast_toNat_of_lt_aleph0]
  exact Module.rank_lt_aleph0 S (Ω[S⁄R])

theorem kw_isStandardSmoothOfRelativeDimension_unique
    {R : Type*} {S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Nontrivial S] {n m : ℕ}
    (hn : Algebra.IsStandardSmoothOfRelativeDimension n R S)
    (hm : Algebra.IsStandardSmoothOfRelativeDimension m R S) : n = m := by
  have h1 := @Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential R S _ _ _ _ n hn
  have h2 := @Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential R S _ _ _ _ m hm
  exact Nat.cast_injective (h1.symm.trans h2)

section SchemeLevel

variable {X Y : Scheme.{u}}

theorem kw_isStandardSmoothOfRelDim_basicOpen {g : X ⟶ Y} [IsAffine Y]
    {V : X.Opens} (hV : IsAffineOpen V) {n : ℕ}
    (h : (g.appLE ⊤ V le_top).hom.IsStandardSmoothOfRelativeDimension n) (s : Γ(X, V)) :
    (g.appLE ⊤ (X.basicOpen s) le_top).hom.IsStandardSmoothOfRelativeDimension n := by
  haveI := hV.isLocalization_basicOpen s
  have hfac : g.appLE ⊤ V le_top ≫ X.presheaf.map (homOfLE (X.basicOpen_le s)).op
      = g.appLE ⊤ (X.basicOpen s) le_top := g.appLE_map _ _
  rw [← hfac, CommRingCat.hom_comp]
  exact (isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n).right
    _ s _ h

theorem kw_exists_relDim_appLE_top_of_relDim
    (g : X ⟶ Y) [IsAffine Y] (n : ℕ) [hg : SmoothOfRelativeDimension n g] (x : X) :
    ∃ (V : X.Opens) (_ : IsAffineOpen V), x ∈ V ∧
      (g.appLE ⊤ V le_top).hom.IsStandardSmoothOfRelativeDimension n := by
  obtain ⟨_, ⟨V₀, hV₀, rfl⟩, hxV₀, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
  have hloc : RingHom.Locally (RingHom.IsStandardSmoothOfRelativeDimension n)
      (g.appLE ⊤ V₀ le_top).hom :=
    HasRingHomProperty.appLE (@SmoothOfRelativeDimension n) g hg
      ⟨⊤, isAffineOpen_top Y⟩ ⟨V₀, hV₀⟩ le_top
  obtain ⟨T, hTspan, hT⟩ := hloc
  have hcov : V₀ ≤ ⨆ t : T, X.basicOpen (t : Γ(X, V₀)) :=
    (hV₀.self_le_iSup_basicOpen_iff).mpr hTspan
  obtain ⟨t, hxt⟩ : ∃ t : T, x ∈ X.basicOpen (t : Γ(X, V₀)) := by
    have := hcov hxV₀
    simpa [TopologicalSpace.Opens.mem_iSup] using this
  refine ⟨X.basicOpen (t : Γ(X, V₀)), hV₀.basicOpen _, hxt, ?_⟩
  haveI := hV₀.isLocalization_basicOpen (t : Γ(X, V₀))
  have hfac : g.appLE ⊤ V₀ le_top ≫ X.presheaf.map (homOfLE (X.basicOpen_le _)).op
      = g.appLE ⊤ (X.basicOpen (t : Γ(X, V₀))) le_top := g.appLE_map _ _
  rw [← hfac, CommRingCat.hom_comp]
  have hres := isStandardSmoothOfRelativeDimension_respectsIso.left _
    (IsLocalization.algEquiv (.powers (t : Γ(X, V₀))) (Localization.Away (t : Γ(X, V₀)))
      Γ(X, X.basicOpen (t : Γ(X, V₀)))).toRingEquiv (hT t t.2)
  convert hres using 2
  rw [← RingHom.comp_assoc]; congr 1
  exact ((IsLocalization.algEquiv (.powers (t : Γ(X, V₀))) (Localization.Away (t : Γ(X, V₀)))
    Γ(X, X.basicOpen (t : Γ(X, V₀)))).toAlgHom.comp_algebraMap).symm

theorem kw_exists_relDim_appLE_top
    (g : X ⟶ Y) [IsAffine Y] [Smooth g] (x : X) :
    ∃ (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (r : ℕ),
      (g.appLE ⊤ V le_top).hom.IsStandardSmoothOfRelativeDimension r := by
  obtain ⟨_, ⟨V₀, hV₀, rfl⟩, hxV₀, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
  have hloc : RingHom.Locally RingHom.IsStandardSmooth (g.appLE ⊤ V₀ le_top).hom := by
    rw [← smooth_iff_locally_isStandardSmooth]
    exact g.smooth_appLE (isAffineOpen_top Y) hV₀ le_top
  obtain ⟨T, hTspan, hT⟩ := hloc
  have hcov : V₀ ≤ ⨆ t : T, X.basicOpen (t : Γ(X, V₀)) :=
    (hV₀.self_le_iSup_basicOpen_iff).mpr hTspan
  obtain ⟨t, hxt⟩ : ∃ t : T, x ∈ X.basicOpen (t : Γ(X, V₀)) := by
    have := hcov hxV₀
    simpa [TopologicalSpace.Opens.mem_iSup] using this
  haveI := hV₀.isLocalization_basicOpen (t : Γ(X, V₀))
  haveI : Nontrivial Γ(X, X.basicOpen (t : Γ(X, V₀))) :=
    @Scheme.component_nontrivial X _ ⟨⟨x, hxt⟩⟩
  have hfac : g.appLE ⊤ V₀ le_top ≫ X.presheaf.map (homOfLE (X.basicOpen_le _)).op
      = g.appLE ⊤ (X.basicOpen (t : Γ(X, V₀))) le_top := g.appLE_map _ _
  have hstd : (g.appLE ⊤ (X.basicOpen (t : Γ(X, V₀))) le_top).hom.IsStandardSmooth := by
    rw [← hfac, CommRingCat.hom_comp]
    have hres := isStandardSmooth_respectsIso.left _
      (IsLocalization.algEquiv (.powers (t : Γ(X, V₀))) (Localization.Away (t : Γ(X, V₀)))
        Γ(X, X.basicOpen (t : Γ(X, V₀)))).toRingEquiv (hT t t.2)
    convert hres using 2
    rw [← RingHom.comp_assoc]; congr 1
    exact ((IsLocalization.algEquiv (.powers (t : Γ(X, V₀))) (Localization.Away (t : Γ(X, V₀)))
      Γ(X, X.basicOpen (t : Γ(X, V₀)))).toAlgHom.comp_algebraMap).symm
  algebraize [(g.appLE ⊤ (X.basicOpen (t : Γ(X, V₀))) le_top).hom]
  exact ⟨X.basicOpen (t : Γ(X, V₀)), hV₀.basicOpen _, hxt, _,
    kw_isStandardSmoothOfRelativeDimension_finrank⟩

theorem kw_relDim_eq_of_mem_both {g : X ⟶ Y} [IsAffine Y]
    {V₁ V₂ : X.Opens} (hV₁ : IsAffineOpen V₁) (hV₂ : IsAffineOpen V₂) {n₁ n₂ : ℕ}
    (h₁ : (g.appLE ⊤ V₁ le_top).hom.IsStandardSmoothOfRelativeDimension n₁)
    (h₂ : (g.appLE ⊤ V₂ le_top).hom.IsStandardSmoothOfRelativeDimension n₂)
    {z : X} (hz₁ : z ∈ V₁) (hz₂ : z ∈ V₂) : n₁ = n₂ := by
  obtain ⟨s₁, hs₁le, hzs₁⟩ := hV₁.exists_basicOpen_le ⟨z, hz₂⟩ hz₁
  have h₁' := kw_isStandardSmoothOfRelDim_basicOpen hV₁ h₁ s₁
  obtain ⟨s₂, hs₂le, hzs₂⟩ :=
    hV₂.exists_basicOpen_le ⟨z, show z ∈ X.basicOpen s₁ from hzs₁⟩ hz₂
  have h₂' := kw_isStandardSmoothOfRelDim_basicOpen hV₂ h₂ s₂

  let s₂' : Γ(X, X.basicOpen s₁) :=
    X.presheaf.map (homOfLE (hs₁le : X.basicOpen s₁ ≤ V₂)).op s₂
  have hEq : X.basicOpen s₂' = X.basicOpen s₂ := by
    have := X.basicOpen_res s₂ (homOfLE hs₁le).op
    simp only [s₂', this]; exact inf_eq_right.mpr hs₂le
  have h₁'' :
      (g.appLE ⊤ (X.basicOpen s₂) le_top).hom.IsStandardSmoothOfRelativeDimension n₁ := by
    have := kw_isStandardSmoothOfRelDim_basicOpen (hV₁.basicOpen s₁) h₁' s₂'
    rwa [hEq] at this
  haveI : Nontrivial Γ(X, X.basicOpen s₂) := @Scheme.component_nontrivial X _ ⟨⟨z, hzs₂⟩⟩
  algebraize [(g.appLE ⊤ (X.basicOpen s₂) le_top).hom]
  exact kw_isStandardSmoothOfRelativeDimension_unique h₁'' h₂'

theorem kw_appLE_top_opensImage {W : X.Opens} {g : X ⟶ Y} [IsAffine Y]
    {V : (W : Scheme.{u}).Opens} {n : ℕ}
    (h : ((W.ι ≫ g).appLE ⊤ V le_top).hom.IsStandardSmoothOfRelativeDimension n) :
    (g.appLE ⊤ (W.ι ''ᵁ V) le_top).hom.IsStandardSmoothOfRelativeDimension n := by
  have hle : V ≤ W.ι ⁻¹ᵁ (W.ι ''ᵁ V) := (Scheme.Hom.preimage_image_eq W.ι V).ge
  have hcomp : g.appLE ⊤ (W.ι ''ᵁ V) le_top ≫ W.ι.appLE (W.ι ''ᵁ V) V hle
      = (W.ι ≫ g).appLE ⊤ V le_top := Scheme.Hom.appLE_comp_appLE _ _ _ _ _ _ _
  haveI hiso : IsIso (W.ι.appLE (W.ι ''ᵁ V) V hle) := by
    have heq : W.ι.appLE (W.ι ''ᵁ V) V hle
        = W.ι.app (W.ι ''ᵁ V) ≫
          (W : Scheme.{u}).presheaf.map
            (eqToHom (Scheme.Hom.preimage_image_eq W.ι V).symm).op := by
      simp only [Scheme.Hom.appLE]; congr 1
    rw [heq]; exact IsIso.comp_isIso
  have heq2 : g.appLE ⊤ (W.ι ''ᵁ V) le_top
      = (W.ι ≫ g).appLE ⊤ V le_top ≫ inv (W.ι.appLE (W.ι ''ᵁ V) V hle) := by
    rw [← hcomp, Category.assoc, IsIso.hom_inv_id, Category.comp_id]
  rw [heq2, CommRingCat.hom_comp]
  exact isStandardSmoothOfRelativeDimension_respectsIso.left _
    (asIso (W.ι.appLE (W.ι ''ᵁ V) V hle)).symm.commRingCatIsoToRingEquiv h

theorem kw_smoothOfRelativeDimension_of_irreducible_of_nonempty_open
    (g : X ⟶ Y) [IsAffine Y] [Smooth g] [IrreducibleSpace X]
    (n : ℕ) (W : X.Opens) (hWne : (W : Set X).Nonempty)
    (hWg : SmoothOfRelativeDimension n (W.ι ≫ g)) :
    SmoothOfRelativeDimension n g := by
  have _ := kwSmoothIrredRelDimConstantEngine_axiomAnchor

  obtain ⟨w₀, hw₀W⟩ := hWne
  obtain ⟨Vw, hVw, hw₀Vw, hVwn⟩ :=
    kw_exists_relDim_appLE_top_of_relDim (X := (W : Scheme.{u})) (W.ι ≫ g) n ⟨w₀, hw₀W⟩
  have hVwX : IsAffineOpen (W.ι ''ᵁ Vw) := hVw.image_of_isOpenImmersion W.ι
  have hw₀VwX : w₀ ∈ (W.ι ''ᵁ Vw : X.Opens) := ⟨⟨w₀, hw₀W⟩, hw₀Vw, rfl⟩
  have hVwXn : (g.appLE ⊤ (W.ι ''ᵁ Vw) le_top).hom.IsStandardSmoothOfRelativeDimension n :=
    kw_appLE_top_opensImage hVwn

  constructor
  intro x
  obtain ⟨Vx, hVx, hxVx, r, hVxr⟩ := kw_exists_relDim_appLE_top g x
  obtain ⟨z, hzVx, hzVw⟩ : ((Vx : Set X) ∩ (W.ι ''ᵁ Vw : Set X)).Nonempty := by
    have := (IrreducibleSpace.isIrreducible_univ X).2 Vx (W.ι ''ᵁ Vw) Vx.2
      (W.ι ''ᵁ Vw).2 (by exact ⟨x, Set.mem_univ x, hxVx⟩)
      (by exact ⟨w₀, Set.mem_univ w₀, hw₀VwX⟩)
    simpa using this
  have hreq : r = n := kw_relDim_eq_of_mem_both hVx hVwX hVxr hVwXn hzVx hzVw
  exact ⟨⊤, isAffineOpen_top Y, Vx, hVx, hxVx, le_top, hreq ▸ hVxr⟩

theorem kw_of_comp_isOpenImmersion (P : MorphismProperty Scheme.{u})
    [IsZariskiLocalAtTarget P] {Z : Scheme.{u}} (f : X ⟶ Y) (i : Y ⟶ Z) [IsOpenImmersion i]
    (h : P (f ≫ i)) : P f := by
  have hr := IsZariskiLocalAtTarget.restrict h i.opensRange
  have hpre : (f ≫ i) ⁻¹ᵁ i.opensRange = ⊤ := by
    ext x; simp [Scheme.Hom.opensRange]
  let α : X ≅ ((f ≫ i) ⁻¹ᵁ i.opensRange : X.Opens) := X.topIso.symm ≪≫ X.isoOfEq hpre.symm
  have hα : α.hom ≫ ((f ≫ i) ⁻¹ᵁ i.opensRange).ι = 𝟙 X := by
    simp [α, ← Scheme.topIso_hom]
  have harr : Arrow.mk f ≅ Arrow.mk ((f ≫ i) ∣_ i.opensRange) :=
    Arrow.isoMk α i.isoOpensRange <| by
      dsimp only [Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom]
      rw [← cancel_mono i.opensRange.ι, Category.assoc, morphismRestrict_ι,
        ← Category.assoc, hα, Category.id_comp, Category.assoc,
        Scheme.Hom.isoOpensRange_hom_ι]
  exact (P.arrow_mk_iso_iff harr).mpr hr

theorem kw_smoothOfRelativeDimension_of_irreducible_of_isOpenImmersion
    (g : X ⟶ Y) [IsAffine Y] [Smooth g] [IrreducibleSpace X]
    (n : ℕ) {W : Scheme.{u}} (i : W ⟶ X) [IsOpenImmersion i] [Nonempty W]
    (hig : SmoothOfRelativeDimension n (i ≫ g)) :
    SmoothOfRelativeDimension n g := by
  haveI := smoothOfRelativeDimension_isStableUnderBaseChange (n := n)
  refine kw_smoothOfRelativeDimension_of_irreducible_of_nonempty_open g n i.opensRange
    ⟨i (Classical.arbitrary W), ⟨_, rfl⟩⟩ ?_
  rw [← MorphismProperty.cancel_left_of_respectsIso (P := @SmoothOfRelativeDimension n)
    i.isoOpensRange.hom (i.opensRange.ι ≫ g), ← Category.assoc,
    Scheme.Hom.isoOpensRange_hom_ι]
  exact hig

end SchemeLevel

end KwSmoothIrredRelDimConstantEngine

end AlgebraicGeometry

namespace AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine

theorem kw_not_isStandardSmoothOfRelDim_succ_of_finite
    {k : Type*} [Field k] [PerfectField k]
    {A : Type*} [CommRing A] [Algebra k A] [Nontrivial A] [Module.Finite k A]
    [_root_.IsReduced A] (n : ℕ) :
    ¬ Algebra.IsStandardSmoothOfRelativeDimension (n + 1) k A := by
  intro hsm
  obtain ⟨ι, σ, _, _, P, hPdim⟩ := hsm

  have hne : Nonempty ((Set.range P.map)ᶜ : Set ι) := by
    haveI : _root_.Finite ((Set.range P.map)ᶜ : Set ι) := Subtype.finite
    have hcard : Nat.card ((Set.range P.map)ᶜ : Set ι) = n + 1 := by
      have := Module.finrank_eq_nat_card_basis P.basisKaehler
      rw [Module.finrank, P.rank_kaehlerDifferential, hPdim, Cardinal.toNat_natCast] at this
      exact this.symm
    exact Nat.card_pos_iff.mp (hcard ▸ Nat.succ_pos n) |>.1
  obtain ⟨⟨i₀, hi₀⟩⟩ := hne
  set a : A := P.val i₀ with ha

  have hDa_free : ∀ x : A, x • (KaehlerDifferential.D k A) a = 0 → x = 0 := by
    intro x hx
    rw [(P.basisKaehler_apply ⟨i₀, hi₀⟩).symm] at hx
    have hrepr : P.basisKaehler.repr (x • P.basisKaehler ⟨i₀, hi₀⟩) ⟨i₀, hi₀⟩ = 0 := by
      rw [hx]; simp
    rw [map_smul, Module.Basis.repr_self, Finsupp.smul_single, smul_eq_mul, mul_one,
      Finsupp.single_eq_same] at hrepr
    exact hrepr

  haveI hAint : Algebra.IsIntegral k A := Algebra.IsIntegral.of_finite k A
  have hint : _root_.IsIntegral k a := hAint.isIntegral a
  set p := minpoly k a with hp
  have hpdeg : 0 < p.natDegree := minpoly.natDegree_pos hint
  have hpa : Polynomial.aeval a p = 0 := minpoly.aeval k a

  have hD0 : Polynomial.aeval a p.derivative • (KaehlerDifferential.D k A) a = 0 := by
    rw [← Derivation.map_aeval, hpa, map_zero]
  have hp'a : Polynomial.aeval a p.derivative = 0 := hDa_free _ hD0

  have hp'ker : p.derivative ∈ RingHom.ker (Polynomial.aeval a : Polynomial k →ₐ[k] A) := hp'a
  rw [minpoly.ker_aeval_eq_span_minpoly k a, ← hp] at hp'ker
  have hp'0 : p.derivative = 0 := by
    rcases Submodule.mem_span_singleton.mp hp'ker with ⟨q, hq⟩
    by_contra hne0
    have hdeg : p.derivative.natDegree < p.natDegree :=
      Polynomial.natDegree_derivative_lt hpdeg.ne'
    rw [← hq, smul_eq_mul] at hdeg hne0
    have hqne : q ≠ 0 := left_ne_zero_of_mul (by simpa using hne0)
    have hpne : p ≠ 0 := minpoly.ne_zero hint
    rw [Polynomial.natDegree_mul hqne hpne] at hdeg
    omega

  have hnotsep : ¬ p.Separable := by
    rw [Polynomial.separable_def, hp'0, isCoprime_zero_right]
    exact fun hu ↦ (minpoly.degree_pos hint).ne'
      (hp ▸ Polynomial.isUnit_iff_degree_eq_zero.mp hu)

  refine hnotsep (PerfectField.separable_iff_squarefree.mpr ?_)
  intro q hq2

  obtain ⟨c, hc⟩ := hq2
  have hqc0 : (Polynomial.aeval a (q * c)) ^ 2 = 0 := by
    have heq : (q * c) ^ 2 = p * c := by rw [hc]; ring
    rw [← map_pow, heq, map_mul, hpa, zero_mul]
  have hqcmem : q * c ∈ RingHom.ker (Polynomial.aeval a : Polynomial k →ₐ[k] A) :=
    (IsNilpotent.eq_zero ⟨2, hqc0⟩ : _)
  rw [minpoly.ker_aeval_eq_span_minpoly, ← hp, Ideal.mem_span_singleton, hc] at hqcmem

  rcases eq_or_ne (q * c) 0 with hqc | hqcne
  · have : p = 0 := by rw [hc, show q * q * c = q * (q * c) from by ring, hqc, mul_zero]
    exact absurd this (minpoly.ne_zero hint)
  · have hcan : q * (q * c) ∣ 1 * (q * c) := by
      rw [one_mul, ← mul_assoc]; exact hqcmem
    exact isUnit_of_dvd_one ((mul_dvd_mul_iff_right hqcne).mp hcan)

end AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine

end

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kwSmoothIrredRelDimConstantEngine_axiomAnchor' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kwSmoothIrredRelDimConstantEngine_axiomAnchor

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelativeDimension_unique' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelativeDimension_unique

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_smoothOfRelativeDimension_of_irreducible_of_nonempty_open' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_smoothOfRelativeDimension_of_irreducible_of_nonempty_open

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_of_comp_isOpenImmersion' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_of_comp_isOpenImmersion

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_not_isStandardSmoothOfRelDim_succ_of_finite' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_not_isStandardSmoothOfRelDim_succ_of_finite

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelativeDimension_finrank' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelativeDimension_finrank

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelDim_basicOpen' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_isStandardSmoothOfRelDim_basicOpen

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_exists_relDim_appLE_top_of_relDim' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_exists_relDim_appLE_top_of_relDim

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_exists_relDim_appLE_top' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_exists_relDim_appLE_top

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_relDim_eq_of_mem_both' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_relDim_eq_of_mem_both

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_appLE_top_opensImage' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_appLE_top_opensImage

/--
info: 'AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_smoothOfRelativeDimension_of_irreducible_of_isOpenImmersion' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs (whitespace := lax) in
#print axioms AlgebraicGeometry.KwSmoothIrredRelDimConstantEngine.kw_smoothOfRelativeDimension_of_irreducible_of_isOpenImmersion