awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N N₁ N₂ : Submodule R M
S S₁ S₂ : Set M
P : Submodule R M
r s : R
hr : r ∈ N.colon (↑P : Set M)
p : M
hp : p ∈ (r * s) • (↑P : Set M)
⊢ p ∈ (↑N : Set M)
have obtain : ∀ (p : M) (hp : p ∈ (↑P : Set M)), (fun (x : M) ↦ (r * s) • x) p ∈ (↑N : Set M)
Tactic: obtain ⟨p, hp, rfl⟩ := hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
Goal:
R : Type u_1
inst : Semiring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ colon I Set.univ = I
have simp_rw : ∀ (x : R), (∀ (s : R), Membership.mem (γ := Set R) Set.univ s → x * s ∈ I) ↔ x ∈ I
Tactic: simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ colon ⊥ (↑N : Set M) = N.annihilator
have h : ∀ (x : R), Membership.mem (γ := Ideal R) (colon ⊥ (↑N : Set M)) x ↔ x ∈ N.annihilator
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ N.colon (↑(span R S) : Set M) = N.colon S
have refine : ∀ (r : R) (h : r ∈ N.colon S) (s : M) (hs : s ∈ (↑(span R S) : Set M)), r • s ∈ N
Tactic: refine (colon_mono le_rfl subset_span).antisymm fun r h ↦ mem_colon.mpr fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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)
⊢ r • s ∈ N
have mem : ∀ x ∈ S, r • x ∈ 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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ r • s ∈ N
have zero : HSMul.hSMul (β := M) r 0 ∈ 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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ r • s ∈ N
have 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
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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ r • s ∈ N
have smul : ∀ (a : R) (x : M), Membership.mem (γ := Submodule R M) (span R S) x → r • x ∈ N → r • a • x ∈ 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]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ (map N.mkQ P).annihilator = N.colon (↑P : Set M)
have h : ∀ (x : R), x ∈ (map N.mkQ P).annihilator ↔ x ∈ N.colon (↑P : Set M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ x ∈ (map N.mkQ P).annihilator ↔ x ∈ N.colon (↑P : Set M)
have h : (∀ n ∈ map N.mkQ P, x • n = 0) ↔ ∀ s ∈ (↑P : Set M), x • s ∈ N
Tactic: rw [mem_annihilator, mem_colon]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ Module.annihilator.{u_1, u_2} R (M ⧸ N) = N.colon Set.univ
have h : ∀ (r : R), Membership.mem (γ := Ideal R) (Module.annihilator.{u_1, u_2} R (M ⧸ N)) r ↔ r ∈ N.colon Set.univ
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (hypothesis)
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
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_1, u_2} R (M ⧸ N)) r ↔ r ∈ N.colon Set.univ
have htop : ⊤ = 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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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 ⊤
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_1, u_2} R (M ⧸ N)) r ↔ r ∈ N.colon Set.univ
have h : Membership.mem (γ := Ideal R) (annihilator.{u_1, u_2} (M := 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_1, u_2} R (M ⧸ N)) r ↔ r ∈ N.colon Set.univ
have h₁ : r ∈ (map N.mkQ ⊤).annihilator ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_1, u_2} R (M ⧸ N)) r ↔ r ∈ N.colon Set.univ
have h₂ : r ∈ N.colon (↑⊤ : Set M) ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
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
⊢ Membership.mem (γ := Ideal R) (Module.annihilator.{u_1, u_2} R (M ⧸ N)) r ↔ r ∈ N.colon Set.univ
have h₃ : r ∈ N.colon Set.univ ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ Module.annihilator R (R ⧸ I) = I
have rw : colon I Set.univ = I
Tactic: rw [Submodule.annihilator_quotient, colon_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
rw : colon I Set.univ = I
⊢ Module.annihilator R (R ⧸ I) = I
have rw₁ : I = I
Tactic: rw [Submodule.annihilator_quotient, colon_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.subtype I) I.toCotangent.ker = HPow.hPow (β := ℕ) I 2
have 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
Tactic: rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
    smul_eq_mul, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ Submodule.map (Submodule.subtype I) I.toCotangent.ker = HPow.hPow (β := ℕ) I 2
have rw₁ : Submodule.map (Submodule.subtype I) (HSMul.hSMul (β := Submodule R ↥I) I ⊤) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ Submodule.map (Submodule.subtype I) I.toCotangent.ker = HPow.hPow (β := ℕ) I 2
have rw₂ : Submodule.map (Submodule.subtype I) (HSMul.hSMul (β := Submodule R ↥I) I ⊤) = I * I
Tactic: rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
    smul_eq_mul, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ Submodule.map (Submodule.subtype I) I.toCotangent.ker = HPow.hPow (β := ℕ) I 2
have rw₃ : I • Submodule.map (Submodule.subtype I) ⊤ = I * I
Tactic: rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
    smul_eq_mul, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ Submodule.map (Submodule.subtype I) I.toCotangent.ker = HPow.hPow (β := ℕ) I 2
have rw₄ : I * Submodule.map (Submodule.subtype I) ⊤ = I * I
Tactic: rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
    smul_eq_mul, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ Submodule.map (Submodule.subtype I) I.toCotangent.ker = HPow.hPow (β := ℕ) I 2
have rw₅ : I * I = I * I
Tactic: rw [Ideal.toCotangent, Submodule.ker_mkQ, pow_two, Submodule.map_smul'' I ⊤ (Submodule.subtype I),
    smul_eq_mul, Submodule.map_subtype_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : ↥I
⊢ x ∈ I.toCotangent.ker ↔ (↑x : R) ∈ HPow.hPow (β := ℕ) I 2
have rw : x ∈ I.toCotangent.ker ↔ (↑x : R) ∈ Submodule.map (Submodule.subtype I) I.toCotangent.ker
Tactic: rw [← I.map_toCotangent_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x y : ↥I
⊢ 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
have 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
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ Subsingleton.{u + 1} I.Cotangent ↔ IsIdempotentElem I
have mp : Subsingleton.{u + 1} I.Cotangent → IsIdempotentElem I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
mp : Subsingleton.{u + 1} I.Cotangent → IsIdempotentElem I
⊢ Subsingleton.{u + 1} I.Cotangent ↔ IsIdempotentElem I
have mpr : IsIdempotentElem I → Subsingleton.{u + 1} I.Cotangent
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
H : Subsingleton.{u + 1} I.Cotangent
⊢ IsIdempotentElem I
have mp : I ≤ HPow.hPow (β := ℕ) I 2
Tactic: refine (pow_two I).symm.trans (le_antisymm (Ideal.pow_le_self two_ne_zero) ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ HSMul.hSMul (β := Submodule R ↥I) I ⊤ ≤ Submodule.comap (Submodule.subtype I) (HPow.hPow (β := ℕ) I 2)
have rw : Submodule.map (Submodule.subtype I) (HSMul.hSMul (β := Submodule R ↥I) 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ HSMul.hSMul (β := Submodule R ↥I) I ⊤ ≤ Submodule.comap (Submodule.subtype I) (HPow.hPow (β := ℕ) I 2)
have rw₁ : I • Submodule.map (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ HSMul.hSMul (β := Submodule R ↥I) I ⊤ ≤ Submodule.comap (Submodule.subtype I) (HPow.hPow (β := ℕ) I 2)
have rw₂ : I • (Submodule.subtype I).range ≤ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ HSMul.hSMul (β := Submodule R ↥I) I ⊤ ≤ Submodule.comap (Submodule.subtype I) (HPow.hPow (β := ℕ) I 2)
have rw₃ : I • 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ HSMul.hSMul (β := Submodule R ↥I) I ⊤ ≤ Submodule.comap (Submodule.subtype I) (HPow.hPow (β := ℕ) I 2)
have rw₄ : I * 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ HSMul.hSMul (β := Submodule R ↥I) I ⊤ ≤ Submodule.comap (Submodule.subtype I) (HPow.hPow (β := ℕ) I 2)
have rw₅ : I * I ≤ I * I
Tactic: rw [← Submodule.map_le_iff_le_comap, Submodule.map_smul'', Submodule.map_top,
        Submodule.range_subtype, smul_eq_mul, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ Function.Injective (α := I.Cotangent) (β := R ⧸ HPow.hPow (β := ℕ) I 2)
    (⇑I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2)
have 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
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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)
⊢ x = 0
have 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)
Tactic: obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (hypothesis)
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 (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent) (0 : I.Cotangent)
have 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)
Tactic: rw [toCotangent_to_quotient_square] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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)
⊢ Eq (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent) (0 : I.Cotangent)
have rwa : (↑x : R) ∈ HPow.hPow (β := ℕ) I 2
Tactic: rwa [Ideal.toCotangent_eq_zero, ← Submodule.Quotient.mk_eq_zero (I ^ 2)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
⊢ Eq (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent) (0 : I.Cotangent)
have rwa₁ : Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2) (Submodule.Quotient.mk (↑x : R)) 0
Tactic: rwa [Ideal.toCotangent_eq_zero, ← Submodule.Quotient.mk_eq_zero (I ^ 2)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : I.Cotangent
⊢ x • m = 0
have obtain : ∀ (m : ↥I), HSMul.hSMul (β := I.Cotangent) x ((I.toCotangent : (a : ↥I) → I.Cotangent) m : I.Cotangent) = 0
Tactic: obtain ⟨m, rfl⟩ := Ideal.toCotangent_surjective _ m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
hx : x ∈ I
m : ↥I
⊢ HSMul.hSMul (β := I.Cotangent) x ((I.toCotangent : (a : ↥I) → I.Cotangent) m : I.Cotangent) = 0
have rw : (↑(x • m) : R) ∈ I * I
Tactic: rw [← map_smul, Ideal.toCotangent_eq_zero, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ HPow.hPow (β := ℕ) I.cotangentIdeal 2 = ⊥
have rw : I.cotangentIdeal • I.cotangentIdeal ≤ ⊥
Tactic: rw [eq_bot_iff, pow_two I.cotangentIdeal, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
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
have refine_1 : ∀ r ∈ I.cotangentIdeal,
  ∀ n ∈ I.cotangentIdeal,
    Membership.mem (γ := Submodule (R ⧸ HPow.hPow (β := ℕ) I 2) (R ⧸ HPow.hPow (β := ℕ) I 2)) ⊥ (r • n)
Tactic: refine Submodule.smul_induction_on hx ?_ ?_