awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = ⊤
⊢ maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M
have apply : maximalIdeal R ≤
  Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
    HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
Tactic: apply Submodule.le_of_le_smul_of_le_jacobson_bot (IsNoetherian.noetherian _)
    (IsLocalRing.jacobson_eq_maximalIdeal _ bot_ne_top).ge
-- 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 = ⊤
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw : maximalIdeal R ≤
  Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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 = ⊤
rw :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw₁ : maximalIdeal R ≤
  Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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 = ⊤
rw :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
rw₁ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw₂ : maximalIdeal R ≤
  Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
    Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
      (LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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 = ⊤
rw :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
rw₁ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2
rw₂ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
        (LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw₃ : maximalIdeal R ≤
  Submodule.map (Submodule.subtype (maximalIdeal R)) (M ⊔ LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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 = ⊤
rw :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
rw₁ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2
rw₂ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
        (LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₃ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) (M ⊔ LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw₄ : maximalIdeal R ≤
  Submodule.map (Submodule.subtype (maximalIdeal R))
    (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) (Submodule.map (Ideal.toCotangent (maximalIdeal R)) M))
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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 = ⊤
rw :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
rw₁ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2
rw₂ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
        (LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₃ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) (M ⊔ LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₄ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R))
      (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) (Submodule.map (Ideal.toCotangent (maximalIdeal R)) M))
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw₅ : LE.le (α := Submodule R R) (maximalIdeal R)
  (Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
    (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) ⊤))
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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 = ⊤
rw :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
rw₁ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2
rw₂ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
        (LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₃ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) (M ⊔ LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₄ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R))
      (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) (Submodule.map (Ideal.toCotangent (maximalIdeal R)) M))
rw₅ :
  LE.le (α := Submodule R R) (maximalIdeal R)
    (Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
      (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) ⊤))
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw₆ : LE.le (α := Submodule R R) (maximalIdeal R)
  (Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)) ⊤)
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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 = ⊤
rw :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
rw₁ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2
rw₂ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
        (LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₃ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) (M ⊔ LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₄ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R))
      (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) (Submodule.map (Ideal.toCotangent (maximalIdeal R)) M))
rw₅ :
  LE.le (α := Submodule R R) (maximalIdeal R)
    (Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
      (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) ⊤))
rw₆ :
  LE.le (α := Submodule R R) (maximalIdeal R)
    (Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)) ⊤)
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw₇ : LE.le (α := Submodule R R) (maximalIdeal R)
  (LinearMap.range (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)))
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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 = ⊤
rw :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
rw₁ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2
rw₂ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
        (LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₃ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) (M ⊔ LinearMap.ker (Ideal.toCotangent (maximalIdeal R)))
rw₄ :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R))
      (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) (Submodule.map (Ideal.toCotangent (maximalIdeal R)) M))
rw₅ :
  LE.le (α := Submodule R R) (maximalIdeal R)
    (Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R))
      (Submodule.comap (Ideal.toCotangent (maximalIdeal R)) ⊤))
rw₆ :
  LE.le (α := Submodule R R) (maximalIdeal R)
    (Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)) ⊤)
rw₇ :
  LE.le (α := Submodule R R) (maximalIdeal R)
    (LinearMap.range (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)))
⊢ maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
have rw₈ : LE.le (α := Submodule R R) (maximalIdeal R) (maximalIdeal R)
Tactic: rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
-- 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
s : Set ↥(maximalIdeal R)
⊢ Eq (α := Submodule (ResidueField R) (Ideal.Cotangent (maximalIdeal R)))
      (Submodule.span (ResidueField R)
        ((⇑(Ideal.toCotangent (maximalIdeal R)) : (a : ↥(maximalIdeal R)) → (maximalIdeal R).Cotangent) '' s))
      ⊤ ↔
    Eq (α := Submodule R ↥(maximalIdeal R)) (Submodule.span R s) ⊤
have rw : Eq (α := Submodule R (Ideal.Cotangent (maximalIdeal R)))
    (Submodule.span R
      ((⇑(Ideal.toCotangent (maximalIdeal R)) : (a : ↥(maximalIdeal R)) → (maximalIdeal R).Cotangent) '' s))
    (Submodule.restrictScalars R (R := ResidueField R) ⊤) ↔
  Submodule.map (Ideal.toCotangent (maximalIdeal R)) (Submodule.span R s) = ⊤
Tactic: rw [← map_eq_top_iff, ← (Submodule.restrictScalars_injective R ..).eq_iff,
    Submodule.restrictScalars_span]
-- 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
s : Set ↥(maximalIdeal R)
rw :
  Eq (α := Submodule R (Ideal.Cotangent (maximalIdeal R)))
      (Submodule.span R
        ((⇑(Ideal.toCotangent (maximalIdeal R)) : (a : ↥(maximalIdeal R)) → (maximalIdeal R).Cotangent) '' s))
      (Submodule.restrictScalars R (R := ResidueField R) ⊤) ↔
    Submodule.map (Ideal.toCotangent (maximalIdeal R)) (Submodule.span R s) = ⊤
⊢ Eq (α := Submodule (ResidueField R) (Ideal.Cotangent (maximalIdeal R)))
      (Submodule.span (ResidueField R)
        ((⇑(Ideal.toCotangent (maximalIdeal R)) : (a : ↥(maximalIdeal R)) → (maximalIdeal R).Cotangent) '' s))
      ⊤ ↔
    Eq (α := Submodule R ↥(maximalIdeal R)) (Submodule.span R s) ⊤
have hsur : Function.Surjective (α := R) (β := ResidueField R) (⇑(algebraMap R (ResidueField R)) : (a : R) → ResidueField R)
Tactic: rw [← map_eq_top_iff, ← (Submodule.restrictScalars_injective R ..).eq_iff,
    Submodule.restrictScalars_span]
-- 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
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R
have rw : Subsingleton.{u_1 + 1} (CotangentSpace R) ↔ IsField R
Tactic: rw [finrank_zero_iff, subsingleton_cotangentSpace_iff]
-- 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
rw : Subsingleton.{u_1 + 1} (CotangentSpace R) ↔ IsField R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R
have rw₁ : IsField R ↔ IsField R
Tactic: rw [finrank_zero_iff, subsingleton_cotangentSpace_iff]
-- 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
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
have rw : (∃ (x : ↥(maximalIdeal R)),
    Eq (α := Submodule (ResidueField R) (CotangentSpace R)) ⊤
      (span (ResidueField R)
        (singleton (α := CotangentSpace R)
          ((Ideal.toCotangent (maximalIdeal R) : (a : ↥(maximalIdeal R)) → (maximalIdeal R).Cotangent) x :
            Ideal.Cotangent (maximalIdeal R))))) ↔
  ∃ (a : R), Eq (α := Submodule R R) (maximalIdeal R) (R ∙ a)
Tactic: rw [Module.finrank_le_one_iff_top_isPrincipal, isPrincipal_iff,
    (maximalIdeal R).toCotangent_surjective.exists, isPrincipal_iff]
-- 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
⊢ (∃ (x : ↥(maximalIdeal R)),
      Eq (α := Submodule (ResidueField R) (CotangentSpace R)) ⊤
        (span (ResidueField R)
          (singleton (α := CotangentSpace R)
            ((Ideal.toCotangent (maximalIdeal R) : (a : ↥(maximalIdeal R)) → (maximalIdeal R).Cotangent) x :
              Ideal.Cotangent (maximalIdeal R))))) ↔
    ∃ (a : R), Eq (α := Submodule R R) (maximalIdeal R) (R ∙ a)
have simp_rw : (∃ (x : ↥(maximalIdeal R)),
    Eq (α := Submodule R R)
      (span R (singleton (α := R) ((Submodule.subtype (maximalIdeal R) : (a : ↥(maximalIdeal R)) → R) x : R)))
      (maximalIdeal R)) ↔
  ∃ (a : R), Eq (α := Ideal R) (R ∙ a) (maximalIdeal R)
Tactic: simp_rw [← Set.image_singleton, eq_comm (a := ⊤), CotangentSpace.span_image_eq_top_iff,
    ← (map_injective_of_injective (injective_subtype _)).eq_iff, map_span, Set.image_singleton,
    Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
x : I.Cotangent
⊢ ∃ (a : J.Cotangent), (J.mapCotangent I (Algebra.ofId A B) ⋯ : (a : J.Cotangent) → I.Cotangent) a = x
have rcases : ∀ (x' : ↥I),
  ∃ (a : J.Cotangent),
    Eq.{u_2 + 1} (α := I.Cotangent)
      ((J.mapCotangent I (Algebra.ofId A B) sorry : (a : J.Cotangent) → I.Cotangent) a : I.Cotangent)
      ((I.toCotangent : (a : ↥I) → I.Cotangent) x' : I.Cotangent)
Tactic: rcases I.toCotangent_surjective x with ⟨x', rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
x' : ↥I
⊢ ∃ (a : J.Cotangent),
    Eq.{u_2 + 1} (α := I.Cotangent)
      ((J.mapCotangent I (Algebra.ofId A B) ⋯ : (a : J.Cotangent) → I.Cotangent) a : I.Cotangent)
      ((I.toCotangent : (a : ↥I) → I.Cotangent) x' : I.Cotangent)
have rcases : ∀ (y' : A) (mem : y' ∈ J) (hy' : ((algebraMap A B : A →+* B) : (a : A) → B) y' = (↑x' : B)),
  ∃ (a : J.Cotangent),
    Eq.{u_2 + 1} (α := I.Cotangent)
      ((J.mapCotangent I (Algebra.ofId A B) sorry : (a : J.Cotangent) → I.Cotangent) a : I.Cotangent)
      ((I.toCotangent : (a : ↥I) → I.Cotangent) x' : I.Cotangent)
Tactic: rcases Ideal.exists_of_comap_eq_ker_sup _ surj eq x'.2 with ⟨y', mem, hy'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
x' : ↥I
y' : A
mem : y' ∈ J
hy' : ((algebraMap A B : A →+* B) : (a : A) → B) y' = (↑x' : B)
⊢ ∃ (a : J.Cotangent),
    Eq.{u_2 + 1} (α := I.Cotangent)
      ((J.mapCotangent I (Algebra.ofId A B) ⋯ : (a : J.Cotangent) → I.Cotangent) a : I.Cotangent)
      ((I.toCotangent : (a : ↥I) → I.Cotangent) x' : I.Cotangent)
have h : Eq.{u_2 + 1} (α := I.Cotangent)
  ((J.mapCotangent I (Algebra.ofId A B) sorry : (a : J.Cotangent) → I.Cotangent)
      ((J.toCotangent : (a : ↥J) → J.Cotangent) (Subtype.mk (p := fun (x : A) ↦ x ∈ J) y' mem)) :
    I.Cotangent)
  ((I.toCotangent : (a : ↥I) → I.Cotangent) x' : I.Cotangent)
Tactic: use J.toCotangent ⟨y', mem⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
⊢ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker =
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have eqmap : I = map (F := A →+* B) (algebraMap A B) J
Tactic: have eqmap := Ideal.eq_map_of_comap_eq_ker_sup _ surj eq
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
⊢ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker =
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have refine_1 : ∀ (x : J.Cotangent) (hx : x ∈ (J.mapCotangent I (Algebra.ofId A B) sorry).ker),
  x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
Tactic: refine le_antisymm (fun x hx ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
refine_1 :
  ∀ (x : J.Cotangent) (hx : x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker),
    x ∈
      Submodule.map J.toCotangent
        (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
⊢ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker =
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have refine_2 : Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J)) ≤
  (J.mapCotangent I (Algebra.ofId A B) sorry).ker
Tactic: refine le_antisymm (fun x hx ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Cotangent (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap (F := A →+* B) (algebraMap A B) I = RingHom.ker (F := A →+* B) (algebraMap A B) ⊔ J
eqmap : I = map (F := A →+* B) (algebraMap A B) J
x : J.Cotangent
hx : x ∈ (J.mapCotangent I (Algebra.ofId A B) ⋯).ker
⊢ x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
have refine_1 : ∀ (x' : ↥J) (hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x),
  x ∈
    Submodule.map J.toCotangent
      (Submodule.comap (Submodule.subtype J) (RingHom.ker (F := A →+* B) (algebraMap A B) ⊓ J))
Tactic: rcases J.toCotangent_surjective x with ⟨x', hx'⟩