awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
⊢ (R ⧸ HPow.hPow (β := ℕ) I 2) ⧸ I.cotangentIdeal ≃+* R ⧸ I
have refine : HasQuotient.Quotient (R ⧸ HPow.hPow (β := ℕ) I 2) (B := Ideal (R ⧸ HPow.hPow (β := ℕ) I 2))
    (map (F := R →+* R ⧸ HPow.hPow (β := ℕ) I 2) (Quotient.mk (HPow.hPow (β := ℕ) I 2)) I) ≃+*
  R ⧸ I
Tactic: refine (Ideal.quotEquivOfEq (Ideal.map_eq_submodule_map _ _).symm).trans ?_
-- 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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
⊢ HasQuotient.Quotient (R ⧸ HPow.hPow (β := ℕ) I 2) (B := Ideal (R ⧸ HPow.hPow (β := ℕ) I 2))
      (map (F := R →+* R ⧸ HPow.hPow (β := ℕ) I 2) (Quotient.mk (HPow.hPow (β := ℕ) I 2)) I) ≃+*
    R ⧸ I
have refine : R ⧸ HPow.hPow (β := ℕ) I 2 ⊔ I ≃+* R ⧸ I
Tactic: refine (DoubleQuot.quotQuotEquivQuotSup _ _).trans ?_
-- 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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ LinearMap.{u, u, u_1, u_2} (RingHom.id R) I₁.Cotangent I₂.Cotangent
have refine_1 : LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥I₁ ↥I₂
Tactic: refine Submodule.mapQ ((I₁ • ⊤ : Submodule A I₁).restrictScalars R)
    ((I₂ • ⊤ : Submodule B I₂).restrictScalars R) ?_ ?_
-- 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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
refine_1 : LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥I₁ ↥I₂
⊢ LinearMap.{u, u, u_1, u_2} (RingHom.id R) I₁.Cotangent I₂.Cotangent
have refine_2 : LE.le (α := Submodule R ↥I₁) (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤))
  (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
    (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)))
Tactic: refine Submodule.mapQ ((I₁ • ⊤ : Submodule A I₁).restrictScalars R)
    ((I₂ • ⊤ : Submodule B I₂).restrictScalars R) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (hypothesis)
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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : Membership.mem (γ := Submodule R ↥I₁) (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤)) x
⊢ Membership.mem (γ := Submodule R ↥I₁)
    (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
        (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)) :
      Submodule R ↥I₁)
    x
have hx₁ : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
Tactic: rw [Submodule.restrictScalars_mem] at hx
Cleared hypotheses: hx
-- 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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
⊢ Membership.mem (γ := Submodule R ↥I₁)
    (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
        (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)) :
      Submodule R ↥I₁)
    x
have refine_2 : ∀ r ∈ I₁,
  ∀ (n : ↥I₁),
    Membership.mem (γ := Submodule A ↥I₁) ⊤ n →
      Membership.mem (γ := Submodule R ↥I₁)
        (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
            (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)) :
          Submodule R ↥I₁)
        (r • n)
Tactic: refine Submodule.smul_induction_on hx ?_ (fun _ _ ↦ add_mem)
-- 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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ Membership.mem (γ := Submodule R ↥I₁)
    (Submodule.comap (σ₁₂ := RingHom.id R) (f.toLinearMap.restrict h)
        (Submodule.restrictScalars R (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)) :
      Submodule R ↥I₁)
    (a • Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) b hb)
have refine_2 : Membership.mem (α := ↥I₂) (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)
  (((f.toLinearMap.restrict h :
          LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
            ↥(Submodule.restrictScalars R I₂)) :
        (a : ↥I₁) → ↥I₂)
      (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) sorry) :
    ↥I₂)
Tactic: simp only [SetLike.mk_smul_mk, smul_eq_mul, Submodule.mem_comap, Submodule.restrictScalars_mem]
-- 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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ Membership.mem (α := ↥I₂) (HSMul.hSMul (β := Submodule B ↥I₂) I₂ ⊤)
    (((f.toLinearMap.restrict h :
            LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
              ↥(Submodule.restrictScalars R I₂)) :
          (a : ↥I₁) → ↥I₂)
        (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯) :
      ↥I₂)
have h₁ : ((f.toLinearMap.restrict h :
        LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁) ↥(Submodule.restrictScalars R I₂)) :
      (a : ↥I₁) → ↥I₂)
    (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) sorry) =
  HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
    (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) sorry : ↥I₂)
Tactic: convert!
      (Submodule.smul_mem_smul (M := I₂) (r := f a) (n := ⟨f b, h hb⟩) (h ha)
        (Submodule.mem_top)) using 1
-- 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
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ HSMul.hSMul (β := Submodule A ↥I₁) I₁ ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ ((f.toLinearMap.restrict h :
          LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
            ↥(Submodule.restrictScalars R I₂)) :
        (a : ↥I₁) → ↥I₂)
      (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) ⋯) =
    HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
      (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) ⋯ : ↥I₂)
have h₁ : (↑(((f.toLinearMap.restrict h :
            LinearMap.{u, u, u_1, u_2} (RingHom.id R) ↥(Submodule.restrictScalars R I₁)
              ↥(Submodule.restrictScalars R I₂)) :
          (a : ↥I₁) → ↥I₂)
        (Subtype.mk (p := fun (x : A) ↦ x ∈ I₁) (a * b) sorry)) :
    B) =
  (↑(HSMul.hSMul (α := B) (β := ↥I₂) ((f : (a : A) → B) a : B)
        (Subtype.mk (p := fun (x : B) ↦ x ∈ I₂) ((f : (a : A) → B) b) sorry : ↥I₂)) :
    B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
S_1 : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S_1
inst_2 : Algebra S_1 R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S_1 S'
inst_6 : IsScalarTower S_1 S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
S : Type u_3
inst_11 : CommRing S
inst_12 : Algebra R S
I : Ideal S
M : Type u_4
inst_13 : AddCommGroup M
inst_14 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
x : ↥I
hx : Membership.mem (γ := AddSubgroup ↥I) (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup x
⊢ Membership.mem (γ := AddSubgroup ↥I) f.toAddMonoidHom.ker x
have simp : ∀ (hx : x ∈ HSMul.hSMul (β := Submodule S ↥I) I ⊤),
  Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) x : M) (0 : M)
Tactic: simp only [Submodule.mem_toAddSubgroup, AddMonoidHom.mem_ker] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
S_1 : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S_1
inst_2 : Algebra S_1 R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S_1 S'
inst_6 : IsScalarTower S_1 S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
S : Type u_3
inst_11 : CommRing S
inst_12 : Algebra R S
I : Ideal S
M : Type u_4
inst_13 : AddCommGroup M
inst_14 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
x : ↥I
hx : x ∈ HSMul.hSMul (β := Submodule S ↥I) I ⊤
⊢ Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) x : M) (0 : M)
have refine : ∀ (x y : ↥I) (hx : Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) x : M) (0 : M))
  (hy : Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) y : M) (0 : M)),
  Eq.{u_4 + 1} (α := M) ((f.toAddMonoidHom : (a : ↥I) → M) (x + y) : M) (0 : M)
Tactic: refine Submodule.smul_induction_on hx (fun r hr y _ ↦ hf ⟨r, hr⟩ y) fun x y hx hy ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
S_1 : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S_1
inst_2 : Algebra S_1 R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S_1 S'
inst_6 : IsScalarTower S_1 S' R
I_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
S : Type u_3
inst_11 : CommRing S
inst_12 : Algebra R S
I : Ideal S
M : Type u_4
inst_13 : AddCommGroup M
inst_14 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
r : R
x : I.Cotangent
⊢ ZeroHom.toFun
      (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
        ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
      (r • x) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R)
      (ZeroHom.toFun
        (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom ⋯) :
          ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
        x)
have obtain : ∀ (x : ↥I),
  ZeroHom.toFun
      (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom sorry) :
        ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
      (HSMul.hSMul (β := I.Cotangent) r ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) r : R)
      (ZeroHom.toFun.{u_3, u_4} (M :=
        HasQuotient.Quotient ↥I (B := AddSubgroup ↥I) (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup)
        (↑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom sorry) :
          ZeroHom (↥I ⧸ (I • ⊤).toAddSubgroup) M)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) x))
Tactic: obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M) ↔
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
have refine_1 : ∀ (h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)),
  Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
refine_1 :
  ∀ (h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)),
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M) ↔
    Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
have refine_2 : ∀ (h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)),
  Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
have refine_1 : Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M)
  (Function.comp (β := I.Cotangent) (⇑(lift f hf) : (a : I.Cotangent) → M)
    (⇑((↑R :
            {S M M₂ : Type u_3} →
              [inst : Semiring R] →
                [inst_5 : Semiring S] →
                  [inst_6 : AddCommMonoid M] →
                    [inst_7 : AddCommMonoid M₂] →
                      [inst_8 : Module R M] →
                        [inst_9 : Module R M₂] →
                          [inst_10 : Module S M] →
                            [inst_11 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          I.toCotangent) :
      (a : ↥I) → I.Cotangent))
Tactic: rw [← Cotangent.lift_comp_toCotangent f hf, LinearMap.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
f : LinearMap.{u, u, u_3, u_4} (RingHom.id R) (↥I) M
hf : ∀ (x y : ↥I), Eq.{u_4 + 1} (α := M) ((f : (a : ↥I) → M) (x * y) : M) (0 : M)
h : Function.Surjective.{u_3 + 1, u_4 + 1} (α := ↥I) (β := M) (⇑f : (a : ↥I) → M)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M) (⇑(lift f hf) : (a : I.Cotangent) → M)
have refine_2 : Function.Surjective.{u_3 + 1, u_4 + 1} (α := I.Cotangent) (β := M)
  (⇑(QuotientAddGroup.lift (HSMul.hSMul (β := Submodule S ↥I) I ⊤).toAddSubgroup f.toAddMonoidHom sorry) :
    (a : ↥I ⧸ (I • ⊤).toAddSubgroup) → M)
Tactic: dsimp [Cotangent.lift]
-- 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_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I J : Ideal R
hIJ : I = J
x : I.Cotangent
⊢ (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq J I ⋯) : ↥J →ₗ[R] ↥I)) ⋯ : (a : J.Cotangent) → I.Cotangent)
      ((lift (J.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I J hIJ) : ↥I →ₗ[R] ↥J)) ⋯).toFun x) =
    x
have subst : (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I sorry) : ↥I →ₗ[R] ↥I)) sorry : (a : I.Cotangent) → I.Cotangent)
    ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I sorry) : ↥I →ₗ[R] ↥I)) sorry).toFun x) =
  x
Tactic: subst hIJ
Cleared hypotheses: J, hIJ
-- 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_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I : Ideal R
x : I.Cotangent
__spread.0 : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯
⊢ (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent)
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun x) =
    x
have obtain : ∀ (x : ↥I),
  Eq (α := I.Cotangent)
    ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I sorry) : ↥I →ₗ[R] ↥I)) sorry : (a : I.Cotangent) → I.Cotangent)
        ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I sorry) : ↥I →ₗ[R] ↥I)) sorry).toFun
          ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
      I.Cotangent)
    ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)
Tactic: obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
Cleared hypotheses: x
-- 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_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I J : Ideal R
hIJ : I = J
x : J.Cotangent
⊢ (lift (J.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I J hIJ) : ↥I →ₗ[R] ↥J)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq J I ⋯) : ↥J →ₗ[R] ↥I)) ⋯ : (a : J.Cotangent) → I.Cotangent) x) =
    x
have subst : ∀ (x : I.Cotangent),
  (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I sorry) : ↥I →ₗ[R] ↥I)) sorry).toFun
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I sorry) : ↥I →ₗ[R] ↥I)) sorry : (a : I.Cotangent) → I.Cotangent) x) =
    x
Tactic: subst hIJ
Cleared hypotheses: J, hIJ, x
-- 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_1 : Ideal R
A : Type u_1
B : Type u_2
inst_7 : CommRing A
inst_8 : CommRing B
inst_9 : Algebra R A
inst_10 : Algebra R B
I : Ideal R
__spread.0 : I.Cotangent →ₗ[R] I.Cotangent := lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯
x : I.Cotangent
⊢ (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I ⋯) : ↥I →ₗ[R] ↥I)) ⋯ : (a : I.Cotangent) → I.Cotangent) x) =
    x
have obtain : ∀ (x : ↥I),
  (lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I sorry) : ↥I →ₗ[R] ↥I)) sorry).toFun
      ((lift (I.toCotangent ∘ₗ (↑(LinearEquiv.ofEq I I sorry) : ↥I →ₗ[R] ↥I)) sorry : (a : I.Cotangent) → I.Cotangent)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) =
    (I.toCotangent : (a : ↥I) → I.Cotangent) x
Tactic: obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ Subsingleton.{u_1 + 1} (CotangentSpace R) ↔ IsField R
have refine : IsIdempotentElem (M := Ideal R) (maximalIdeal R) ↔ IsField R
Tactic: refine (maximalIdeal R).cotangent_subsingleton_iff.trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ IsIdempotentElem (M := Ideal R) (maximalIdeal R) ↔ IsField R
have rw : Eq (α := Ideal R) (maximalIdeal R) ⊥ ∨ Eq (α := Ideal R) (maximalIdeal R) ⊤ ↔ Eq (α := Ideal R) (maximalIdeal R) ⊥
Tactic: rw [IsLocalRing.isField_iff_maximalIdeal_eq,
    Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
⊢ Submodule.map (Ideal.toCotangent (maximalIdeal R)) M = ⊤ ↔ M = ⊤
have refine : ∀ (H : Submodule.map (Ideal.toCotangent (maximalIdeal R)) M = ⊤), ⊤ ≤ M
Tactic: refine ⟨fun H ↦ eq_top_iff.mpr ?_, by rintro rfl; simp [Ideal.toCotangent_range]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (Ideal.toCotangent (maximalIdeal R)) M = ⊤
⊢ ⊤ ≤ M
have refine : Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)) ⊤ ≤
  Submodule.map (Submodule.subtype (maximalIdeal R)) M
Tactic: refine (Submodule.map_le_map_iff_of_injective (Submodule.injective_subtype _) _ _).mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
H : Submodule.map (Ideal.toCotangent (maximalIdeal R)) M = ⊤
⊢ Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)) ⊤ ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M
have rw : maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M
Tactic: rw [Submodule.map_top, Submodule.range_subtype]