awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 0 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 1 : ℝ) = 2 * z.re

Tactic:
exact (two_mul _).symm

Premises used: two_mul, Eq.symm
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
rw :
  HMul.hMul (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 0 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 1 : ℝ) -
      HMul.hMul (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 1 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 0 : ℝ) =
    z.re * z.re + z.im * z.im
⊢ Eq (α := ℝ) ((norm ℝ : (a : ℂ) → ℝ) z : ℝ) ((normSq : (a : ℂ) → ℝ) z : ℝ)

Tactic:
rw [Algebra.norm_eq_matrix_det Complex.basisOneI, Algebra.leftMulMatrix_complex,
    Matrix.det_fin_two, normSq_apply]

Premises used: Algebra.norm_eq_matrix_det, Algebra.leftMulMatrix_complex, Complex.basisOneI, Complex.normSq_apply, Matrix.det_fin_two
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
⊢ HMul.hMul (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 0 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 1 : ℝ) -
      HMul.hMul (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 1 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 0 : ℝ) =
    z.re * z.re + z.im * z.im

Tactic:
simp
-- Module: Mathlib.RingTheory.Complex
Goal:
⊢ norm ℝ = (↑normSq : ℂ →* ℝ)

Tactic:
MonoidHom.ext Algebra.norm_complex_apply

Premises used: MonoidHom.ext, Algebra.norm_complex_apply
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x a b : S
ha : Membership.mem (γ := Set S) {a : S | ∀ (b : S), Membership.mem (γ := Subalgebra R S) R[x] (a * b)} a
hb : Membership.mem (γ := Set S) {a : S | ∀ (b : S), Membership.mem (γ := Subalgebra R S) R[x] (a * b)} b
c : S
⊢ Membership.mem (γ := Subalgebra R S) R[x] ((a + b) * c)

Tactic:
simpa only [add_mul] using Subalgebra.add_mem _ (ha c) (hb c)

Premises used: add_mul, Subalgebra.add_mem
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x b : S
⊢ Membership.mem (γ := Subalgebra R S) R[x] (0 * b)

Tactic:
simp only [zero_mul, zero_mem]

Premises used: MulZeroClass.zero_mul, ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x c a : S
ha : Membership.mem (γ := Set S) {a : S | ∀ (b : S), Membership.mem (γ := Subalgebra R S) R[x] (a * b)} a
b : S
⊢ Membership.mem (γ := Subalgebra R S) R[x] (c • a * b)

Tactic:
simpa only [smul_eq_mul, mul_left_comm, mul_assoc] using ha (c * b)

Premises used: HMul.hMul, mul_assoc, mul_left_comm, smul_eq_mul
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y : S
h : (↑R[x] : Set S) = (↑R[y] : Set S)
⊢ Eq (α := Ideal S) (conductor R x) (conductor R y)

Tactic:
Ideal.ext fun _ => forall_congr' fun _ => Set.ext_iff.mp h _

Premises used: HMul.hMul, Ideal.ext, Iff.mp, forall_congr', Set.ext_iff
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y : S
hy : y ∈ (↑(conductor R x) : Set S)
⊢ y ∈ (↑R[x] : Set S)

Tactic:
simpa only [mul_one] using hy 1

Premises used: mul_one, OfNat.ofNat
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x y : S
⊢ Membership.mem (γ := Ideal S) (conductor R x) y ↔ ∀ (b : S), Membership.mem (γ := Subalgebra R S) R[x] (y * b)

Tactic:
⟨fun h => h, fun h => h⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
h : Eq (α := Subalgebra R S) R[x] ⊤
⊢ Eq (α := Ideal S) (conductor R x) ⊤

Tactic:
simp only [Ideal.eq_top_iff_one, mem_conductor_iff, h, mem_top, forall_const]

Premises used: Algebra.mem_top, mem_conductor_iff, Ideal.eq_top_iff_one, forall_const
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
pb : PowerBasis R S
⊢ Eq (α := Ideal S) (conductor R pb.gen) ⊤

Tactic:
conductor_eq_top_of_adjoin_eq_top pb.adjoin_gen_eq_top

Premises used: PowerBasis.adjoin_gen_eq_top, conductor_eq_top_of_adjoin_eq_top
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
h : Eq (α := Ideal S) (conductor R x) ⊤
⊢ Eq (α := Subalgebra R S) R[x] ⊤

Tactic:
eq_top_iff.mpr fun y ↦
    one_mul y ▸ mem_conductor_iff.mp ((Ideal.eq_top_iff_one (conductor R x)).mp h) y

Premises used: Iff.mpr, Eq.rec, mem_conductor_iff, Ideal.eq_top_iff_one, conductor, Iff.mp, Algebra.eq_top_iff, one_mul
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
⊢ Eq (α := Ideal S) (conductor R x) ⊤ ↔ Eq (α := Subalgebra R S) R[x] ⊤

Tactic:
⟨fun h ↦ adjoin_eq_top_of_conductor_eq_top h, fun h ↦ conductor_eq_top_of_adjoin_eq_top h⟩

Premises used: adjoin_eq_top_of_conductor_eq_top, Iff.intro, conductor_eq_top_of_adjoin_eq_top
-- Module: Mathlib.RingTheory.Conductor
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
inl :
  Subsingleton L →
    (Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
      ∀ (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)))
inr :
  Nontrivial L →
    (Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
      ∀ (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)))
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (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:
cases subsingleton_or_nontrivial L

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Conductor
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 : Subsingleton L
inl :
  Membership.mem (γ := Submodule S L) ⊤ y ↔
    ∀ (z : S), Membership.mem (γ := Subalgebra R L) ⊤ (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (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 [Subsingleton.elim (coeSubmodule L _) ⊤, Subsingleton.elim (Algebra.adjoin R _) ⊤]

Premises used: Algebra.adjoin, Subsingleton.elim, Top.top, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.Conductor
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 : Subsingleton L
⊢ Membership.mem (γ := Submodule S L) ⊤ y ↔
    ∀ (z : S), Membership.mem (γ := Subalgebra R L) ⊤ (HMul.hMul (β := L) y ((algebraMap S L : (a : S) → L) z : L))

Tactic:
simp
-- Module: Mathlib.RingTheory.Conductor
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
trans :
  Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (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))
trans₁ :
  (∀ (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))
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (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:
trans ∀ z, y * (algebraMap S L) z ∈ (R[x]).map (IsScalarTower.toAlgHom R S L)
-- Module: Mathlib.RingTheory.Conductor
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
simp :
  (∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y) ↔
    ∀ (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)
⊢ Membership.mem (γ := Submodule S L) (coeSubmodule L (conductor R x)) y ↔
    ∀ (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))

Tactic:
simp only [coeSubmodule, Submodule.mem_map, linearMap_apply, Subalgebra.mem_map,
      IsScalarTower.coe_toAlgHom']

Premises used: IsScalarTower.coe_toAlgHom', Submodule.mem_map, Algebra.linearMap_apply, Subalgebra.mem_map, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.Conductor
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
mp :
  (∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y) →
    ∀ (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)
mpr :
  (∀ (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
⊢ (∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y) ↔
    ∀ (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)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Conductor
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
hy : Membership.mem (γ := Submodule S S) (conductor R x) y
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)

Tactic:
⟨_, hy z, map_mul _ _ _⟩

Premises used: map_mul, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Conductor
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
hy : Membership.mem (γ := Submodule S S) (conductor R x) y
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)

Tactic:
exact ⟨_, hy z, map_mul _ _ _⟩
-- Module: Mathlib.RingTheory.Conductor
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)
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
⊢ ∃ (y_1 : S), Membership.mem (γ := Submodule S S) (conductor R x) y_1 ∧ (algebraMap S L : (a : S) → L) y_1 = y

Tactic:
obtain ⟨y, _, e⟩ := H 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Conductor
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)
⊢ (algebraMap S L : (a : S) → L) y = y_1

Tactic:
rw [map_one, mul_one] at e

Premises used: map_one, mul_one
-- Module: Mathlib.RingTheory.Conductor
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
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)
⊢ ∃ (y : S), Membership.mem (γ := Submodule S S) (conductor R x) y ∧ (algebraMap S L : (a : S) → L) y = y_1

Tactic:
subst e
-- Module: Mathlib.RingTheory.Conductor
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)
⊢ ∀ (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

Premises used: Function.Injective.eq_iff, exists_eq_right, map_mul, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Conductor
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), Membership.mem (γ := Subalgebra R S) R[x] (y * z)
⊢ ∃ (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)

Tactic:
⟨_, H, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Conductor
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), Membership.mem (γ := Subalgebra R S) R[x] (y * z)
⊢ ∃ (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)

Tactic:
exact ⟨_, H, rfl⟩
-- Module: Mathlib.RingTheory.Conductor
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
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))
⊢ (∀ (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))

Tactic:
rw [AlgHom.map_adjoin, Set.image_singleton]

Premises used: Set.image_singleton, AlgHom.map_adjoin
-- Module: Mathlib.RingTheory.Conductor
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) 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:
rfl
-- Module: Mathlib.RingTheory.Conductor
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
⊢ ∃ (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'

Premises used: Ideal.map, Ideal.span, Finsupp.mem_span_image_iff_linearCombination
-- Module: Mathlib.RingTheory.Conductor
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
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)
⊢ 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'
-- Module: Mathlib.RingTheory.Conductor
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
⊢ (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'

Premises used: Finsupp.linearCombination_apply
-- Module: Mathlib.RingTheory.Conductor
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
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))
⊢ 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:
rw [← H', mul_comm, Finsupp.sum_mul]

Premises used: mul_comm, Finsupp.sum_mul