awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI :
  IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
h : Eq.{v + 1} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) ⊤
mp :
  ∃ (p : Ideal R),
    p.IsPrime ∧
      Eq (α := Ideal (R × S))
        (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (p.prod ⊤)
⊢ (∃ (p : Ideal R),
      p.IsPrime ∧
        Eq (α := Ideal (R × S))
          (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (p.prod ⊤)) ∨
    ∃ (p : Ideal S),
      p.IsPrime ∧
        Eq (α := Ideal (R × S))
          (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (prod ⊤ p)

Tactic:
left
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI :
  IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I))
h : Eq.{v + 1} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) ⊤
mp :
  ∀ (hI : IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤))
    (h : Eq.{v + 1} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) ⊤),
    ∃ (p : Ideal R),
      p.IsPrime ∧ Eq (α := Ideal (R × S)) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤) (p.prod ⊤)
⊢ ∃ (p : Ideal R),
    p.IsPrime ∧
      Eq (α := Ideal (R × S))
        (prod (map (F := R × S →+* R) (RingHom.fst R S) I) (map (F := R × S →+* S) (RingHom.snd R S) I)) (p.prod ⊤)

Tactic:
rw [h] at hI ⊢
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI : IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤)
h : Eq.{v + 1} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) ⊤
⊢ ∃ (p : Ideal R), p.IsPrime ∧ Eq (α := Ideal (R × S)) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤) (p.prod ⊤)

Tactic:
⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩

Premises used: Ideal.isPrime_of_isPrime_prod_top, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal (R × S)
hI : IsPrime (α := R × S) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤)
h : Eq.{v + 1} (α := Ideal S) (map (F := R × S →+* S) (RingHom.snd R S) I) ⊤
⊢ ∃ (p : Ideal R), p.IsPrime ∧ Eq (α := Ideal (R × S)) (prod (map (F := R × S →+* R) (RingHom.fst R S) I) ⊤) (p.prod ⊤)

Tactic:
exact ⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : Ideal R
h : p.IsPrime
⊢ IsPrime (α := R × S) (p.prod ⊤)

Tactic:
isPrime_ideal_prod_top

Premises used: Ideal.isPrime_ideal_prod_top
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : Ideal R
h : p.IsPrime
⊢ IsPrime (α := R × S) (p.prod ⊤)

Tactic:
exact isPrime_ideal_prod_top

Premises used: Ideal.isPrime_ideal_prod_top
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : Ideal S
h : p.IsPrime
⊢ IsPrime (α := R × S) (prod ⊤ p)

Tactic:
isPrime_ideal_prod_top'

Premises used: Ideal.isPrime_ideal_prod_top'
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : Ideal S
h : p.IsPrime
⊢ IsPrime (α := R × S) (prod ⊤ p)

Tactic:
exact isPrime_ideal_prod_top'

Premises used: Ideal.isPrime_ideal_prod_top'
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J : Ideal S
inst_2 : IsPrincipalIdealRing R
inst_3 : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Set.Nonempty (α := R) {generator (Ideal.map (F := R × S →+* R) (RingHom.fst R S) I)}

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J : Ideal S
inst_2 : IsPrincipalIdealRing R
inst_3 : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Set.Nonempty (α := S) {generator (Ideal.map (F := R × S →+* S) (RingHom.snd R S) I)}

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J : Ideal S
inst_2 : IsPrincipalIdealRing R
inst_3 : IsPrincipalIdealRing S
I : Ideal (R × S)
rw :
  Submodule.IsPrincipal (R := R × S)
    (Ideal.span
      {(generator (Ideal.map (F := R × S →+* R) (RingHom.fst R S) I),
          generator (Ideal.map (F := R × S →+* S) (RingHom.snd R S) I))})
⊢ Submodule.IsPrincipal I

Tactic:
rw [I.ideal_prod_eq, ← span_singleton_generator (I.map _),
      ← span_singleton_generator (I.map (RingHom.snd R S)), ← Ideal.span, ← Ideal.span,
      ← Ideal.span_prod (iff_of_true (by simp) (by simp)), Set.singleton_prod_singleton]

Premises used: Ideal.span_prod, Ideal.map, Set.singleton_prod_singleton, Ideal.ideal_prod_eq, RingHom.snd, iff_of_true, Submodule.IsPrincipal.span_singleton_generator, Ideal.span
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J : Ideal S
inst_2 : IsPrincipalIdealRing R
inst_3 : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal (R := R × S)
    (Ideal.span
      {(generator (Ideal.map (F := R × S →+* R) (RingHom.fst R S) I),
          generator (Ideal.map (F := R × S →+* S) (RingHom.snd R S) I))})

Tactic:
⟨_, rfl⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Prod
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I_1 : Ideal R
J : Ideal S
inst_2 : IsPrincipalIdealRing R
inst_3 : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal (R := R × S)
    (Ideal.span
      {(generator (Ideal.map (F := R × S →+* R) (RingHom.fst R S) I),
          generator (Ideal.map (F := R × S →+* S) (RingHom.snd R S) I))})

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
⊢ HSMul.hSMul (β := Submodule R ↥J) I ⊤ ≤ Submodule.comap (Submodule.subtype J) I

Tactic:
simp [← Submodule.map_le_iff_le_comap, Ideal.mul_le_right]

Premises used: Ideal.mul_le_right, Submodule.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
a :
  ∀ (x : R ⧸ I) (x_1 : ↥J),
    Eq (α := (R ⧸ I) ⊗[R] R)
      (((((AlgebraTensorModule.curry (LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) :
                    R ⧸ I →ₗ[R] ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
                  (a : R ⧸ I) → ↥J →ₗ[R] (R ⧸ I) ⊗[R] R)
                x :
              ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
            (a : ↥J) → (R ⧸ I) ⊗[R] R)
          x_1 :
        (R ⧸ I) ⊗[R] R)
      (((((AlgebraTensorModule.curry
                      ((↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
                        f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)) :
                    R ⧸ I →ₗ[R] ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
                  (a : R ⧸ I) → ↥J →ₗ[R] (R ⧸ I) ⊗[R] R)
                x :
              ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
            (a : ↥J) → (R ⧸ I) ⊗[R] R)
          x_1 :
        (R ⧸ I) ⊗[R] R)
⊢ LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
x : R ⧸ I
x_1 : ↥J
a :
  Eq (α := (R ⧸ I) ⊗[R] R) (x ⊗ₜ[R] (↑x_1 : R))
    (((HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯ : (a : ↥J ⧸ I • ⊤) → R ⧸ I)
        (((quotTensorEquivQuotSMul (↥J) I : (R ⧸ I) ⊗[R] ↥J ≃ₗ[R] ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤) :
            (a : (R ⧸ I) ⊗[R] ↥J) → ↥J ⧸ I • ⊤)
          (x ⊗ₜ[R] x_1)) ⊗ₜ[R]
      1)
⊢ Eq (α := (R ⧸ I) ⊗[R] R)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) :
                  R ⧸ I →ₗ[R] ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
                (a : R ⧸ I) → ↥J →ₗ[R] (R ⧸ I) ⊗[R] R)
              x :
            ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
          (a : ↥J) → (R ⧸ I) ⊗[R] R)
        x_1 :
      (R ⧸ I) ⊗[R] R)
    (((((AlgebraTensorModule.curry
                    ((↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
                      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)) :
                  R ⧸ I →ₗ[R] ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
                (a : R ⧸ I) → ↥J →ₗ[R] (R ⧸ I) ⊗[R] R)
              x :
            ↥J →ₗ[R] (R ⧸ I) ⊗[R] R) :
          (a : ↥J) → (R ⧸ I) ⊗[R] R)
        x_1 :
      (R ⧸ I) ⊗[R] R)

Tactic:
simp [f, ← Ideal.Quotient.algebraMap_eq, Algebra.TensorProduct.tmul_one_eq_one_tmul]

Premises used: Ideal.Quotient.algebraMap_eq, Algebra.TensorProduct.tmul_one_eq_one_tmul
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
⊢ LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)

Tactic:
have : J.subtype.lTensor (R ⧸ I) =
      (TensorProduct.rid R (R ⧸ I)).symm ∘ₗ f ∘ₗ TensorProduct.quotTensorEquivQuotSMul J I := by
    ext
    simp [f, ← Ideal.Quotient.algebraMap_eq, Algebra.TensorProduct.tmul_one_eq_one_tmul]
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)
rw :
  Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
      (⇑((↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
            f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)) :
        (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R) ↔
    I ⊓ J = I * J
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
      (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R) ↔
    I ⊓ J = I * J

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)
simp :
  Submodule.map (Submodule.subtype J) (Submodule.comap (Submodule.subtype J) I) ≤
      Submodule.map (Submodule.subtype J) (HSMul.hSMul (β := Submodule R ↥J) I ⊤) ↔
    I ⊓ J = I * J
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
      (⇑((↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
            f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)) :
        (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R) ↔
    I ⊓ J = I * J

Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
    EquivLike.injective_comp, ← LinearMap.ker_eq_bot, f, Submodule.ker_mapQ,
    ← LinearMap.le_ker_iff_map, Submodule.ker_mkQ,
    ← (Submodule.map_le_map_iff_of_injective J.injective_subtype)]

Premises used: LinearMap.ker_eq_bot, EquivLike.injective_comp, Submodule.map_le_map_iff_of_injective, EmbeddingLike.comp_injective, Submodule.injective_subtype, Submodule.ker_mapQ, LinearMap.coe_comp, Submodule.ker_mkQ, LinearMap.le_ker_iff_map, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
f : ↥J ⧸ HSMul.hSMul (β := Submodule R ↥J) I ⊤ →ₗ[R] R ⧸ I :=
  (HSMul.hSMul (β := Submodule R ↥J) I ⊤).mapQ I (Submodule.subtype J) ⋯
this :
  LinearMap.lTensor (R ⧸ I) (Submodule.subtype J) =
    (↑(LinearEquiv.symm (TensorProduct.rid R (R ⧸ I))) : R ⧸ I →ₗ[R] (R ⧸ I) ⊗[R] R) ∘ₗ
      f ∘ₗ (↑(quotTensorEquivQuotSMul (↥J) I) : (R ⧸ I) ⊗[R] ↥J →ₗ[R] ↥J ⧸ I • ⊤)
⊢ Submodule.map (Submodule.subtype J) (Submodule.comap (Submodule.subtype J) I) ≤
      Submodule.map (Submodule.subtype J) (HSMul.hSMul (β := Submodule R ↥J) I ⊤) ↔
    I ⊓ J = I * J

Tactic:
simp [inf_comm, le_antisymm_iff, Ideal.mul_le_inf (I := I) (J := J)]

Premises used: inf_comm, le_antisymm_iff, Ideal.mul_le_inf
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
rw :
  Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
    (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R)
⊢ I ⊓ J = I * J

Tactic:
rw [← injective_lTensor_quotient_iff_inf_eq_mul]

Premises used: injective_lTensor_quotient_iff_inf_eq_mul
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
hf : Function.Injective (α := ↥J) (β := R) (⇑(Submodule.subtype J) : (a : ↥J) → R)
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
    (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R)

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
⊢ Function.Injective (α := ↥J) (β := R) (⇑(Submodule.subtype J) : (a : ↥J) → R)

Tactic:
J.injective_subtype

Premises used: Submodule.injective_subtype
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
⊢ Function.Injective (α := ↥J) (β := R) (⇑(Submodule.subtype J) : (a : ↥J) → R)

Tactic:
exact J.injective_subtype

Premises used: Submodule.injective_subtype
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
⊢ IsIdempotentElem I

Tactic:
simp [IsIdempotentElem, ← Ideal.inf_eq_mul_of_pure]

Premises used: Ideal.inf_eq_mul_of_pure, IsIdempotentElem
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
h' : IsIdempotentElem I
⊢ ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e

Tactic:
rw [Ideal.isIdempotentElem_iff_of_fg _ h] at h'

Premises used: Ideal.isIdempotentElem_iff_of_fg
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I.FG
h' : ∃ (e : R), IsIdempotentElem e ∧ I = R ∙ e
obtain : ∀ (e : R) (he : IsIdempotentElem e) (h : FG (R ∙ e)), Pure (R ∙ e)
⊢ I.Pure

Tactic:
obtain ⟨e, he, rfl⟩ := h'

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
⊢ e + (1 - e) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
⊢ e * (1 - e) = 0

Tactic:
grind [IsIdempotentElem]

Premises used: IsIdempotentElem
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
⊢ Module.Flat R
    (HasQuotient.Quotient R (B := Submodule R R) (R ∙ e) × HasQuotient.Quotient R (B := Ideal R) (span {1 - e}))

Tactic:
have : Module.Flat R ((R ⧸ R ∙ e) × R ⧸ span {1 - e}) :=
    .of_linearEquiv <| AlgEquiv.prodQuotientOfIsIdempotentElem R he he.one_sub (by simp)
      (by grind [IsIdempotentElem]) |>.toLinearEquiv.symm
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
this :
  Module.Flat R
    (HasQuotient.Quotient R (B := Submodule R R) (R ∙ e) × HasQuotient.Quotient R (B := Ideal R) (span {1 - e}))
apply :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ e) →ₗ[R] HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
    (LinearMap.fst R (HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
        (HasQuotient.Quotient R (B := Ideal R) (span {1 - e})) ∘ₗ
      LinearMap.inl R (HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
        (HasQuotient.Quotient R (B := Ideal R) (span {1 - e})))
    LinearMap.id
⊢ Pure (R ∙ e)

Tactic:
apply Module.Flat.of_retract (LinearMap.inl R _ (R ⧸ span {1 - e})) (LinearMap.fst R _ _)

Premises used: LinearMap.fst, LinearMap.inl, HSub.hSub, HasQuotient.Quotient, Module.Flat.of_retract, Ideal.span, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
e : R
he : IsIdempotentElem e
h : FG (R ∙ e)
this :
  Module.Flat R
    (HasQuotient.Quotient R (B := Submodule R R) (R ∙ e) × HasQuotient.Quotient R (B := Ideal R) (span {1 - e}))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (R ∙ e) →ₗ[R] HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
    (LinearMap.fst R (HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
        (HasQuotient.Quotient R (B := Ideal R) (span {1 - e})) ∘ₗ
      LinearMap.inl R (HasQuotient.Quotient R (B := Ideal R) (R ∙ e))
        (HasQuotient.Quotient R (B := Ideal R) (span {1 - e})))
    LinearMap.id

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
rw :
  ∀ ⦃I_1 : Ideal R⦄,
    I_1.FG →
      Function.Injective (α := (R ⧸ I) ⊗[R] ↥I_1) (β := (R ⧸ I) ⊗[R] R)
        (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype I_1)) : (a : (R ⧸ I) ⊗[R] ↥I_1) → (R ⧸ I) ⊗[R] R)
⊢ I.Pure

Tactic:
rw [Pure, Module.Flat.iff_lTensor_injective]

Premises used: Module.Flat.iff_lTensor_injective, Ideal.Pure
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
hJ : J.FG
rw : I ⊓ J = I * J
⊢ Function.Injective (α := (R ⧸ I) ⊗[R] ↥J) (β := (R ⧸ I) ⊗[R] R)
    (⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) : (a : (R ⧸ I) ⊗[R] ↥J) → (R ⧸ I) ⊗[R] R)

Tactic:
rw [injective_lTensor_quotient_iff_inf_eq_mul]

Premises used: injective_lTensor_quotient_iff_inf_eq_mul
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
hJ : J.FG
⊢ I ⊓ J = I * J

Tactic:
H hJ
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
hJ : J.FG
⊢ I ⊓ J = I * J

Tactic:
exact H hJ
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
h : x ∈ I * span {x}
⊢ ∃ z ∈ I, z * x = x

Tactic:
rw [Ideal.mem_mul_span_singleton] at h

Premises used: Ideal.mem_mul_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
h : ∃ z ∈ I, z * x = x
⊢ ∃ y ∈ I, x = x * y

Tactic:
grind
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
suffices : x ∈ I * span {x}
⊢ ∃ y ∈ I, x = x * y

Tactic:
suffices h : x ∈ I * Ideal.span {x} by
    rw [Ideal.mem_mul_span_singleton] at h
    grind
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
rw : x ∈ I ⊓ span {x}
⊢ x ∈ I * span {x}

Tactic:
rw [← I.inf_eq_mul_of_pure]

Premises used: Ideal.inf_eq_mul_of_pure
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
⊢ x ∈ I ⊓ span {x}

Tactic:
⟨hx, subset_span rfl⟩

Premises used: Ideal.subset_span, Set.Mem, setOf, Set.inter, And.intro, rfl
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : I.Pure
x : R
hx : x ∈ I
⊢ x ∈ I ⊓ span {x}

Tactic:
exact ⟨hx, subset_span rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
obtain :
  ∀ (y : R) (hy : y ∈ I) (heq : x = x * y),
    Membership.mem (γ := Submodule R R)
      (RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))) x
⊢ Membership.mem (γ := Submodule R R)
    (RingHom.ker (F := R →+* Localization.AtPrime p) (algebraMap R (Localization.AtPrime p))) x

Tactic:
obtain ⟨y, hy, heq⟩ := h _ hx
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
rw : ∃ m ∈ p.primeCompl, 1 - y ∣ m
⊢ IsUnit (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (1 - y) : Localization.AtPrime p)

Tactic:
rw [IsLocalization.algebraMap_isUnit_iff p.primeCompl]

Premises used: IsLocalization.algebraMap_isUnit_iff, Ideal.primeCompl
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
⊢ 1 - y ∣ 1 - y

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
refine : ∀ (hz : 1 - y ∈ (↑p : Set R)), 1 ∈ p
⊢ ∃ m ∈ p.primeCompl, 1 - y ∣ m

Tactic:
refine ⟨1 - y, fun hz ↦ p.one_notMem ?_, by simp⟩
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
hz : 1 - y ∈ (↑p : Set R)
rw : 1 - y + y ∈ p
⊢ 1 ∈ p

Tactic:
rw [← sub_add_cancel 1 y]

Premises used: OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
hz : 1 - y ∈ (↑p : Set R)
⊢ 1 - y + y ∈ p

Tactic:
Ideal.add_mem _ hz (hle hy)

Premises used: Set.Mem, Ideal.add_mem
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
hz : 1 - y ∈ (↑p : Set R)
⊢ 1 - y + y ∈ p

Tactic:
exact Ideal.add_mem _ hz (hle hy)

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.Ideal.Pure
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : ∀ x ∈ I, ∃ y ∈ I, x = x * y
p : Ideal R
inst_1 : p.IsPrime
hle : I ≤ p
x : R
hx : x ∈ I
y : R
hy : y ∈ I
heq : x = x * y
⊢ IsUnit (M := Localization.AtPrime p)
    ((algebraMap R (Localization.AtPrime p) : (a : R) → Localization.AtPrime p) (1 - y) : Localization.AtPrime p)

Tactic:
have : IsUnit (algebraMap R (Localization.AtPrime p) (1 - y)) := by
    rw [IsLocalization.algebraMap_isUnit_iff p.primeCompl]
    refine ⟨1 - y, fun hz ↦ p.one_notMem ?_, by simp⟩
    rw [← sub_add_cancel 1 y]
    exact Ideal.add_mem _ hz (hle hy)