awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
⊢ Eq (α := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
have rw : ∀ (hx : 1 ∈ comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I)
  (h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S))
  (y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) (z : S)
  (hz :
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z =
      y),
  Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) 1
Tactic: rw [Ideal.eq_top_iff_one] at hx ⊢
Cleared hypotheses: hx, h_alg, f, y, z, hz
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : 1 ∈ comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
⊢ Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) 1
have hx₁ : Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S)
  (Ideal.map (F := R →+* S) (algebraMap R S) (comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I))
  ((algebraMap R S : (a : R) → S) 1 : S)
Tactic: replace hx := Ideal.mem_map_of_mem (algebraMap R S) hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
hx :
  Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S) (comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I))
    ((algebraMap R S : (a : R) → S) 1 : S)
⊢ Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) 1
have hx₁ : Membership.mem (γ := Ideal S)
  (Ideal.map (F := R →+* S) (algebraMap R S) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) ⊔
    Ideal.map (F := R →+* S) (algebraMap R S) I)
  1
Tactic: rw [Ideal.map_sup, map_one] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
⊢ ∃ (a : ↥R[x]),
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        a =
      y
have this : Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) z
Tactic: have : z ∈ conductor R x ⊔ I.map (algebraMap R S) := by
      suffices conductor R x ⊔ I.map (algebraMap R S) = ⊤ by simp only [this, Submodule.mem_top]
      rw [Ideal.eq_top_iff_one] at hx ⊢
      replace hx := Ideal.mem_map_of_mem (algebraMap R S) hx
      rw [Ideal.map_sup, map_one] at hx
      exact (sup_le_sup
        (show ((conductor R x).comap (algebraMap R S)).map (algebraMap R S) ≤ conductor R x
          from Ideal.map_comap_le)
          (le_refl (I.map (algebraMap R S)))) hx
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
this : Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) z
⊢ ∃ (a : ↥R[x]),
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        a =
      y
have refine_2 : ∀
  (this :
    ∃ (x_1 : S),
      Membership.mem (γ := Ideal S) (conductor R x) x_1 ∧
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
            x_1 =
          y),
  ∃ (a : ↥R[x]),
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        a =
      y
Tactic: rw [← Ideal.mem_quotient_iff_mem_sup, hz, Ideal.mem_map_iff_of_surjective] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
this : Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) z
refine_2 :
  ∀
    (this :
      ∃ (x_1 : S),
        Membership.mem (γ := Ideal S) (conductor R x) x_1 ∧
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
              x_1 =
            y),
    ∃ (a : ↥R[x]),
      (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
            (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
          a =
        y
⊢ ∃ (a : ↥R[x]),
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        a =
      y
have refine_2₁ : ∀
  (this :
    Membership.mem (γ := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))
      (Ideal.map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (conductor R x))
      y),
  Function.Surjective.{u_2 + 1, u_2 + 1} (α := S) (β :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
Tactic: rw [← Ideal.mem_quotient_iff_mem_sup, hz, Ideal.mem_map_iff_of_surjective] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
this :
  ∃ (x_1 : S),
    Membership.mem (γ := Ideal S) (conductor R x) x_1 ∧
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          x_1 =
        y
⊢ ∃ (a : ↥R[x]),
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        a =
      y
have refine_2 : ∀ (u : S) (hu : Membership.mem (γ := Ideal S) (conductor R x) u)
  (hu' :
    (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u =
      y),
  ∃ (a : ↥R[x]),
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        a =
      y
Tactic: obtain ⟨u, hu, hu'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
u : S
hu : Membership.mem (γ := Ideal S) (conductor R x) u
hu' :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u = y
⊢ ∃ (a : ↥R[x]),
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        a =
      y
have h : (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
      (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) u sorry) =
  y
Tactic: use ⟨u, conductor_subset_adjoin hu⟩
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
u : S
hu : Membership.mem (γ := Ideal S) (conductor R x) u
hu' :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u = y
⊢ (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
        (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) u ⋯) =
    y
have h : Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
  ((RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
        (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) u sorry) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
  ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
Tactic: simp only [← hu']
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
P : Ideal S
inst_3 : P.IsPrime
hx : ¬conductor R x ≤ P
s : Subalgebra R S
hs : s = R[x]
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
⊢ Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
have obtain : ∀ (a : S) (ha : Membership.mem (γ := Ideal S) (conductor R x) a) (haP : a ∉ P),
  Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) sorry) : (a : Localization.AtPrime p) → Localization.AtPrime P)
Tactic: obtain ⟨a, ha, haP⟩ := SetLike.not_le_iff_exists.mp hx
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
P : Ideal S
inst_3 : P.IsPrime
hx : ¬conductor R x ≤ P
s : Subalgebra R S
hs : s = R[x]
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
ha : Membership.mem (γ := Ideal S) (conductor R x) a
haP : a ∉ P
⊢ Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
have ha₁ : ∀ (b : S), a * b ∈ s
Tactic: replace ha (b : _) : a * b ∈ s := by simpa [hs] using ha b
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x y : R
h : ((sInf S).toSetoid : R → R → Prop) x y
r : Setoid R
h_1 : Membership.mem (γ := Set (Setoid R)) ((fun (x : RingCon R) ↦ x.toSetoid) '' S) r
c : RingCon R
hS : c ∈ S
hr : (fun (x : RingCon R) ↦ x.toSetoid) c = r
⊢ (r : R → R → Prop) x y
have rw : ((fun (x : RingCon R) ↦ x.toSetoid) c : R → R → Prop) x y
Tactic: rw [← hr]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
⊢ Eq (α := (a : R) → R → Prop) (⇑(sInf S) : (a : R) → R → Prop) (sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' S))
have h : ∀ (x x_1 : R), (sInf S : (a : R) → R → Prop) x x_1 ↔ sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' S) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x x_1 : R
⊢ (sInf S : (a : R) → R → Prop) x x_1 ↔ sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' S) x x_1
have h : (sInf S : (a : R) → R → Prop) x x_1 ↔ ∀ (i : RingCon R) (i_1 : i ∈ S), (i : (a : R) → R → Prop) x x_1
Tactic: simp only [sInf_image, iInf_apply, iInf_Prop_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
ι : Sort u_4
f : ι → RingCon R
⊢ Eq (α := (a : R) → R → Prop) (⇑(iInf f) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
have rw : Eq (α := (a : R) → R → Prop) (⇑(sInf (Set.range f)) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
ι : Sort u_4
f : ι → RingCon R
rw :
  Eq (α := (a : R) → R → Prop) (⇑(sInf (Set.range f)) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
⊢ Eq (α := (a : R) → R → Prop) (⇑(iInf f) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
have rw₁ : Eq (α := (a : R) → R → Prop) (sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' Set.range f))
  (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
ι : Sort u_4
f : ι → RingCon R
rw :
  Eq (α := (a : R) → R → Prop) (⇑(sInf (Set.range f)) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₁ :
  Eq (α := (a : R) → R → Prop) (sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' Set.range f))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
⊢ Eq (α := (a : R) → R → Prop) (⇑(iInf f) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
have rw₂ : Eq (α := (a : R) → R → Prop) (sInf (Set.range (DFunLike.coe (β := fun (x : R) ↦ R → Prop) ∘ f)))
  (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
ι : Sort u_4
f : ι → RingCon R
rw :
  Eq (α := (a : R) → R → Prop) (⇑(sInf (Set.range f)) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₁ :
  Eq (α := (a : R) → R → Prop) (sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' Set.range f))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₂ :
  Eq (α := (a : R) → R → Prop) (sInf (Set.range (DFunLike.coe (β := fun (x : R) ↦ R → Prop) ∘ f)))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
⊢ Eq (α := (a : R) → R → Prop) (⇑(iInf f) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
have rw₃ : Eq (α := (a : R) → R → Prop) (iInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) ∘ f))
  (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
ι : Sort u_4
f : ι → RingCon R
rw :
  Eq (α := (a : R) → R → Prop) (⇑(sInf (Set.range f)) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₁ :
  Eq (α := (a : R) → R → Prop) (sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' Set.range f))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₂ :
  Eq (α := (a : R) → R → Prop) (sInf (Set.range (DFunLike.coe (β := fun (x : R) ↦ R → Prop) ∘ f)))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₃ :
  Eq (α := (a : R) → R → Prop) (iInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) ∘ f))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
⊢ Eq (α := (a : R) → R → Prop) (⇑(iInf f) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
have rw₄ : Eq.{u_3 + 1} (α := (a : R) → R → Prop) (⨅ (x : ι), (⇑(f x) : (a : R) → R → Prop))
  (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
Tactic: rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ c.toCon = ⊤ ↔ c = ⊤
have rw : c.toCon = toCon ⊤ ↔ c = ⊤
Tactic: rw [← toCon_top, toCon_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
rw : c.toCon = toCon ⊤ ↔ c = ⊤
⊢ c.toCon = ⊤ ↔ c = ⊤
have rw₁ : c = ⊤ ↔ c = ⊤
Tactic: rw [← toCon_top, toCon_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ c.toCon = ⊥ ↔ c = ⊥
have rw : c.toCon = toCon ⊥ ↔ c = ⊥
Tactic: rw [← toCon_bot, toCon_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
rw : c.toCon = toCon ⊥ ↔ c = ⊥
⊢ c.toCon = ⊥ ↔ c = ⊥
have rw₁ : c = ⊥ ↔ c = ⊥
Tactic: rw [← toCon_bot, toCon_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Congruence.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Add R
inst_1 : Mul R
c_1 d : RingCon R
inst_2 : Subsingleton R
c c' : RingCon R
r r' : R
⊢ (c : (a : R) → R → Prop) r r' ↔ (c' : (a : R) → R → Prop) r r'
have simp_rw : (c : (a : R) → R → Prop) r r ↔ (c' : (a : R) → R → Prop) r r
Tactic: simp_rw [Subsingleton.elim r' r, c.refl, c'.refl]