awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
T : Type u_2
inst_4 : CommRing T
f : R →+* S
g : S →+* T
H₁ : ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)
H₂ : ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)
s : Set (PrimeSpectrum T)
hs : IsConstructible s
⊢ IsConstructible (comap (g.comp f) '' s)
have refine_2 : IsConstructible (comap f '' comap g '' s)
Tactic: simp only [comap_comp, Set.image_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
inst_4 : Algebra.FinitePresentation R S
⊢ IsOpenMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (comap (algebraMap R S))
have rw : ∀ s ∈ Set.image (α := TopologicalSpace.Opens (PrimeSpectrum S)) SetLike.coe (Set.range basicOpen),
  IsOpen (X := PrimeSpectrum R) (comap (algebraMap R S) '' s)
Tactic: rw [isBasis_basic_opens.isOpenMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
have inr : ∀
  (this :
    ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
      (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
      IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U))
  (hU' : ¬∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
  IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
Tactic: wlog hU' : ∃ f, U = SetLike.coe (basicOpen f) generalizing U
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
inr :
  ∀
    (this :
      ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
        (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
        IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U))
    (hU' : ¬∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
have wlog : ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
  (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
  IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
Tactic: wlog hU' : ∃ f, U = SetLike.coe (basicOpen f) generalizing U
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
this :
  ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
    (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
hU' : ¬∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
have inr : IsOpen.{u_4} (X := PrimeSpectrum A)
  (⋃ (i : A ⊗[K] B),
    ⋃ (_ : (↑(basicOpen i) : Set (PrimeSpectrum (A ⊗[K] B))) ⊆ U),
      comap (algebraMap A (A ⊗[K] B)) '' (↑(basicOpen i) : Set (PrimeSpectrum (A ⊗[K] B))))
Tactic: rw [eq_biUnion_of_isOpen hU, Set.image_iUnion₂]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
have obtain : ∀ (f : A ⊗[K] B) (hU : IsOpen (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
  IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B))))
Tactic: obtain ⟨f, rfl⟩ := hU'
Cleared hypotheses: U, hU, hU'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
f : A ⊗[K] B
hU : IsOpen (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B))))
have obtain : ∀ (B' : Subalgebra K B) (hB : B'.FG) (f : TensorProduct.{u_3, u_4, u_5} K A ↥B')
  (hU :
    IsOpen
      (↑(basicOpen
              ((AlgHom.toRingHom
                    (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                      TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                  (a : A ⊗[K] ↥B') → A ⊗[K] B)
                f) :
            TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
        Set (PrimeSpectrum (A ⊗[K] B)))),
  IsOpen (X := PrimeSpectrum A)
    (comap (algebraMap A (A ⊗[K] B)) ''
      (↑(basicOpen
              ((AlgHom.toRingHom
                    (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                      TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                  (a : A ⊗[K] ↥B') → A ⊗[K] B)
                f) :
            TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
        Set (PrimeSpectrum (A ⊗[K] B))))
Tactic: obtain ⟨B', hB, f, rfl⟩ := exists_fg_and_mem_baseChange f
Cleared hypotheses: f, hU
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (hypothesis)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
⊢ IsOpen (X := PrimeSpectrum A)
    (comap (algebraMap A (A ⊗[K] B)) ''
      (↑(basicOpen
              ((AlgHom.toRingHom
                    (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                      TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                  (a : A ⊗[K] ↥B') → A ⊗[K] B)
                f) :
            TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
        Set (PrimeSpectrum (A ⊗[K] B))))
have this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
Tactic: have : Algebra.FinitePresentation K B' :=
    Algebra.FinitePresentation.of_finiteType.mp ⟨B'.fg_top.mpr hB⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
⊢ IsOpen (X := PrimeSpectrum A)
    (comap (algebraMap A (A ⊗[K] B)) ''
      (↑(basicOpen
              ((AlgHom.toRingHom
                    (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                      TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                  (a : A ⊗[K] ↥B') → A ⊗[K] B)
                f) :
            TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
        Set (PrimeSpectrum (A ⊗[K] B))))
have h : Eq (α := Set (PrimeSpectrum A))
  (comap (algebraMap A (A ⊗[K] B)) ''
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B))))
  (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) '' (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))
Tactic: convert!
    isOpenMap_comap_of_hasGoingDown_of_finitePresentation (R := A) (S := A ⊗[K] B') _
      (basicOpen f).isOpen using 1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
⊢ Eq (α := Set (PrimeSpectrum A))
    (comap (algebraMap A (A ⊗[K] B)) ''
      (↑(basicOpen
              ((AlgHom.toRingHom
                    (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                      TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                  (a : A ⊗[K] ↥B') → A ⊗[K] B)
                f) :
            TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
        Set (PrimeSpectrum (A ⊗[K] B))))
    (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) ''
      (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))
have h : ∀ (x : PrimeSpectrum A),
  Membership.mem (γ := Set (PrimeSpectrum A))
      (comap (algebraMap A (A ⊗[K] B)) ''
        (↑(basicOpen
                ((AlgHom.toRingHom
                      (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                        TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                    (a : A ⊗[K] ↥B') → A ⊗[K] B)
                  f) :
              TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
          Set (PrimeSpectrum (A ⊗[K] B))))
      x ↔
    Membership.mem (γ := Set (PrimeSpectrum A))
      (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) ''
        (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Chevalley (goal)
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
x : PrimeSpectrum A
⊢ Membership.mem (γ := Set (PrimeSpectrum A))
      (comap (algebraMap A (A ⊗[K] B)) ''
        (↑(basicOpen
                ((AlgHom.toRingHom
                      (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                        TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                    (a : A ⊗[K] ↥B') → A ⊗[K] B)
                  f) :
              TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
          Set (PrimeSpectrum (A ⊗[K] B))))
      x ↔
    Membership.mem (γ := Set (PrimeSpectrum A))
      (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) ''
        (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))
      x
have h : IsNilpotent (R := A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
    ((algebraMap (A ⊗[K] B) (A ⊗[K] B ⊗[A] x.asIdeal.ResidueField) :
          (a : A ⊗[K] B) → A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
        ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
            (a : A ⊗[K] ↥B') → A ⊗[K] B)
          f) :
      A ⊗[K] B ⊗[A] x.asIdeal.ResidueField) ↔
  IsNilpotent (R := TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField)
    ((algebraMap (TensorProduct.{u_3, u_4, u_5} K A ↥B')
            (TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField) :
          (a : A ⊗[K] ↥B') → A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField)
        f :
      TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField)
Tactic: rw [PrimeSpectrum.mem_image_comap_basicOpen, PrimeSpectrum.mem_image_comap_basicOpen,
    not_iff_not]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R₀ : Type u_1
R : Type u_2
inst : CommRing R₀
inst_1 : CommRing R
inst_2 : Algebra R₀ R
n : ℕ
e : InductionObj R n
⊢ LE.le (α := Submodule R₀ R) 1 (coeffSubmodule R₀ e)
have rw : 1 ∈ (↑(coeffSubmodule R₀ e) : Set R)
Tactic: rw [Submodule.one_eq_span, Submodule.span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
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 (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) : InductionObj R n } →
            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 :=
                HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                  ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                  ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
              InductionObj (Away c) n } →
          P (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))
              {
                val :=
                  (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                      (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                    e.val } →
            P R e
R : Type u
inst : CommRing R
e : InductionObj R n
⊢ P R e
have set : let v := e.degree;
∀ (hv : v = e.degree), P R e
Tactic: set v := e.degree with hv
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
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 (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) : InductionObj R n } →
            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 :=
                HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                  ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                  ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
              InductionObj (Away c) n } →
          P (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))
              {
                val :=
                  (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                      (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                    e.val } →
            P R e
R : Type u
inst : CommRing R
e : InductionObj R n
v : DegreeType n := e.degree
hv : v = e.degree
⊢ P R e
have clear_value : ∀ (v : DegreeType n) (hv : v = e.degree), P R e
Tactic: clear_value v
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
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 (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) : InductionObj R n } →
            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 :=
                HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                  ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                  ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
              InductionObj (Away c) n } →
          P (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))
              {
                val :=
                  (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                      (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                    e.val } →
            P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n) (hv : y = e.degree), P R e
R : Type u
inst : CommRing R
e : InductionObj R n
hv : v = e.degree
⊢ P R e
have pos : ∀ (he0 : e = { val := 0 }), P R e
Tactic: by_cases he0 : e = ⟨0⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
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 (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) : InductionObj R n } →
            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 :=
                HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                  ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                  ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
              InductionObj (Away c) n } →
          P (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))
              {
                val :=
                  (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                      (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                    e.val } →
            P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n) (hv : y = e.degree), P R e
R : Type u
inst : CommRing R
e : InductionObj R n
hv : v = e.degree
pos : ∀ (he0 : e = { val := 0 }), P R e
⊢ P R e
have neg : ∀ (he0 : ¬e = { val := 0 }), P R e
Tactic: by_cases he0 : e = ⟨0⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
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 (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) : InductionObj R n } →
            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 :=
                HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                  ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                  ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
              InductionObj (Away c) n } →
          P (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))
              {
                val :=
                  (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                      (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                    e.val } →
            P R e
v : DegreeType n
H_IH : ∀ y < v, ∀ {R : Type u} [inst : CommRing R] (e : InductionObj R n) (hv : y = e.degree), P R e
R : Type u
inst : CommRing R
e : InductionObj R n
hv : v = e.degree
he0 : ¬e = { val := 0 }
⊢ P R e
have neg : Subsingleton R → P R e
Tactic: cases subsingleton_or_nontrivial R