awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :=
  map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
this_1 :
  Set.SurjOn (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p)
    (↑P : Set S) (↑s' : Set (S ⧸ map (algebraMap R S) p))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
this :
  Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))
⊢ Membership.mem (γ := Set (Ideal S)) (Ideal.minimalPrimes (span (↑t : Set S))) P
have refine : Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
  (Ideal.minimalPrimes
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) (span (↑o : Set S))))
  (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
Tactic: refine this ▸ map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes hp (span_le.mpr ho) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
s : Finset R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p
heq : (↑s.card : ℕ∞) = p.height
P' : Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) :=
  map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P
s' : Finset (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
hP' :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))) P'
heq' : (↑s'.card : ℕ∞) = P'.height
hsP'sub : (↑s' : Set (S ⧸ map (algebraMap R S) p)) ⊆ (↑P' : Set (S ⧸ map (algebraMap R S) p))
this_1 :
  Set.SurjOn (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p)
    (↑P : Set S) (↑s' : Set (S ⧸ map (algebraMap R S) p))
o : Finset S
ho : (↑o : Set S) ⊆ (↑P : Set S)
hinj :
  Set.InjOn (β := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
    (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) (↑o : Set S)
himgo :
  Finset.image (⇑(Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ map (algebraMap R S) p) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S) : (a : R) → S) s ∪ o
this :
  Eq (α := Ideal S) (span (↑t : Set S)) (map (F := R →+* S) (algebraMap R S) (span (↑s : Set R)) ⊔ span (↑o : Set S))
⊢ Membership.mem (γ := Set (Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
    (Ideal.minimalPrimes
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) (span (↑o : Set S))))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
have h : Eq.{u_2 + 1} (α := CommSemiring (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    (Quotient.commSemiring (map (F := R →+* S) (algebraMap R S) p)) CommRing.toCommSemiring →
  Eq (α := Ideal (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
    (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) (span (↑o : Set S)))
    (span (↑s' : Set (S ⧸ map (algebraMap R S) p)))
Tactic: convert! hP'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
p : Ideal R
inst_5 : p.IsPrime
P : Ideal S
inst_6 : P.IsPrime
inst_7 : P.LiesOver p
⊢ P.height ≤
    p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
have obtain : ∀ (s : Finset R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (↑s : Set R))) p)
  (heq : (↑s.card : ℕ∞) = p.height),
  P.height ≤
    p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
Tactic: classical
  obtain ⟨s, hp, heq⟩ := p.exists_finset_card_eq_height_of_isNoetherianRing
  let P' := P.map (Ideal.Quotient.mk <| p.map (algebraMap R S))
  obtain ⟨s', hP', heq'⟩ := P'.exists_finset_card_eq_height_of_isNoetherianRing
  have hsP'sub : (s' : Set <| S ⧸ (Ideal.map (algebraMap R S) p)) ⊆ (P' : Set <| S ⧸ _) :=
    fun x hx ↦ hP'.le (Ideal.subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk (p.map (algebraMap R S))) P s' := by
    refine Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_
    obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective x
    rw [SetLike.mem_coe, Ideal.mem_quotient_iff_mem] at hx
    · use y, hx
    · rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]
  obtain ⟨o, ho, hinj, himgo⟩ := s'.exists_subset_injOn_image_eq_of_surjOn (P : Set S) this
  let t : Finset S := Finset.image (algebraMap R S) s ∪ o
  suffices h : P.height ≤ t.card by
    rw [← heq, ← heq']
    apply le_trans h
    norm_cast
    refine le_trans (Finset.card_union_le _ _) (add_le_add Finset.card_image_le ?_)
    rw [← himgo, Finset.card_image_of_injOn hinj]
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  have : Ideal.span t = Ideal.map (algebraMap R S) (.span s) ⊔ .span o := by
    simp [t, Ideal.map_span]
  refine this ▸ map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes hp (span_le.mpr ho) ?_
  convert! hP'
  simp [Ideal.map_span, ← himgo]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
⊢ P.height =
    p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
have refine : p.height +
    height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P) ≤
  P.height
Tactic: refine le_antisymm (height_le_height_add_of_liesOver p P) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
⊢ p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P) ≤
    P.height
have obtain : ∀ (lp : LTSeries (PrimeSpectrum R))
  (hlp :
    RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        lp =
      { asIdeal := p, isPrime := sorry })
  (hlenp :
    (↑(lp.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) =
      p.height),
  p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P) ≤
    P.height
Tactic: obtain ⟨lp, hlp, hlenp⟩ := p.exists_ltSeries_length_eq_height
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      lp =
    { asIdeal := p, isPrime := ⋯ }
hlenp :
  (↑(lp.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    p.height
lq : LTSeries (PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
hlq :
  RelSeries.last (r :=
      {x :
        PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
        match (motive :=
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
            Prop)
          x with
        | (a, b) => a < b})
      lq =
    {
      asIdeal :=
        map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P,
      isPrime := ⋯ }
hlenq :
  (↑(lq.length (r :=
          {x :
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
            match (motive :=
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                  PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
                Prop)
              x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (F := R →+* S) (algebraMap R S) p))) ⋯
| p
have rw : comap (F := R →+* S) (algebraMap R S) P
Tactic: rw [LiesOver.over (p := p) (P := P), under_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Lattice (goal)
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b a_1 x : α
h : Membership.mem (γ := Ideal α) ⊥ a_1
⊢ Membership.mem (γ := Ideal α) ⊥ (a_1 * x)
have rw : Membership.mem (γ := Ideal α) ⊥ 0
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Lattice (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hx : x ∈ I
h : y * x = 1
z : α
h_1 : Membership.mem (γ := Submodule α α) ⊤ z
⊢ z * (y * x) = z
have rw : z * 1 = z
Tactic: rw [h, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Lattice (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hx : x ∈ I
h : y * x = 1
z : α
h_1 : Membership.mem (γ := Submodule α α) ⊤ z
rw : z * 1 = z
⊢ z * (y * x) = z
have rw₁ : z = z
Tactic: rw [h, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Lattice (goal)
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
⊢ I = ⊥ ∨ I = ⊤
have rw : ¬I = ⊤ → I = ⊥
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Lattice (goal)
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
⊢ I ≠ ⊤ → I = ⊥
have rw : 1 ∉ I → I = ⊥
Tactic: rw [Ideal.ne_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Lattice (goal)
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
⊢ I = ⊥
have rw : I ≤ ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Lattice (goal)
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
⊢ Membership.mem (γ := Submodule K K) ⊥ r
have pos : ∀ (H : r = 0), Membership.mem (γ := Submodule K K) ⊥ r
Tactic: by_cases H : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Lattice (goal)
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
pos : ∀ (H : r = 0), Membership.mem (γ := Submodule K K) ⊥ r
⊢ Membership.mem (γ := Submodule K K) ⊥ r
have neg : ∀ (H : ¬r = 0), Membership.mem (γ := Submodule K K) ⊥ r
Tactic: by_cases H : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
x y : R
hx : Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) x
hy : Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) y
⊢ Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) (x + y)
have simp : ∀ (hx : Membership.mem (α := S) I ((f : (a : R) → S) x : S)) (hy : Membership.mem (α := S) I ((f : (a : R) → S) y : S)),
  HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ∈ I
Tactic: simp only [Set.mem_preimage, SetLike.mem_coe, map_add f] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
c x : R
hx : Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) x
⊢ Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) (c • x)
have simp : ∀ (hx : Membership.mem (α := S) I ((f : (a : R) → S) x : S)),
  HMul.hMul (α := S) (β := S) ((f : (a : R) → S) c : S) ((f : (a : R) → S) x : S) ∈ I
Tactic: simp only [smul_eq_mul, Set.mem_preimage, map_mul, SetLike.mem_coe] at *
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
K : Ideal S
inst_3 : RingHomClass F R S
hK : K ≠ ⊤
⊢ 1 ∉ comap f K
have rw : 1 ∉ K
Tactic: rw [mem_comap, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn.{u, v} (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S) (↑I : Set R)
⊢ LE.le (α := Ideal S) (map f I) (comap g I)
have refine : (⇑f : (a : R) → S) '' (↑I : Set R) ⊆ (↑(comap g I) : Set S)
Tactic: refine Ideal.span_le.2 ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn.{u, v} (β := S) (⇑g : (a : S) → R) (⇑f : (a : R) → S) (↑I : Set R)
x : R
hx : x ∈ (↑I : Set R)
⊢ Membership.mem (α := S) (↑(comap g I) : Set S) ((f : (a : R) → S) x : S)
have rw : x ∈ I
Tactic: rw [SetLike.mem_coe, mem_comap, hf hx]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
h : Eq (α := Ideal R) (comap f I) ⊥
⊢ I = ⊥
have h₁ : ∀ (x : S), x ∈ I ↔ Membership.mem (γ := Ideal S) ⊥ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
h : Eq (α := Ideal R) (comap f I) ⊥
x : S
⊢ x ∈ I ↔ Membership.mem (γ := Ideal S) ⊥ x
have h₁ : ∀ (y : R) (hy : (f : (a : R) → S) y = x), x ∈ I ↔ Membership.mem (γ := Ideal S) ⊥ x
Tactic: obtain ⟨y, hy⟩ := hf x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
inst_5 : K.IsTwoSided
a b : R
ha : Membership.mem (γ := Ideal R) (comap f K) a
⊢ Membership.mem (γ := Ideal R) (comap f K) (a * b)
have rw : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈ K
Tactic: rw [mem_comap, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
hK : K.IsPrime
x y : R
⊢ Membership.mem (γ := Ideal R) (Ideal.comap f K) (x * y) →
    Membership.mem (γ := Ideal R) (Ideal.comap f K) x ∨ Membership.mem (γ := Ideal R) (Ideal.comap f K) y
have simp : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ∈ K →
  Membership.mem (α := S) K ((f : (a : R) → S) x : S) ∨ Membership.mem (α := S) K ((f : (a : R) → S) y : S)
Tactic: simp only [mem_comap, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
⊢ Eq.{v + 1} (α := Ideal S) (map f (span s)) (span ((⇑f : (a : R) → S) '' s))
have refine_1 : (⇑f : (a : R) → S) '' s ⊆ (↑(map f (span s)) : Set S)
Tactic: refine (Submodule.span_eq_of_le _ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
refine_1 : (⇑f : (a : R) → S) '' s ⊆ (↑(map f (span s)) : Set S)
⊢ Eq.{v + 1} (α := Ideal S) (map f (span s)) (span ((⇑f : (a : R) → S) '' s))
have refine_2 : LE.le (α := Submodule S S) (map f (span s)) (Submodule.span S ((⇑f : (a : R) → S) '' s))
Tactic: refine (Submodule.span_eq_of_le _ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set R
⊢ LE.le (α := Submodule S S) (map f (span s)) (Submodule.span S ((⇑f : (a : R) → S) '' s))
have refine_2 : (⇑f : (a : R) → S) '' s ⊆ (↑(Submodule.span S ((⇑f : (a : R) → S) '' s)) : Set S)
Tactic: rw [map_le_iff_le_comap, span_le, coe_comap, ← Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
I : Ideal S
h : I = ⊤
⊢ Eq (α := Ideal R) (comap f I) ⊤
have rw : Eq (α := Ideal R) (comap f ⊤) ⊤
Tactic: rw [h, comap_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
I : Ideal S
h : I = ⊤
rw : Eq (α := Ideal R) (comap f ⊤) ⊤
⊢ Eq (α := Ideal R) (comap f I) ⊤
have rw₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [h, comap_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
s : Set (Ideal S)
⊢ Eq.{u + 1} (α := Ideal R) (⨅ I ∈ s, comap f I)
    (⨅ (I : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (comap f '' s) I), I)
have rw : Eq.{u + 1} (α := Ideal R) (⨅ I ∈ s, comap f I) (⨅ b ∈ s, comap f b)
Tactic: rw [iInf_image]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_4
S : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (HSMul.hSMul.{u_5, u_6, u_6} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) I) N) =
    HSMul.hSMul (β := Submodule R M) I (Submodule.restrictScalars R N)
have simp_rw : Eq.{u_6 + 1} (α := Submodule R M)
  (Submodule.restrictScalars.{u_4, u_5, u_6} R (R := S)
    (⨆ b ∈ (↑I : Set R), HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) b : S) N))
  (⨆ a ∈ (↑I : Set R),
    Submodule.restrictScalars R (HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) a : S) N))
Tactic: simp_rw [map, Submodule.span_smul_eq, ← Submodule.coe_set_smul,
    Submodule.set_smul_eq_iSup, ← element_smul_restrictScalars, iSup_image]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
a b : S
ha : Membership.mem (γ := Ideal S) (map f I) a
⊢ Membership.mem (γ := Ideal S) (map f I) (a * b)
have rw : ∀ (ha : a ∈ Submodule.map f.toSemilinearMap I), a * b ∈ Submodule.map f.toSemilinearMap I
Tactic: rw [map_eq_submodule_map] at ha ⊢
Cleared hypotheses: ha