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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
this :
  Membership.mem (γ := Set S)
      ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
        (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
      z ↔
    Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
a : ↥R[x]
ha :
  a ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]) ∧
    (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) a = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z
⊢ (algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
      (a +
        HMul.hMul (α := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z
have simp : HMul.hMul (α := S) (β := S)
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x]) : S)
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) :
      S) =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z
Tactic: simp only [ha.right, map_add, map_mul, add_right_inj]
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
this :
  Membership.mem (γ := Set S)
      ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
        (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
      z ↔
    Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
a : ↥R[x]
ha :
  a ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]) ∧
    (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) a = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z
⊢ a +
        HMul.hMul (α := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) ∈
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]) ∧
    (algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
        (a +
          HMul.hMul (α := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x])
            (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)) =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z
have h : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
  (HMul.hMul (α := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz))
Tactic: refine ⟨Ideal.add_mem (I.map (algebraMap R R<x>)) ha.left ?_, by
          simp only [ha.right, map_add, map_mul, add_right_inj]; 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
this :
  Membership.mem (γ := Set S)
      ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
        (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
      z ↔
    Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
a : ↥R[x]
ha :
  a ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]) ∧
    (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) a = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (HMul.hMul (α := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz))
have h : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
  (HMul.hMul (β := ↥R[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
    ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x]))
Tactic: rw [mul_comm]
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
⊢ Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
have a : Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z ↔
  Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
Tactic: suffices z ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>) ↔
        (⟨z, hz⟩ : R<x>) ∈ I.map (algebraMap R R<x>) by
      rw [← this, ← temp]
      obtain ⟨a, ha⟩ := (Set.mem_image _ _ _).mp (prod_mem_ideal_map_of_mem_conductor hp
          (show z ∈ I.map (algebraMap R S) by rwa [Ideal.mem_comap] at hy))
      use a + algebraMap R R<x> q * ⟨z, hz⟩
      refine ⟨Ideal.add_mem (I.map (algebraMap R R<x>)) ha.left ?_, by
          simp only [ha.right, map_add, map_mul, add_right_inj]; rfl⟩
      rw [mul_comm]
      exact Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ hq)
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
⊢ Membership.mem (γ := Set S)
      ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
        (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
      z ↔
    Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
have a : ∀
  (h :
    Membership.mem (γ := Set S)
      ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
        (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
      z),
  Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
Tactic: refine ⟨fun h => ?_,
      fun h => (Set.mem_image _ _ _).mpr (Exists.intro ⟨z, hz⟩ ⟨by simp [h], 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
have a : ∀ (x₁ : ↥R[x]) (hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
  (hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z),
  Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
Tactic: obtain ⟨x₁, hx₁, hx₂⟩ := (Set.mem_image _ _ _).mp h
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
⊢ x₁ = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz
have a : Eq (α := S) ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ : S)
  ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) :
    S)
Tactic: apply h_alg
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
⊢ Eq (α := S) ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ : S)
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) :
      S)
have a : z = HSMul.hSMul (β := S) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) 1
Tactic: simp only [hx₂, algebraMap_eq_smul_one]
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
⊢ z = HSMul.hSMul (β := S) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) 1
have a : z = HSMul.hSMul (β := S) z 1
Tactic: rw [Submonoid.mk_smul, smul_eq_mul, mul_one]
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
a : z = HSMul.hSMul (β := S) z 1
⊢ z = HSMul.hSMul (β := S) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) 1
have a₁ : z = z * 1
Tactic: rw [Submonoid.mk_smul, smul_eq_mul, mul_one]
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
a : z = HSMul.hSMul (β := S) z 1
a₁ : z = z * 1
⊢ z = HSMul.hSMul (β := S) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) 1
have a₂ : z = z
Tactic: rw [Submonoid.mk_smul, smul_eq_mul, mul_one]
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
have this : x₁ = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz
Tactic: have : x₁ = ⟨z, hz⟩ := by
      apply h_alg
      simp only [hx₂, algebraMap_eq_smul_one]
      rw [Submonoid.mk_smul, smul_eq_mul, mul_one]
-- 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)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
this : x₁ = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
have a : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) x₁
Tactic: rwa [← this]