awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Set M
r : R
h : r ∈ N.colon S
s : M
hs : s ∈ (↑(span R S) : Set M)
mem : ∀ x ∈ S, r • x ∈ N
zero : HSMul.hSMul (β := M) r 0 ∈ N
add :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (span R S) x →
      Membership.mem (γ := Submodule R M) (span R S) y → r • x ∈ N → r • y ∈ N → r • (x + y) ∈ N
smul : ∀ (a : R) (x : M), Membership.mem (γ := Submodule R M) (span R S) x → r • x ∈ N → r • a • x ∈ N
⊢ r • s ∈ N

Tactic:
induction hs using Submodule.span_induction with
  | mem => aesop (add simp mem_colon)
  | zero => simp
  | add => aesop
  | smul => simp_all [smul_mem, smul_comm r]

Premises used: Submodule.smul, Submodule.zero, Submodule.mem_colon, SMulCommClass.smul_comm, Submodule.add, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
S : Set R
⊢ colon I (↑(Ideal.span S) : Set R) = colon I S

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
x : M
r : R
⊢ r ∈ N.colon (↑(R ∙ x) : Set M) ↔ r • x ∈ N

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x r : R
⊢ r ∈ colon I (↑(Ideal.span {x}) : Set R) ↔ r * x ∈ I

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N P : Submodule R M
h : ∀ (x : R), x ∈ (map N.mkQ P).annihilator ↔ x ∈ N.colon (↑P : Set M)
⊢ (map N.mkQ P).annihilator = N.colon (↑P : Set M)

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N P : Submodule R M
x : R
h : (∀ n ∈ map N.mkQ P, x • n = 0) ↔ ∀ s ∈ (↑P : Set M), x • s ∈ N
⊢ x ∈ (map N.mkQ P).annihilator ↔ x ∈ N.colon (↑P : Set M)

Tactic:
rw [mem_annihilator, mem_colon]

Premises used: Submodule.mem_annihilator, Submodule.mem_colon
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N P : Submodule R M
x : R
⊢ (∀ n ∈ map N.mkQ P, x • n = 0) ↔ ∀ s ∈ (↑P : Set M), x • s ∈ N

Tactic:
⟨fun H p hp ↦ (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
    fun H _ ⟨p, hp, hpm⟩ ↦ hpm ▸ ((Quotient.mk_eq_zero N).2 <| H p hp)⟩

Premises used: Iff.mpr, Submodule.Quotient.mk, Eq.rec, _private.0.Submodule.annihilator_map_mkQ_eq_colon.match_1, Iff.intro, Iff.mp, HSMul.hSMul, Submodule.mem_map_of_mem, OfNat.ofNat, Eq, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N P : Submodule R M
x : R
⊢ (∀ n ∈ map N.mkQ P, x • n = 0) ↔ ∀ s ∈ (↑P : Set M), x • s ∈ N

Tactic:
exact ⟨fun H p hp ↦ (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
    fun H _ ⟨p, hp, hpm⟩ ↦ hpm ▸ ((Quotient.mk_eq_zero N).2 <| H p hp)⟩
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
h : ∀ (r : R), Membership.mem (γ := Ideal R) (Module.annihilator.{u_1, u_2} R (M ⧸ N)) r ↔ r ∈ N.colon Set.univ
⊢ Module.annihilator.{u_1, u_2} R (M ⧸ N) = N.colon Set.univ

Tactic:
ext r
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
⊢ ⊤ = map N.mkQ ⊤

Tactic:
simpa [map_top] using (LinearMap.range_eq_top.mpr (mkQ_surjective N)).symm

Premises used: Iff.mpr, Submodule.map_top, LinearMap.range_eq_top, Submodule.mkQ_surjective, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
⊢ ⊤ = map N.mkQ ⊤

Tactic:
have htop : (⊤ : Submodule R (M ⧸ N)) = (⊤ : Submodule R M).map N.mkQ := by
    simpa [map_top] using (LinearMap.range_eq_top.mpr (mkQ_surjective N)).symm
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
r : R
htop : ⊤ = map N.mkQ ⊤
h : Membership.mem (γ := Ideal R) (annihilator.{u_1, u_2} (M := M ⧸ N) ⊤) r ↔ r ∈ N.colon Set.univ
h₁ : r ∈ (map N.mkQ ⊤).annihilator ↔ r ∈ N.colon Set.univ
h₂ : r ∈ N.colon (↑⊤ : Set M) ↔ r ∈ N.colon Set.univ
h₃ h₄ : r ∈ N.colon Set.univ ↔ r ∈ N.colon Set.univ
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_1, u_2} R (M ⧸ N)) r ↔ r ∈ N.colon Set.univ

Tactic:
rw [← annihilator_top (R := R) (M := M ⧸ N), htop,
    annihilator_map_mkQ_eq_colon (N := N) (P := ⊤), Submodule.top_coe]

Premises used: Submodule.annihilator_map_mkQ_eq_colon, Submodule.annihilator_top, Submodule.top_coe
-- Module: Mathlib.RingTheory.Ideal.Colon
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
rw : colon I Set.univ = I
rw₁ rw₂ : I = I
⊢ Module.annihilator R (R ⧸ I) = I

Tactic:
rw [Submodule.annihilator_quotient, colon_univ]

Premises used: Submodule.annihilator_quotient, Submodule.colon_univ
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
rw :
  Submodule.map (Submodule.subtype I)
      (LinearMap.ker (R₂ := R) (M₂ := I.Cotangent) (τ₁₂ := RingHom.id R) (HSMul.hSMul (β := Submodule R ↥I) I ⊤).mkQ) =
    HPow.hPow (β := ℕ) I 2
rw₁ : Submodule.map (Submodule.subtype I) (HSMul.hSMul (β := Submodule R ↥I) I ⊤) = HPow.hPow (β := ℕ) I 2
rw₂ : Submodule.map (Submodule.subtype I) (HSMul.hSMul (β := Submodule R ↥I) I ⊤) = I * I
rw₃ : I • Submodule.map (Submodule.subtype I) ⊤ = I * I
rw₄ : I * Submodule.map (Submodule.subtype I) ⊤ = I * I
rw₅ rw₆ : I * I = I * I
⊢ Submodule.map (Submodule.subtype I) I.toCotangent.ker = HPow.hPow (β := ℕ) I 2

Tactic:
rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
    smul_eq_mul, Submodule.map_subtype_top]

Premises used: pow_two, Submodule.map_smul'', Submodule.subtype, Submodule.map_subtype_top, Submodule.ker_mkQ, smul_eq_mul, Ideal.toCotangent, Top.top
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : ↥I
rw : x ∈ I.toCotangent.ker ↔ (↑x : R) ∈ Submodule.map (Submodule.subtype I) I.toCotangent.ker
⊢ x ∈ I.toCotangent.ker ↔ (↑x : R) ∈ HPow.hPow (β := ℕ) I 2

Tactic:
rw [← I.map_toCotangent_ker]

Premises used: Ideal.map_toCotangent_ker
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : ↥I
⊢ x ∈ I.toCotangent.ker ↔ (↑x : R) ∈ Submodule.map (Submodule.subtype I) I.toCotangent.ker

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x y : ↥I
rw :
  HSub.hSub (α := I.Cotangent) (β := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) y : I.Cotangent) =
      0 ↔
    (↑x : R) - (↑y : R) ∈ HPow.hPow (β := ℕ) I 2
⊢ Eq (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)
      ((I.toCotangent : (a : ↥I) → I.Cotangent) y : I.Cotangent) ↔
    (↑x : R) - (↑y : R) ∈ HPow.hPow (β := ℕ) I 2

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x y : ↥I
⊢ HSub.hSub (α := I.Cotangent) (β := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) y : I.Cotangent) =
      0 ↔
    (↑x : R) - (↑y : R) ∈ HPow.hPow (β := ℕ) I 2

Tactic:
I.mem_toCotangent_ker

Premises used: Ideal.mem_toCotangent_ker, Set.Mem, Submodule.Quotient.mk, setOf, Quotient.map₂, Set.preimage, Set.singleton
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x y : ↥I
⊢ HSub.hSub (α := I.Cotangent) (β := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) y : I.Cotangent) =
      0 ↔
    (↑x : R) - (↑y : R) ∈ HPow.hPow (β := ℕ) I 2

Tactic:
exact I.mem_toCotangent_ker

Premises used: Ideal.mem_toCotangent_ker
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : ↥I
⊢ Eq (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent) (0 : I.Cotangent) ↔
    (↑x : R) ∈ HPow.hPow (β := ℕ) I 2

Tactic:
I.mem_toCotangent_ker

Premises used: Ideal.mem_toCotangent_ker, Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ Function.Surjective (α := ↥I) (β := I.Cotangent) (⇑I.toCotangent : (a : ↥I) → I.Cotangent)

Tactic:
Submodule.mkQ_surjective _

Premises used: Ideal.Cotangent, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ I.toCotangent.range = ⊤

Tactic:
Submodule.range_mkQ _

Premises used: Set.Mem, Submodule.range_mkQ, Ideal.Cotangent, Ideal.toCotangent
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
mp : Subsingleton.{u + 1} I.Cotangent → IsIdempotentElem I
mpr : IsIdempotentElem I → Subsingleton.{u + 1} I.Cotangent
⊢ Subsingleton.{u + 1} I.Cotangent ↔ IsIdempotentElem I

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
H : Subsingleton.{u + 1} I.Cotangent
⊢ IsIdempotentElem I

Tactic:
(pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) ?_)

Premises used: pow_two, Set.Mem, Ideal.pow_le_self, two_ne_zero, le_antisymm, IsIdempotentElem, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
H : Subsingleton.{u + 1} I.Cotangent
mp : I ≤ HPow.hPow (β := ℕ) I 2
⊢ IsIdempotentElem I

Tactic:
refine (pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) ?_)

Premises used: pow_two, Ideal.pow_le_self, two_ne_zero, le_antisymm, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
H : Subsingleton.{u + 1} I.Cotangent
⊢ I ≤ HPow.hPow (β := ℕ) I 2

Tactic:
fun x hx => (I.toCotangent_eq_zero ⟨x, hx⟩).mp (Subsingleton.elim _ _)

Premises used: Set.Mem, Subtype.mk, Ideal.toCotangent_eq_zero, Iff.mp, Ideal.toCotangent, Subsingleton.elim, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ IsIdempotentElem I → Subsingleton.{u + 1} I.Cotangent

Tactic:
fun e =>
      ⟨fun x y =>
        Quotient.inductionOn₂' x y fun x y =>
          I.toCotangent_eq.mpr <| ((pow_two I).trans e).symm ▸ I.sub_mem x.prop y.prop⟩

Premises used: Quotient.inductionOn₂', Subsingleton.intro
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ IsIdempotentElem I → Subsingleton.{u + 1} I.Cotangent

Tactic:
exact fun e =>
      ⟨fun x y =>
        Quotient.inductionOn₂' x y fun x y =>
          I.toCotangent_eq.mpr <| ((pow_two I).trans e).symm ▸ I.sub_mem x.prop y.prop⟩
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
rw : Submodule.map (Submodule.subtype I) (HSMul.hSMul (β := Submodule R ↥I) I ⊤) ≤ HPow.hPow (β := ℕ) I 2
rw₁ : I • Submodule.map (Submodule.subtype I) ⊤ ≤ HPow.hPow (β := ℕ) I 2
rw₂ : I • (Submodule.subtype I).range ≤ HPow.hPow (β := ℕ) I 2
rw₃ : I • I ≤ HPow.hPow (β := ℕ) I 2
rw₄ : I * I ≤ HPow.hPow (β := ℕ) I 2
rw₅ rw₆ : I * I ≤ I * I
⊢ HSMul.hSMul (β := Submodule R ↥I) I ⊤ ≤ Submodule.comap (Submodule.subtype I) (HPow.hPow (β := ℕ) I 2)

Tactic:
rw [← Submodule.map_le_iff_le_comap, Submodule.map_smul'', Submodule.map_top,
        Submodule.range_subtype, smul_eq_mul, pow_two]

Premises used: pow_two, Submodule.map_smul'', Submodule.map_top, smul_eq_mul, Submodule.map_le_iff_le_comap, Submodule.range_subtype
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ I.cotangentToQuotientSquare ∘ₗ I.toCotangent = Submodule.mkQ (HPow.hPow (β := ℕ) I 2) ∘ₗ Submodule.subtype I

Tactic:
LinearMap.ext fun _ => rfl

Premises used: LinearMap.ext, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : ↥I
⊢ Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) ((I.toCotangent : (a : ↥I) → I.Cotangent) x) :
      R ⧸ HPow.hPow (β := ℕ) I 2)
    ((Submodule.mkQ (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) (↑x : R) : R ⧸ HPow.hPow (β := ℕ) I 2)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
rw :
  ∀ (a : I.Cotangent),
    Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
        ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) a : R ⧸ HPow.hPow (β := ℕ) I 2)
        (0 : R ⧸ HPow.hPow (β := ℕ) I 2) →
      a = 0
⊢ Function.Injective (α := I.Cotangent) (β := R ⧸ HPow.hPow (β := ℕ) I 2)
    (⇑I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : I.Cotangent
hx :
  Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)
    (0 : R ⧸ HPow.hPow (β := ℕ) I 2)
obtain :
  ∀ (x : ↥I)
    (hx :
      Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
        ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) ((I.toCotangent : (a : ↥I) → I.Cotangent) x) :
          R ⧸ HPow.hPow (β := ℕ) I 2)
        (0 : R ⧸ HPow.hPow (β := ℕ) I 2)),
    Eq (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent) (0 : I.Cotangent)
⊢ x = 0

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : ↥I
hx :
  Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) ((I.toCotangent : (a : ↥I) → I.Cotangent) x) :
      R ⧸ HPow.hPow (β := ℕ) I 2)
    (0 : R ⧸ HPow.hPow (β := ℕ) I 2)
⊢ Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    ((Submodule.mkQ (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) (↑x : R) : R ⧸ HPow.hPow (β := ℕ) I 2)
    (0 : R ⧸ HPow.hPow (β := ℕ) I 2)

Tactic:
rw [toCotangent_to_quotient_square] at hx

Premises used: Ideal.toCotangent_to_quotient_square
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : ↥I
hx :
  Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    ((Submodule.mkQ (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) (↑x : R) : R ⧸ HPow.hPow (β := ℕ) I 2)
    (0 : R ⧸ HPow.hPow (β := ℕ) I 2)
rwa : (↑x : R) ∈ HPow.hPow (β := ℕ) I 2
rwa₁ rwa₂ rwa₃ rwa₄ : Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2) (Submodule.Quotient.mk (↑x : R)) 0
⊢ Eq (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent) (0 : I.Cotangent)

Tactic:
rwa [Ideal.toCotangent_eq_zero, ← Submodule.Quotient.mk_eq_zero (I ^ 2)]

Premises used: Ideal.toCotangent_eq_zero, HPow.hPow, OfNat.ofNat, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : I.Cotangent
obtain : ∀ (m : ↥I), HSMul.hSMul (β := I.Cotangent) x ((I.toCotangent : (a : ↥I) → I.Cotangent) m : I.Cotangent) = 0
⊢ x • m = 0

Tactic:
obtain ⟨m, rfl⟩ := Ideal.toCotangent_surjective _ m

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
rw : (↑(x • m) : R) ∈ I * I
⊢ HSMul.hSMul (β := I.Cotangent) x ((I.toCotangent : (a : ↥I) → I.Cotangent) m : I.Cotangent) = 0

Tactic:
rw [← map_smul, Ideal.toCotangent_eq_zero, pow_two]

Premises used: pow_two, Ideal.toCotangent_eq_zero, map_smul
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ (↑(x • m) : R) ∈ I * I

Tactic:
Ideal.mul_mem_mul hx m.2

Premises used: Set.Mem, Ideal.mul_mem_mul, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ (↑(x • m) : R) ∈ I * I

Tactic:
exact Ideal.mul_mem_mul hx m.2

Premises used: Ideal.mul_mem_mul, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ Module.IsTorsionBySet R I.Cotangent (↑I : Set R)

Tactic:
fun m x ↦ m.smul_eq_zero_of_mem x.2

Premises used: Ideal.Cotangent.smul_eq_zero_of_mem, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
rw : I.cotangentIdeal • I.cotangentIdeal ≤ ⊥
⊢ HPow.hPow (β := ℕ) I.cotangentIdeal 2 = ⊥

Tactic:
rw [eq_bot_iff, pow_two I.cotangentIdeal, ← smul_eq_mul]

Premises used: Ideal.cotangentIdeal, pow_two, smul_eq_mul, eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R ⧸ HPow.hPow (β := ℕ) I 2
hx : x ∈ I.cotangentIdeal • I.cotangentIdeal
⊢ Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ x

Tactic:
Submodule.smul_induction_on hx ?_ ?_

Premises used: Submodule.smul_induction_on
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R ⧸ HPow.hPow (β := ℕ) I 2
hx : x ∈ I.cotangentIdeal • I.cotangentIdeal
refine_1 :
  ∀ r ∈ I.cotangentIdeal,
    ∀ n ∈ I.cotangentIdeal,
      Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ (r • n)
refine_2 :
  ∀ (x y : R ⧸ HPow.hPow (β := ℕ) I 2),
    Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ x →
      Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ y →
        Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ (x + y)
⊢ Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ x

Tactic:
refine Submodule.smul_induction_on hx ?_ ?_
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x_1 : R ⧸ HPow.hPow (β := ℕ) I 2
hx_1 : x_1 ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ (↑I : Set R)
y : R
hy : y ∈ (↑I : Set R)
apply : HSub.hSub (α := R) ((fun (x1 x2 : R) ↦ x1 * x2) x y) 0 ∈ HPow.hPow (β := ℕ) I 2
⊢ Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥
    (HSMul.hSMul (α := R ⧸ HPow.hPow (β := ℕ) I 2) (β := R ⧸ HPow.hPow (β := ℕ) I 2)
      ((RingHom.toSemilinearMap (Quotient.mk (HPow.hPow (β := ℕ) I 2)) : (a : R) → R ⧸ I ^ 2) x :
        R ⧸ HPow.hPow (β := ℕ) I 2)
      ((RingHom.toSemilinearMap (Quotient.mk (HPow.hPow (β := ℕ) I 2)) : (a : R) → R ⧸ I ^ 2) y :
        R ⧸ HPow.hPow (β := ℕ) I 2))

Tactic:
apply (Submodule.Quotient.eq _).mpr _

Premises used: Submodule.Quotient.eq, Iff.mpr
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x_1 : R ⧸ HPow.hPow (β := ℕ) I 2
hx_1 : x_1 ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ (↑I : Set R)
y : R
hy : y ∈ (↑I : Set R)
rw : (fun (x1 x2 : R) ↦ x1 * x2) x y ∈ I * I
⊢ HSub.hSub (α := R) ((fun (x1 x2 : R) ↦ x1 * x2) x y) 0 ∈ HPow.hPow (β := ℕ) I 2

Tactic:
rw [sub_zero, pow_two]

Premises used: pow_two, sub_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x_1 : R ⧸ HPow.hPow (β := ℕ) I 2
hx_1 : x_1 ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ (↑I : Set R)
y : R
hy : y ∈ (↑I : Set R)
⊢ (fun (x1 x2 : R) ↦ x1 * x2) x y ∈ I * I

Tactic:
Ideal.mul_mem_mul hx hy

Premises used: Set.Mem, Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x_1 : R ⧸ HPow.hPow (β := ℕ) I 2
hx_1 : x_1 ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ (↑I : Set R)
y : R
hy : y ∈ (↑I : Set R)
⊢ (fun (x1 x2 : R) ↦ x1 * x2) x y ∈ I * I

Tactic:
exact Ideal.mul_mem_mul hx hy

Premises used: Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x_1 : R ⧸ HPow.hPow (β := ℕ) I 2
hx_1 : x_1 ∈ I.cotangentIdeal • I.cotangentIdeal
x y : R ⧸ HPow.hPow (β := ℕ) I 2
hx : Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ x
hy : Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ y
⊢ Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ (x + y)

Tactic:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x_1 : R ⧸ HPow.hPow (β := ℕ) I 2
hx_1 : x_1 ∈ I.cotangentIdeal • I.cotangentIdeal
x y : R ⧸ HPow.hPow (β := ℕ) I 2
hx : Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ x
hy : Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ y
⊢ Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ (x + y)

Tactic:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
⊢ Membership.mem (α := R ⧸ HPow.hPow (β := ℕ) I 2) I.cotangentIdeal
      ((Quotient.mk (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2) ↔
    x ∈ I

Tactic:
⟨fun ⟨y, hy, e⟩ ↦ ?_, fun h ↦ ⟨x, h, rfl⟩⟩

Premises used: Membership.mem, And.intro, Iff.intro, Exists.intro, rfl, _private.0.Ideal.mk_mem_cotangentIdeal.match_1
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
refine :
  Membership.mem (α := R ⧸ HPow.hPow (β := ℕ) I 2) I.cotangentIdeal
      ((Quotient.mk (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2) →
    ∀ (y : R) (hy : y ∈ (↑I : Set R))
      (e :
        Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
          ((RingHom.toSemilinearMap (Quotient.mk (HPow.hPow (β := ℕ) I 2)) : (a : R) → R ⧸ I ^ 2) y :
            R ⧸ HPow.hPow (β := ℕ) I 2)
          ((Quotient.mk (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)),
      x ∈ I
⊢ Membership.mem (α := R ⧸ HPow.hPow (β := ℕ) I 2) I.cotangentIdeal
      ((Quotient.mk (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2) ↔
    x ∈ I

Tactic:
refine ⟨fun ⟨y, hy, e⟩ ↦ ?_, fun h ↦ ⟨x, h, rfl⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
h :
  Membership.mem (α := R ⧸ HPow.hPow (β := ℕ) I 2) I.cotangentIdeal
    ((Quotient.mk (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)
y : R
hy : y ∈ (↑I : Set R)
e :
  Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    ((RingHom.toSemilinearMap (Quotient.mk (HPow.hPow (β := ℕ) I 2)) : (a : R) → R ⧸ I ^ 2) y :
      R ⧸ HPow.hPow (β := ℕ) I 2)
    ((Quotient.mk (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)
⊢ x ∈ I

Tactic:
simpa using sub_mem hy (Ideal.pow_le_self two_ne_zero
    ((Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mp e))

Premises used: sub_mem, Ideal.pow_le_self, two_ne_zero, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ comap (F := R →+* R ⧸ HPow.hPow (β := ℕ) I 2) (Quotient.mk (HPow.hPow (β := ℕ) I 2)) I.cotangentIdeal = I

Tactic:
Ideal.ext fun _ ↦ mk_mem_cotangentIdeal

Premises used: Ideal.mk_mem_cotangentIdeal, Ideal.ext