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
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
h : Nontrivial L
H :
  ∀ (z : S),
    ∃ (x_1 : S),
      Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
        (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L)
⊢ ∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y
have mpr : ∀ (y_1 : S),
  Membership.mem (γ := Subalgebra R S) R[x] y_1 →
    ∀ (e : (algebraMap S L : (a : S) → L) y_1 = HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) 1 : L)),
      ∃ (y_2 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_2 ∧ (algebraMap S L : (a : S) → L) y_2 = y
Tactic: obtain ⟨y, _, e⟩ := H 1
-- 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
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y_1 : L
h : Nontrivial L
H :
  ∀ (z : S),
    ∃ (x_1 : S),
      Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
        (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y_1 ((algebraMap S L : (a : S) → L) z : L)
y : S
left : Membership.mem (γ := Subalgebra R S) R[x] y
e : (algebraMap S L : (a : S) → L) y = HMul.hMul (β := L) y_1 ((algebraMap S L : (a : S) → L) 1 : L)
⊢ ∃ (y : S), Membership.mem (γ := Submodule S S) (conductor R x) y ∧ (algebraMap S L : (a : S) → L) y = y_1
have e₁ : (algebraMap S L : (a : S) → L) y = y_1
Tactic: rw [map_one, mul_one] at e
Cleared hypotheses: e
-- 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
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y_1 : L
h : Nontrivial L
H :
  ∀ (z : S),
    ∃ (x_1 : S),
      Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
        (algebraMap S L : (a : S) → L) x_1 = HMul.hMul (β := L) y_1 ((algebraMap S L : (a : S) → L) z : L)
y : S
left : Membership.mem (γ := Subalgebra R S) R[x] y
e : (algebraMap S L : (a : S) → L) y = y_1
⊢ ∃ (y : S), Membership.mem (γ := Submodule S S) (conductor R x) y ∧ (algebraMap S L : (a : S) → L) y = y_1
have mpr : ∀
  (H :
    ∀ (z : S),
      ∃ (x_1 : S),
        Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
          (algebraMap S L : (a : S) → L) x_1 =
            HMul.hMul (α := L) (β := L) ((algebraMap S L : (a : S) → L) y : L) ((algebraMap S L : (a : S) → L) z : L)),
  ∃ (y_2 : S),
    Membership.mem (γ := Submodule S S) (conductor R x) y_2 ∧
      Eq.{u_3 + 1} (α := L) ((algebraMap S L : (a : S) → L) y_2 : L) ((algebraMap S L : (a : S) → L) y : L)
Tactic: subst e
Cleared hypotheses: y_1, H, e
-- 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
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
h : Nontrivial L
y : S
left : Membership.mem (γ := Subalgebra R S) R[x] y
H :
  ∀ (z : S),
    ∃ (x_1 : S),
      Membership.mem (γ := Subalgebra R S) R[x] x_1 ∧
        (algebraMap S L : (a : S) → L) x_1 =
          HMul.hMul (α := L) (β := L) ((algebraMap S L : (a : S) → L) y : L) ((algebraMap S L : (a : S) → L) z : L)
⊢ ∃ (y_1 : S),
    Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧
      Eq.{u_3 + 1} (α := L) ((algebraMap S L : (a : S) → L) y_1 : L) ((algebraMap S L : (a : S) → L) y : L)
have H₁ : ∀ (z : S), Membership.mem (γ := Subalgebra R S) R[x] (y * z)
Tactic: simp only [← map_mul, (FaithfulSMul.algebraMap_injective S L).eq_iff,
        exists_eq_right] at H
Cleared hypotheses: 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
L : Type u_3
inst_3 : CommRing L
inst_4 : Algebra S L
inst_5 : Algebra R L
inst_6 : IsScalarTower R S L
inst_7 : IsDomain S
inst_8 : IsTorsionFree S L
x : S
y : L
h : Nontrivial L
⊢ (∀ (z : S),
      Membership.mem (γ := Subalgebra R L) (Subalgebra.map (IsScalarTower.toAlgHom R S L) R[x])
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))) ↔
    ∀ (z : S),
      Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
have rw : (∀ (z : S),
    Membership.mem (γ := Subalgebra R L) R[((IsScalarTower.toAlgHom R S L : (a : S) → L) x : L)]
      (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))) ↔
  ∀ (z : S),
    Membership.mem (γ := Subalgebra R L) R[((algebraMap S L : (a : S) → L) x : L)]
      (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
Tactic: rw [AlgHom.map_adjoin, Set.image_singleton]
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
hz' : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) 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]))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z)
have hz'₁ : ∃ (l : R →₀ S),
  Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l ∧
    (Finsupp.linearCombination S (⇑(algebraMap R S) : (a : R) → S) : (a : R →₀ S) → S) l = z
Tactic: rw [Ideal.map, Ideal.span, Finsupp.mem_span_image_iff_linearCombination] at hz'
Cleared hypotheses: hz'
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
hz' :
  ∃ (l : R →₀ S),
    Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l ∧
      (Finsupp.linearCombination S (⇑(algebraMap R S) : (a : R) → S) : (a : R →₀ S) → S) l = 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]))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z)
have obtain : ∀ (l : R →₀ S) (H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l)
  (H' : (Finsupp.linearCombination S (⇑(algebraMap R S) : (a : R) → S) : (a : R →₀ S) → S) l = 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]))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z)
Tactic: obtain ⟨l, H, H'⟩ := hz'
Cleared hypotheses: 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (Finsupp.linearCombination S (⇑(algebraMap R S) : (a : R) → S) : (a : R →₀ S) → S) l = 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]))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z)
have H'₁ : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
Tactic: rw [Finsupp.linearCombination_apply] at H'
Cleared hypotheses: 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = 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]))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z)
have rw : 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]))
  (l.sum fun (a : R) (c : S) ↦
    HMul.hMul (β := S) (HSMul.hSMul (β := S) c ((algebraMap R S : (a : R) → S) a : S))
      ((algebraMap R S : (a : R) → S) p : S))
Tactic: rw [← H', mul_comm, Finsupp.sum_mul]
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
a : R
ha : a ∈ I
⊢ 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]))
    (HMul.hMul (β := S) (HSMul.hSMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) a : S))
      ((algebraMap R S : (a : R) → S) p : S))
have rw : ∃ x_1 ∈ (↑(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) x_1 =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
Tactic: rw [smul_eq_mul, mul_assoc, mul_comm, mul_assoc, Set.mem_image]
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
a : R
ha : a ∈ I
⊢ ∃ x_1 ∈ (↑(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) x_1 =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
have refine : HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) sorry) ∈
    (↑(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)
      (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) sorry)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
Tactic: refine Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
a : R
ha : a ∈ I
refine :
  HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) ∈
      (↑(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)
        (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
⊢ ∃ x_1 ∈ (↑(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) x_1 =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
have refine₁ : Membership.mem (γ := Subalgebra R S) R[x]
  (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S))
Tactic: refine Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
a : R
ha : a ∈ I
⊢ Membership.mem (γ := Subalgebra R S) R[x]
    (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S))
have rw : Membership.mem (γ := Subalgebra R S) R[x]
  (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
a : R
ha : a ∈ I
⊢ HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) ∈
      (↑(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)
        (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
have refine_1 : HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
      (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) sorry) ∈
  (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
Tactic: refine ⟨?_, ?_⟩
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
a : R
ha : a ∈ I
refine_1 :
  HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) ∈
    (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
⊢ HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) ∈
      (↑(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)
        (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
have refine_2 : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
    (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) sorry)) =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
Tactic: refine ⟨?_, ?_⟩
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
a : R
ha : a ∈ I
⊢ HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) ∈
    (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
have refine_1 : HMul.hMul (α := ↥R[x]) (β := ↥R[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
      (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) sorry)
    ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x]) ∈
  (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
a : R
ha : a ∈ I
⊢ (algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
      (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
have refine_2 : HMul.hMul (α := S) (β := S)
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥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)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) sorry) :
      S) =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
    (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S))
Tactic: simp only [map_mul, mul_comm (algebraMap R S p) (l a)]
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = 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]))
    (l.sum fun (a : R) (c : S) ↦
      HMul.hMul (β := S) (HSMul.hSMul (β := S) c ((algebraMap R S : (a : R) → S) a : S))
        ((algebraMap R S : (a : R) → S) p : S))
have lem : ∀ {a : R},
  a ∈ I →
    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]))
      (HMul.hMul (β := S)
        (HSMul.hSMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) a : S))
        ((algebraMap R S : (a : R) → S) p : S))
Tactic: have lem : ∀ {a : R}, a ∈ I → l a • algebraMap R S a * algebraMap R S p ∈
      algebraMap R<x> S '' I.map (algebraMap R R<x>) := by
    intro a ha
    rw [smul_eq_mul, mul_assoc, mul_comm, mul_assoc, Set.mem_image]
    refine Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?h⟩) ?_
    case h =>
      rw [mul_comm]
      exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _
    · refine ⟨?_, ?_⟩
      · rw [mul_comm]
        apply Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ ha)
      · simp only [map_mul, mul_comm (algebraMap R S p) (l a)]
        rfl