awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Etale.Weakly (goal)
Goal:
R : Type u₁
S : Type u₂
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u₃
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₂} S)
inst_8 : WeaklyEtale (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max u₁ u₂ u₃, u₃} T)
heq :
  Eq (α :=
    ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
        ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max (max u₁ u₂) u₃, u₁} R]
      ULift.{max u₁ u₂ u₃, u₃} T)
    (TensorProduct.lmul' (ULift.{max (max u₁ u₂) u₃, u₁} R))
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T))
⊢ RingHom.Flat (R := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T) (S :=
    ULift.{max u₁ u₂ u₃, u₃} T) (AlgHom.toRingHom (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₁} R)))
have rw : RingHom.Flat (R := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₁} R] ULift.{max u₁ u₂ u₃, u₃} T) (S :=
  ULift.{max u₁ u₂ u₃, u₃} T)
  (AlgHom.toRingHom (R := ULift.{max u₁ u₂ u₃, u₁} R)
    (AlgHom.comp (B := ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)
      (AlgHom.restrictScalars (ULift.{max u₁ u₂ u₃, u₁} R) (TensorProduct.lmul' (ULift.{max u₁ u₂ u₃, u₂} S)) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T)
      (TensorProduct.mapOfCompatibleSMul (ULift.{max u₁ u₂ u₃, u₂} S) (ULift.{max (max u₁ u₂) u₃, u₁} R)
          (ULift.{max u₁ u₂ u₃, u₁} R) (ULift.{max u₁ u₂ u₃, u₃} T) (ULift.{max u₁ u₂ u₃, u₃} T) :
        ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max (max u₁ u₂) u₃, u₁} R]
            ULift.{max u₁ u₂ u₃, u₃} T →ₐ[ULift.{max u₁ u₂ u₃, u₁} R]
          ULift.{max u₁ u₂ u₃, u₃} T ⊗[ULift.{max u₁ u₂ u₃, u₂} S] ULift.{max u₁ u₂ u₃, u₃} T)))
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I ↔ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
have mp : IsIdempotentElem I → ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
mp : IsIdempotentElem I → ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
⊢ IsIdempotentElem I ↔ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
have mpr : (∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e) → IsIdempotentElem I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I • I
have rw : I ≤ I * I
Tactic: rw [smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
have mp : ∀ (r : R) (hr : r ∈ I) (hr' : ∀ n ∈ I, r • n = n), ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
Tactic: obtain ⟨r, hr, hr'⟩ :=
      Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I I h
        (by
          rw [smul_eq_mul]
          exact e.ge)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
have mp : I ≤ R ∙ r
Tactic: refine ⟨r, hr' r hr, antisymm ?_ ((Submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ n ∈ I, r * n = n
x : R
hx : x ∈ I
⊢ Membership.mem (γ := Submodule R R) (R ∙ r) x
have mp : Membership.mem (γ := Submodule R R) (R ∙ r) (r * x)
Tactic: rw [← hr' x hx]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
have mp : IsIdempotentElem I → I = ⊥ ∨ I = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : I.FG
mp : IsIdempotentElem I → I = ⊥ ∨ I = ⊤
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
have mpr : I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
h : I.FG
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤
have mp : ∀ (e : R) (he : IsIdempotentElem e) (h : FG (R ∙ e)) (H : IsIdempotentElem (M := Ideal R) (R ∙ e)),
  Eq (α := Ideal R) (R ∙ e) ⊥ ∨ Eq (α := Ideal R) (R ∙ e) ⊤
Tactic: obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H
Cleared hypotheses: I, h, H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
H : IsIdempotentElem (M := Ideal R) (R ∙ e)
⊢ Eq (α := Ideal R) (R ∙ e) ⊥ ∨ Eq (α := Ideal R) (R ∙ e) ⊤
have mp : e = 0 ∨ Eq (α := Ideal R) (span {e}) ⊤
Tactic: simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.IdempotentFG (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
H : IsIdempotentElem (M := Ideal R) (R ∙ e)
⊢ e = 0 ∨ Eq (α := Ideal R) (span {e}) ⊤
have apply : e = 1 → Eq (α := Ideal R) (span {e}) ⊤
Tactic: apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ Eq.{u_1 + 1} (α := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical}
have h : ∀ (x : R),
  Membership.mem (γ := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) x ↔
    Membership.mem (γ := Set R) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
⊢ Membership.mem (γ := Set R) (⋃ p ∈ I.minimalPrimes, (↑p : Set R)) x ↔
    Membership.mem (γ := Set R) {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical} x
have h : (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical
Tactic: simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
⊢ (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical
have h : (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
h : (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical
⊢ (∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i) ↔ ∃ y ∉ I.radical, x * y ∈ I.radical
have h₁ : (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
⊢ LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
have rw : ∀ (b : Ideal (Localization.AtPrime p)),
  Membership.mem (γ := Set (Ideal (Localization.AtPrime p)))
      {J : Ideal (Localization.AtPrime p) |
        map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I ≤ J ∧ J.IsPrime}
      b →
    map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p ≤ b
Tactic: rw [Ideal.radical_eq_sInf, le_sInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
⊢ map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p ≤ q
have h₁ : IsPrime.{u_1} (α := R)
  (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
          (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
        (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
    Ideal R)
Tactic: obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
h₁ :
  IsPrime.{u_1} (α := R)
    (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R)
⊢ map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p ≤ q
have h₂ : (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
          (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
        (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
    Ideal R) ≤
  p
Tactic: obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
q : Ideal (Localization.AtPrime p)
hq' : map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I ≤ q
hq : q.IsPrime
h₁ :
  IsPrime.{u_1} (α := R)
    (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R)
h₂ :
  (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
            (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) → { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
          (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
      Ideal R) ≤
    p
⊢ map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p ≤ q
have rw : ∀ (hq' : I ≤ comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) q) (hq : q.IsPrime)
  (h₁ :
    IsPrime.{u_1} (α := R)
      (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
              (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) →
                { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
            (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
        Ideal R))
  (h₂ :
    (↑((IsLocalization.AtPrime.orderIsoOfPrime (Localization.AtPrime p) p :
              (a : { p_1 : Ideal (Localization.AtPrime p) // p_1.IsPrime }) →
                { p_1 : Ideal R // p_1.IsPrime ∧ p_1 ≤ p })
            (Subtype.mk (p := fun (p_1 : Ideal (Localization.AtPrime p)) ↦ p_1.IsPrime) q hq)) :
        Ideal R) ≤
      p),
  p ≤ comap (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) q
Tactic: rw [Ideal.map_le_iff_le_comap] at hq' ⊢
Cleared hypotheses: hq', hq, h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
have this : LE.le (α := Ideal (Localization.AtPrime p))
  (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
  (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
Tactic: have : p.map (algebraMap R (Localization.AtPrime p)) ≤ (I.map (algebraMap _ _)).radical := by
      rw [Ideal.radical_eq_sInf, le_sInf_iff]
      rintro q ⟨hq', hq⟩
      obtain ⟨h₁, h₂⟩ := ((IsLocalization.AtPrime.orderIsoOfPrime _ p) ⟨q, hq⟩).2
      rw [Ideal.map_le_iff_le_comap] at hq' ⊢
      exact hp₃ ⟨h₁, hq'⟩ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
have h : ∀ (n : ℕ)
  (hn :
    Membership.mem (γ := Ideal (Localization.AtPrime p))
      (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I)
      (HPow.hPow (α := Localization.AtPrime p)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)),
  ∃ y ∉ I.radical, x * y ∈ I.radical
Tactic: obtain ⟨n, hn⟩ := this (Ideal.mem_map_of_mem _ hxp)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
hn :
  Membership.mem (γ := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I)
    (HPow.hPow (α := Localization.AtPrime p)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
have hn₁ : ∃ (x_1 : ↥I × ↥p.primeCompl),
  HMul.hMul (β := Localization.AtPrime p)
      (HPow.hPow (α := Localization.AtPrime p)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x_1.2 : R) :
        Localization.AtPrime p) =
    (algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x_1.1 : R)
Tactic: rw [IsLocalization.mem_map_algebraMap_iff (M := p.primeCompl)] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
hn :
  ∃ (x_1 : ↥I × ↥p.primeCompl),
    HMul.hMul (β := Localization.AtPrime p)
        (HPow.hPow (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x_1.2 : R) :
          Localization.AtPrime p) =
      (algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑x_1.1 : R)
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
have h : ∀ (a : ↥I) (b : ↥p.primeCompl)
  (hn :
    HMul.hMul (β := Localization.AtPrime p)
        (HPow.hPow (α := Localization.AtPrime p)
          ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑(a, b).2 : R) :
          Localization.AtPrime p) =
      (algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑(a, b).1 : R)),
  ∃ y ∉ I.radical, x * y ∈ I.radical
Tactic: obtain ⟨⟨a, b⟩, hn⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b : ↥p.primeCompl
hn :
  HMul.hMul (β := Localization.AtPrime p)
      (HPow.hPow (α := Localization.AtPrime p)
        ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) x : Localization.AtPrime p) n)
      ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑(a, b).2 : R) :
        Localization.AtPrime p) =
    (algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (↑(a, b).1 : R)
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
have hn₁ : ∃ (c : ↥p.primeCompl), (↑c : R) * (x ^ n * (↑(a, b).2 : R)) = (↑c : R) * (↑(a, b).1 : R)
Tactic: rw [← map_pow, ← map_mul, IsLocalization.eq_iff_exists p.primeCompl] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b : ↥p.primeCompl
hn : ∃ (c : ↥p.primeCompl), (↑c : R) * (x ^ n * (↑(a, b).2 : R)) = (↑c : R) * (↑(a, b).1 : R)
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
have h : ∀ (t : ↥p.primeCompl) (ht : (↑t : R) * (x ^ n * (↑(a, b).2 : R)) = (↑t : R) * (↑(a, b).1 : R)),
  ∃ y ∉ I.radical, x * y ∈ I.radical
Tactic: obtain ⟨t, ht⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑(a, b).2 : R)) = (↑t : R) * (↑(a, b).1 : R)
⊢ ∃ y ∉ I.radical, x * y ∈ I.radical
have h : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) ∈ I
Tactic: refine ⟨t * b, fun h ↦ (t * b).2 (hp₁.radical_le_iff.mpr hp₂ h), n + 1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
⊢ (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R)
have rw : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * ((↑t : R) * (x ^ n * (↑b : R)))
Tactic: rw [mul_assoc, ← ht]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
⊢ (x * ((↑t : R) * (↑b : R))) ^ (n + 1) ∈ I
have this₁ : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R)
Tactic: have : (x * (t.1 * b.1)) ^ (n + 1) = (t.1 ^ n * b.1 ^ n * x * t.1) * a := by
      rw [mul_assoc, ← ht]; ring
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this_1 :
  LE.le (α := Ideal (Localization.AtPrime p))
    (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) p)
    (radical (map (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p)) I))
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : (↑t : R) * (x ^ n * (↑b : R)) = (↑t : R) * (↑a : R)
this : (x * ((↑t : R) * (↑b : R))) ^ (n + 1) = (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R)
⊢ (x * ((↑t : R) * (↑b : R))) ^ (n + 1) ∈ I
have h : (↑t : R) ^ n * (↑b : R) ^ n * x * (↑t : R) * (↑a : R) ∈ I
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y : R
hy : y ∉ I.radical
hx : x * y ∈ I.radical
⊢ ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i
have h : ∀ (p : Ideal R) (hp : p ∈ I.minimalPrimes) (hyp : y ∉ p), ∃ (i : Ideal R), I.IsMinimalPrime i ∧ x ∈ i
Tactic: obtain ⟨p, hp, hyp⟩ : ∃ p ∈ I.minimalPrimes, y ∉ p := by
      simpa [← Ideal.sInf_minimalPrimes] using hy