awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
hIJ : I = J
⊢ (equivOfEq I J hIJ).symm = equivOfEq J I ⋯

Tactic:
rfl

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, Ideal.Cotangent.equivOfEq, Ideal.Cotangent, Submodule.quotientRel, AddAction.orbitRel, AddCon.Quotient, Ideal.Cotangent.lift, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ IsScalarTower R (ResidueField R) (CotangentSpace R)

Tactic:
inferInstanceAs <| IsScalarTower R (R ⧸ maximalIdeal R) _

Premises used: _private.0.IsLocalRing.instIsScalarTowerResidueFieldCotangentSpace._proof_1
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ FiniteDimensional.{u_1, u_1} (ResidueField R) (CotangentSpace R)

Tactic:
Module.Finite.of_restrictScalars_finite R _ _

Premises used: Module.Finite.of_restrictScalars_finite
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ Subsingleton.{u_1 + 1} (CotangentSpace R) ↔ IsField R

Tactic:
(maximalIdeal R).cotangent_subsingleton_iff.trans ?_

Premises used: IsLocalRing.maximalIdeal, Iff.trans, Ideal.cotangent_subsingleton_iff
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
refine : IsIdempotentElem (M := Ideal R) (maximalIdeal R) ↔ IsField R
⊢ Subsingleton.{u_1 + 1} (CotangentSpace R) ↔ IsField R

Tactic:
refine (maximalIdeal R).cotangent_subsingleton_iff.trans ?_

Premises used: IsLocalRing.maximalIdeal, Iff.trans, Ideal.cotangent_subsingleton_iff
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
rw : Eq (α := Ideal R) (maximalIdeal R) ⊥ ∨ Eq (α := Ideal R) (maximalIdeal R) ⊤ ↔ Eq (α := Ideal R) (maximalIdeal R) ⊥
⊢ IsIdempotentElem (M := Ideal R) (maximalIdeal R) ↔ IsField R

Tactic:
rw [IsLocalRing.isField_iff_maximalIdeal_eq,
    Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing]

Premises used: IsLocalRing.isField_iff_maximalIdeal_eq, Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥ ∨ Eq (α := Ideal R) (maximalIdeal R) ⊤ ↔ Eq (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
simp [(maximalIdeal.isMaximal R).ne_top]

Premises used: IsLocalRing.maximalIdeal.isMaximal, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ Eq (α := Submodule R (Ideal.Cotangent (maximalIdeal R))) (Submodule.map (Ideal.toCotangent (maximalIdeal R)) ⊤) ⊤

Tactic:
simp [Ideal.toCotangent_range]

Premises used: Ideal.toCotangent_range
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
M : Submodule R ↥(maximalIdeal R)
refine : ∀ (H : Submodule.map (Ideal.toCotangent (maximalIdeal R)) M = ⊤), ⊤ ≤ M
⊢ Submodule.map (Ideal.toCotangent (maximalIdeal R)) M = ⊤ ↔ M = ⊤

Tactic:
refine ⟨fun H ↦ eq_top_iff.mpr ?_, by rintro rfl; simp [Ideal.toCotangent_range]⟩
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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

Tactic:
(Submodule.map_le_map_iff_of_injective (Submodule.injective_subtype _) _ _).mp ?_

Premises used: Set.Mem, Submodule.map_le_map_iff_of_injective, Submodule.injective_subtype, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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 = ⊤
refine :
  Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)) ⊤ ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M
⊢ ⊤ ≤ M

Tactic:
refine (Submodule.map_le_map_iff_of_injective (Submodule.injective_subtype _) _ _).mp ?_

Premises used: Submodule.map_le_map_iff_of_injective, Submodule.injective_subtype, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
⊢ Submodule.map (M := ↥(maximalIdeal R)) (Submodule.subtype (maximalIdeal R)) ⊤ ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M

Tactic:
rw [Submodule.map_top, Submodule.range_subtype]

Premises used: Submodule.map_top, Submodule.range_subtype
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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 = ⊤
apply :
  maximalIdeal R ≤
    Submodule.map (Submodule.subtype (maximalIdeal R)) M ⊔
      HSMul.hSMul (α := Ideal R) (β := Submodule R R) (maximalIdeal R) (maximalIdeal R)
⊢ maximalIdeal R ≤ Submodule.map (Submodule.subtype (maximalIdeal R)) M

Tactic:
apply Submodule.le_of_le_smul_of_le_jacobson_bot (IsNoetherian.noetherian _)
    (IsLocalRing.jacobson_eq_maximalIdeal _ bot_ne_top).ge

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot, Eq.ge, IsNoetherian.noetherian, bot_ne_top, IsLocalRing.jacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)))
rw₈ rw₉ : LE.le (α := Submodule R 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)

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]

Premises used: pow_two, Submodule.map_top, Submodule.map_sup, smul_eq_mul, Submodule.range_subtype, Ideal.map_toCotangent_ker, Submodule.comap_top, Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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) = ⊤
hsur : Function.Surjective (α := R) (β := ResidueField R) (⇑(algebraMap R (ResidueField R)) : (a : R) → ResidueField 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) ⊤

Tactic:
rw [← map_eq_top_iff, ← (Submodule.restrictScalars_injective R ..).eq_iff,
    Submodule.restrictScalars_span]

Premises used: Function.Injective.eq_iff, Submodule.restrictScalars_injective, IsLocalRing.CotangentSpace.map_eq_top_iff, Submodule.restrictScalars_span
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Function.Surjective (α := R) (β := ResidueField R) (⇑(algebraMap R (ResidueField R)) : (a : R) → ResidueField R)

Tactic:
Ideal.Quotient.mk_surjective

Premises used: Submodule.Quotient.mk, Ideal.Quotient.mk_surjective, IsLocalRing.ResidueField
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Function.Surjective (α := R) (β := ResidueField R) (⇑(algebraMap R (ResidueField R)) : (a : R) → ResidueField R)

Tactic:
exact Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
rw₁ rw₂ : IsField R ↔ IsField R
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R

Tactic:
rw [finrank_zero_iff, subsingleton_cotangentSpace_iff]

Premises used: IsLocalRing.subsingleton_cotangentSpace_iff, Module.finrank_zero_iff
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_2
inst : Field R
⊢ finrank.{u_2, u_2} (ResidueField R) (CotangentSpace R) = 0

Tactic:
finrank_cotangentSpace_eq_zero_iff.mpr (Field.toIsField R)

Premises used: Iff.mpr, IsLocalRing.finrank_cotangentSpace_eq_zero_iff, Field.toIsField
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
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)
⊢ finrank.{u_1, u_1} (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
rw [Module.finrank_le_one_iff_top_isPrincipal, isPrincipal_iff,
    (maximalIdeal R).toCotangent_surjective.exists, isPrincipal_iff]

Premises used: Function.Surjective.exists, IsLocalRing.maximalIdeal, Submodule.isPrincipal_iff, Ideal.toCotangent_surjective, Module.finrank_le_one_iff_top_isPrincipal
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
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)
⊢ (∃ (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:
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)]

Premises used: Set.image_singleton, Submodule.map_top, Function.Injective.eq_iff, eq_comm, Submodule.injective_subtype, IsLocalRing.CotangentSpace.span_image_eq_top_iff, Submodule.map_span, Submodule.range_subtype, Submodule.map_injective_of_injective
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ (∃ (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:
⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩

Premises used: Set.mem_singleton, _private.0.IsLocalRing.finrank_cotangentSpace_le_one_iff.match_3, IsLocalRing.maximalIdeal, Exists, Eq.rec, Subtype.mk, _private.0.IsLocalRing.finrank_cotangentSpace_le_one_iff.match_2, Iff.intro, Exists.intro, Submodule.span, Submodule.subtype, Submodule.subset_span, Singleton.singleton, Eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ (∃ (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:
exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
rcases :
  ∀ (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)
⊢ ∃ (a : J.Cotangent), (J.mapCotangent I (Algebra.ofId A B) ⋯ : (a : J.Cotangent) → I.Cotangent) a = x

Tactic:
rcases I.toCotangent_surjective x with ⟨x', rfl⟩

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
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) ⋯ : (a : J.Cotangent) → I.Cotangent) a : I.Cotangent)
        ((I.toCotangent : (a : ↥I) → I.Cotangent) x' : I.Cotangent)
⊢ ∃ (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)

Tactic:
rcases Ideal.exists_of_comap_eq_ker_sup _ surj eq x'.2 with ⟨y', mem, hy'⟩

Premises used: Ideal.exists_of_comap_eq_ker_sup, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
h :
  Eq.{u_2 + 1} (α := I.Cotangent)
    ((J.mapCotangent I (Algebra.ofId A B) ⋯ : (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)
⊢ ∃ (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)

Tactic:
use J.toCotangent ⟨y', mem⟩

Premises used: Subtype.mk, Ideal.toCotangent, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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)
⊢ Eq.{u_2 + 1} (α := I.Cotangent)
    ((J.mapCotangent I (Algebra.ofId A B) ⋯ : (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:
simpa using I.toCotangent.congr_arg (SetCoe.ext hy')

Premises used: SetCoe.ext, LinearMap.congr_arg
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
⊢ I = map (F := A →+* B) (algebraMap A B) J

Tactic:
have eqmap := Ideal.eq_map_of_comap_eq_ker_sup _ surj eq
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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))

Tactic:
le_antisymm (fun x hx ↦ ?_) ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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))
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) ⋯).ker
⊢ (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))

Tactic:
refine le_antisymm (fun x hx ↦ ?_) ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
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))
⊢ 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'⟩

Premises used: Ideal.toCotangent_surjective
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)

Tactic:
have : Function.Surjective (Algebra.ofId A B) := surj
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
this : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
⊢ Membership.mem (α := B) (HPow.hPow (α := Ideal B) (β := ℕ) (map (F := A →+* B) (algebraMap A B) J) 2)
    ((algebraMap A B : (a : A) → B) (↑x' : A) : B)

Tactic:
simp only [← hx', LinearMap.mem_ker, Ideal.mapCotangent_toCotangent,
      Ideal.toCotangent_eq_zero, eqmap, Algebra.ofId_apply] at hx

Premises used: Ideal.mapCotangent_toCotangent, LinearMap.mem_ker, Algebra.ofId_apply, Ideal.toCotangent_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
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
x' : ↥J
hx' : (J.toCotangent : (a : ↥J) → J.Cotangent) x' = x
this : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(Algebra.ofId A B) : (a : A) → B)
hx :
  Membership.mem (α := B) (HPow.hPow (α := Ideal B) (β := ℕ) (map (F := A →+* B) (algebraMap A B) J) 2)
    ((algebraMap A B : (a : A) → B) (↑x' : A) : B)
⊢ (↑x' : A) ∈ HPow.hPow (β := ℕ) J 2 ⊔ RingHom.ker (F := A →+* B) (algebraMap A B)

Tactic:
rw [← Ideal.map_pow, ← Ideal.mem_comap, Ideal.comap_map_of_surjective' _ surj] at hx

Premises used: Ideal.comap_map_of_surjective', Ideal.mem_comap, Ideal.map_pow