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)
⊢ LE.le (α := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
have a : LE.le (α := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
  (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
    (Ideal.map (R := ↥R[x]) (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
      (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)))
Tactic: rw [IsScalarTower.algebraMap_eq R R<x> S, ← Ideal.map_map]
-- 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)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
⊢ Eq (α := R →+* S) (algebraMap R S)
    (@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]))
have a : ∀ (x_1 : R),
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x_1 : S)
    ((@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]) : (a : R) → S)
        x_1 :
      S)
Tactic: ext
-- 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)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
⊢ 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)
        r :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
have this : Eq (α := R →+* S) (algebraMap R S)
  (@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]))
Tactic: have : algebraMap R S = (algebraMap R<x> S).comp (algebraMap R R<x>) := by ext; rfl
-- 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)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
this :
  Eq (α := R →+* S) (algebraMap R S)
    (@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]))
⊢ 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)
        r :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
have rw : Membership.mem (α := S) (γ := Ideal S)
  (Ideal.map (R := ↥R[x]) (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
  ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r : S)
Tactic: rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, this, ← Ideal.map_map]
-- 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)) ⋯
⊢ 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)
have refine_1 : Function.Injective (α :=
  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))
  (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
Tactic: refine RingEquiv.ofBijective f ⟨?_, ?_⟩
-- 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)) ⋯
refine_1 :
  Function.Injective (α :=
    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))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
⊢ 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)
have refine_2 : Function.Surjective (α :=
  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))
  (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
Tactic: refine RingEquiv.ofBijective f ⟨?_, ?_⟩
-- 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)) ⋯
⊢ Function.Injective (α :=
    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))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
have refine_1 : ∀ (u : ↥R[x])
  (hu :
    Membership.mem (γ := Submodule ↥R[x] ↥R[x])
      (ker (F := ↥R[x] →+* 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)))
      u),
  Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
Tactic: refine RingHom.lift_injective_of_ker_le_ideal _ _ fun u 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)) ⋯
u : ↥R[x]
hu :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (ker (F := ↥R[x] →+* 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)))
    u
⊢ Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
have refine_1 : ∀
  (hu :
    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)
          u :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))),
  Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
Tactic: rwa [RingHom.mem_ker, RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap,
      comap_map_eq_map_adjoin_of_coprime_conductor hx h_alg] at hu
Cleared hypotheses: 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)) ⋯
u : ↥R[x]
hu :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (ker (F := ↥R[x] →+* 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)))
    u
refine_1 :
  ∀
    (hu :
      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)
            u :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
        (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))),
    Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
⊢ Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
have refine_1₁ : ∀
  (hu :
    Eq (α := 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)
          ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) u) :
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))),
  Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
Tactic: rwa [RingHom.mem_ker, RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap,
      comap_map_eq_map_adjoin_of_coprime_conductor hx h_alg] at hu
Cleared hypotheses: 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)) ⋯
u : ↥R[x]
hu :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (ker (F := ↥R[x] →+* 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)))
    u
refine_1 :
  ∀
    (hu :
      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)
            u :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
        (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))),
    Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
refine_1₁ :
  ∀
    (hu :
      Eq (α := 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)
            ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) u) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
        (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))),
    Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
⊢ Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
have refine_1₂ : ∀
  (hu :
    Membership.mem (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
      ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) u : S)),
  Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
Tactic: rwa [RingHom.mem_ker, RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap,
      comap_map_eq_map_adjoin_of_coprime_conductor hx h_alg] at hu
Cleared hypotheses: 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)) ⋯
u : ↥R[x]
hu :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (ker (F := ↥R[x] →+* 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)))
    u
refine_1 :
  ∀
    (hu :
      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)
            u :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
        (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))),
    Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
refine_1₁ :
  ∀
    (hu :
      Eq (α := 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)
            ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) u) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
        (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))),
    Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
refine_1₂ :
  ∀
    (hu :
      Membership.mem (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
        ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) u : S)),
    Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
⊢ Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
have refine_1₃ : ∀
  (hu :
    Membership.mem (γ := Ideal ↥R[x])
      (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I)) u),
  Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
Tactic: rwa [RingHom.mem_ker, RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap,
      comap_map_eq_map_adjoin_of_coprime_conductor hx h_alg] at hu
Cleared hypotheses: 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)) ⋯
⊢ Function.Surjective (α :=
    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))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
have refine_2 : ∀ (y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)),
  ∃ (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: refine Ideal.Quotient.lift_surjective_of_surjective _ _ fun y => ?_
-- 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)
⊢ ∃ (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 : ∀ (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
Tactic: obtain ⟨z, hz⟩ := Ideal.Quotient.mk_surjective y
-- 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
⊢ Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) z
have suffices : Eq (α := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
Tactic: suffices conductor R x ⊔ I.map (algebraMap R S) = ⊤ by simp only [this, Submodule.mem_top]