awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
trans : I.cotangentToQuotientSquare.range = (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range
trans₁ : (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range = Submodule.restrictScalars R I.cotangentIdeal
⊢ I.cotangentToQuotientSquare.range = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
trans LinearMap.range (I.cotangentToQuotientSquare.comp I.toCotangent)

Premises used: LinearMap.range, LinearMap.comp, Ideal.toCotangent, Ideal.cotangentToQuotientSquare
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
rw : I.cotangentToQuotientSquare.range = Submodule.map I.cotangentToQuotientSquare I.toCotangent.range
rw₁ : I.cotangentToQuotientSquare.range = Submodule.map I.cotangentToQuotientSquare ⊤
rw₂ rw₃ : I.cotangentToQuotientSquare.range = I.cotangentToQuotientSquare.range
⊢ I.cotangentToQuotientSquare.range = (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range

Tactic:
rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]

Premises used: Ideal.toCotangent_range, Submodule.map_top, LinearMap.range_comp
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
rw : Submodule.map (Submodule.mkQ (HPow.hPow (β := ℕ) I 2)) I = Submodule.restrictScalars R I.cotangentIdeal
⊢ (I.cotangentToQuotientSquare ∘ₗ I.toCotangent).range = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]

Premises used: LinearMap.range_comp, Submodule.range_subtype, Ideal.to_quotient_square_comp_toCotangent
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
h :
  ∀ (x : R ⧸ HPow.hPow (β := ℕ) I 2),
    Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
        (Submodule.map (Submodule.mkQ (HPow.hPow (β := ℕ) I 2)) I) x ↔
      Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2)) (Submodule.restrictScalars R I.cotangentIdeal) x
⊢ Submodule.map (Submodule.mkQ (HPow.hPow (β := ℕ) I 2)) I = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R ⧸ HPow.hPow (β := ℕ) I 2
⊢ Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
      (Submodule.map (Submodule.mkQ (HPow.hPow (β := ℕ) I 2)) I) x ↔
    Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2)) (Submodule.restrictScalars R I.cotangentIdeal) x

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x : I.Cotangent
rw :
  Membership.mem (α := R ⧸ HPow.hPow (β := ℕ) I 2) I.cotangentToQuotientSquare.range
    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)
⊢ Membership.mem (α := R ⧸ HPow.hPow (β := ℕ) I 2) (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
    (Submodule.restrictScalars R I.cotangentIdeal)
    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)

Tactic:
rw [← range_cotangentToQuotientSquare]

Premises used: Ideal.range_cotangentToQuotientSquare
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x : I.Cotangent
⊢ Membership.mem (α := R ⧸ HPow.hPow (β := ℕ) I 2) I.cotangentToQuotientSquare.range
    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)

Tactic:
LinearMap.mem_range_self _ _

Premises used: Set.Mem, LinearMap.mem_range_self
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x : I.Cotangent
⊢ Membership.mem (α := R ⧸ HPow.hPow (β := ℕ) I 2) I.cotangentToQuotientSquare.range
    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)

Tactic:
exact LinearMap.mem_range_self _ _

Premises used: LinearMap.mem_range_self
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
refine_1 :
  Function.Injective (β := ↥I.cotangentIdeal) fun (c : I.Cotangent) ↦
    Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
      Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2)) (Submodule.restrictScalars R I.cotangentIdeal) x)
      ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯
refine_2 :
  Function.Surjective (β := ↥I.cotangentIdeal) fun (c : I.Cotangent) ↦
    Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
      Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2)) (Submodule.restrictScalars R I.cotangentIdeal) x)
      ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯
⊢ I.Cotangent ≃ₗ[R] ↥I.cotangentIdeal

Tactic:
refine
  { LinearMap.codRestrict (I.cotangentIdeal.restrictScalars R) I.cotangentToQuotientSquare
      fun x => by rw [← range_cotangentToQuotientSquare]; exact LinearMap.mem_range_self _ _,
    Equiv.ofBijective _ ⟨?_, ?_⟩ with }

Premises used: Ideal.cotangentIdeal, Submodule.restrictScalars, And.intro, Equiv.ofBijective, LinearMap.codRestrict, Ideal.cotangentToQuotientSquare
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x y : I.Cotangent
e :
  Eq.{u + 1} (α := ↥I.cotangentIdeal)
    ((fun (c : I.Cotangent) ↦
        (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
            Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
              (Submodule.restrictScalars R I.cotangentIdeal) x)
            ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
          ↥(Submodule.restrictScalars R I.cotangentIdeal)))
      x)
    ((fun (c : I.Cotangent) ↦
        (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
            Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
              (Submodule.restrictScalars R I.cotangentIdeal) x)
            ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
          ↥(Submodule.restrictScalars R I.cotangentIdeal)))
      y)
⊢ Eq.{u + 1} (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    (↑((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          x) :
      R ⧸ I ^ 2)
    (↑((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          y) :
      R ⧸ I ^ 2)

Tactic:
replace e := congr_arg Subtype.val e
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x y : I.Cotangent
e :
  Eq.{u + 1} (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    (↑((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          x) :
      R ⧸ I ^ 2)
    (↑((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          y) :
      R ⧸ I ^ 2)
refine_1 :
  ∀ (x : ↥I)
    (e :
      Eq.{u + 1} (α := R ⧸ HPow.hPow (β := ℕ) I 2)
        (↑((fun (c : I.Cotangent) ↦
                (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                    Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                      (Submodule.restrictScalars R I.cotangentIdeal) x)
                    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
                  ↥(Submodule.restrictScalars R I.cotangentIdeal)))
              ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
          R ⧸ I ^ 2)
        (↑((fun (c : I.Cotangent) ↦
                (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                    Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                      (Submodule.restrictScalars R I.cotangentIdeal) x)
                    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
                  ↥(Submodule.restrictScalars R I.cotangentIdeal)))
              y) :
          R ⧸ I ^ 2)),
    (I.toCotangent : (a : ↥I) → I.Cotangent) x = y
⊢ x = y

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

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
y : I.Cotangent
x : ↥I
e :
  Eq.{u + 1} (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    (↑((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
      R ⧸ I ^ 2)
    (↑((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          y) :
      R ⧸ I ^ 2)
refine_1 :
  ∀ (y : ↥I)
    (e :
      Eq.{u + 1} (α := R ⧸ HPow.hPow (β := ℕ) I 2)
        (↑((fun (c : I.Cotangent) ↦
                (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                    Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                      (Submodule.restrictScalars R I.cotangentIdeal) x)
                    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
                  ↥(Submodule.restrictScalars R I.cotangentIdeal)))
              ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
          R ⧸ I ^ 2)
        (↑((fun (c : I.Cotangent) ↦
                (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                    Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                      (Submodule.restrictScalars R I.cotangentIdeal) x)
                    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
                  ↥(Submodule.restrictScalars R I.cotangentIdeal)))
              ((I.toCotangent : (a : ↥I) → I.Cotangent) y)) :
          R ⧸ I ^ 2)),
    Eq (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)
      ((I.toCotangent : (a : ↥I) → I.Cotangent) y : I.Cotangent)
⊢ (I.toCotangent : (a : ↥I) → I.Cotangent) x = y

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

Premises used: Ideal.toCotangent_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e :
  Eq.{u + 1} (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    (↑((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          ((I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
      R ⧸ I ^ 2)
    (↑((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          ((I.toCotangent : (a : ↥I) → I.Cotangent) y)) :
      R ⧸ I ^ 2)
refine_1 : (↑x : R) - (↑y : R) ∈ HPow.hPow (β := ℕ) I 2
⊢ Eq (α := I.Cotangent) ((I.toCotangent : (a : ↥I) → I.Cotangent) x : I.Cotangent)
    ((I.toCotangent : (a : ↥I) → I.Cotangent) y : I.Cotangent)

Tactic:
rw [I.toCotangent_eq]

Premises used: Ideal.toCotangent_eq
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e : Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2) (Submodule.Quotient.mk (↑x : R)) (Submodule.Quotient.mk (↑y : R))
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀ (e : (↑x : R) - (↑y : R) ∈ HPow.hPow (β := ℕ) I 2), (↑x : R) - (↑y : R) ∈ HPow.hPow (β := ℕ) I 2
⊢ (↑x : R) - (↑y : R) ∈ HPow.hPow (β := ℕ) I 2

Tactic:
rwa [Submodule.Quotient.eq] at e

Premises used: Submodule.Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ (↑I : Set R)
⊢ ∃ (a : I.Cotangent),
    Eq (α := ↥I.cotangentIdeal)
      ((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          a :
        ↥(Submodule.restrictScalars R I.cotangentIdeal))
      (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦ x ∈ I.cotangentIdeal)
          ((RingHom.toSemilinearMap (Quotient.mk (HPow.hPow (β := ℕ) I 2)) : (a : R) → R ⧸ I ^ 2) x) ⋯ :
        ↥I.cotangentIdeal)

Tactic:
⟨I.toCotangent ⟨x, hx⟩, Subtype.ext rfl⟩

Premises used: Subtype.mk, Exists.intro, Ideal.toCotangent, DFunLike.coe, rfl, Subtype.ext
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ (↑I : Set R)
⊢ ∃ (a : I.Cotangent),
    Eq (α := ↥I.cotangentIdeal)
      ((fun (c : I.Cotangent) ↦
            (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦
                Membership.mem (γ := Submodule R (R ⧸ HPow.hPow (β := ℕ) I 2))
                  (Submodule.restrictScalars R I.cotangentIdeal) x)
                ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) c) ⋯ :
              ↥(Submodule.restrictScalars R I.cotangentIdeal)))
          a :
        ↥(Submodule.restrictScalars R I.cotangentIdeal))
      (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦ x ∈ I.cotangentIdeal)
          ((RingHom.toSemilinearMap (Quotient.mk (HPow.hPow (β := ℕ) I 2)) : (a : R) → R ⧸ I ^ 2) x) ⋯ :
        ↥I.cotangentIdeal)

Tactic:
exact ⟨I.toCotangent ⟨x, hx⟩, Subtype.ext rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : I.Cotangent
⊢ Eq (α := R ⧸ HPow.hPow (β := ℕ) I 2)
    ((↑((I.cotangentEquivIdeal : (a : I.Cotangent) → ↥I.cotangentIdeal) x) : R ⧸ HPow.hPow (β := ℕ) I 2) :
      R ⧸ HPow.hPow (β := ℕ) I 2)
    ((I.cotangentToQuotientSquare : (a : I.Cotangent) → R ⧸ I ^ 2) x : R ⧸ HPow.hPow (β := ℕ) I 2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
I : Ideal R
x : R
hx : x ∈ I
⊢ Eq (α := I.Cotangent)
    ((I.cotangentEquivIdeal.symm : (a : ↥I.cotangentIdeal) → I.Cotangent)
        (Subtype.mk (p := fun (x : R ⧸ HPow.hPow (β := ℕ) I 2) ↦ x ∈ I.cotangentIdeal)
          ((Submodule.mkQ (HPow.hPow (β := ℕ) I 2) : (a : R) → R ⧸ I ^ 2) x) ⋯) :
      I.Cotangent)
    ((I.toCotangent : (a : ↥I) → I.Cotangent) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x hx) : I.Cotangent)

Tactic:
simp [I.cotangentEquivIdeal.symm_apply_eq, Subtype.ext_iff]

Premises used: LinearEquiv.symm_apply_eq, Subtype.ext_iff, Ideal.cotangentEquivIdeal
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
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
f : A →ₐ[R] B
refine_1 :
  ∀ a ∈ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2,
    Eq.{u_2 + 1} (α := B) ((f.toRingHom : (a : A) → B) a : B) (0 : B)
refine_2 :
  ∀ (r : R),
    OneHom.toFun
        (↑(↑(Quotient.lift (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) f.toRingHom ⋯) :
              A ⧸ RingHom.ker f.toRingHom ^ 2 →* B) :
          OneHom (A ⧸ RingHom.ker f.toRingHom ^ 2) B)
        ((algebraMap R (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
            (a : R) → A ⧸ RingHom.ker f.toRingHom ^ 2)
          r) =
      (algebraMap R B : (a : R) → B) r
⊢ AlgHom.{u, u_1, u_2} R (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) B

Tactic:
refine { Ideal.Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ?_ with commutes' := ?_ }

Premises used: HPow.hPow, AlgHom.toRingHom, Ideal.Quotient.lift, OfNat.ofNat, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
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
f : A →ₐ[R] B
a : A
ha : a ∈ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2
⊢ Eq.{u_2 + 1} (α := B) ((f.toRingHom : (a : A) → B) a : B) (0 : B)

Tactic:
Ideal.pow_le_self two_ne_zero ha

Premises used: Set.Mem, setOf, Ideal.pow_le_self, two_ne_zero, Set.preimage, Set.singleton
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
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
f : A →ₐ[R] B
a : A
ha : a ∈ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2
⊢ Eq.{u_2 + 1} (α := B) ((f.toRingHom : (a : A) → B) a : B) (0 : B)

Tactic:
exact Ideal.pow_le_self two_ne_zero ha

Premises used: Ideal.pow_le_self, two_ne_zero
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
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
f : A →ₐ[R] B
r : R
refine_2 :
  Eq.{u_2 + 1} (α := B) ((f.toRingHom : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)
⊢ OneHom.toFun
      (↑(↑(Quotient.lift (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) f.toRingHom ⋯) :
            A ⧸ RingHom.ker f.toRingHom ^ 2 →* B) :
        OneHom (A ⧸ RingHom.ker f.toRingHom ^ 2) B)
      ((algebraMap R (A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
          (a : R) → A ⧸ RingHom.ker f.toRingHom ^ 2)
        r) =
    (algebraMap R B : (a : R) → B) r

Tactic:
rw [IsScalarTower.algebraMap_apply R A, RingHom.toFun_eq_coe, Ideal.Quotient.algebraMap_eq,
      Ideal.Quotient.lift_mk]

Premises used: Ideal.Quotient.algebraMap_eq, Ideal.Quotient.lift_mk, RingHom.toFun_eq_coe, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
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
f : A →ₐ[R] B
r : R
⊢ Eq.{u_2 + 1} (α := B) ((f.toRingHom : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)

Tactic:
f.map_algebraMap r

Premises used: AlgHom.map_algebraMap
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
S : Type v
S' : Type w
inst : CommRing R
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : CommSemiring S'
inst_4 : Algebra S' R
inst_5 : Algebra S S'
inst_6 : IsScalarTower S S' R
I : Ideal R
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
f : A →ₐ[R] B
r : R
⊢ Eq.{u_2 + 1} (α := B) ((f.toRingHom : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B)
    ((algebraMap R B : (a : R) → B) r : B)

Tactic:
exact f.map_algebraMap r

Premises used: AlgHom.map_algebraMap
-- Module: Mathlib.RingTheory.Ideal.Cotangent
Goal:
R : Type u
inst : CommRing R
A : Type u_1
B : Type u_2
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
x : A
⊢ Eq.{u_2 + 1} (α := B)
    ((f.kerSquareLift : (a : A ⧸ RingHom.ker f.toRingHom ^ 2) → B)
        ((Quotient.mk (HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
              (a : A) → A ⧸ RingHom.ker f.toRingHom ^ 2)
            x :
          A ⧸ HPow.hPow (α := Ideal A) (β := ℕ) (RingHom.ker f.toRingHom) 2) :
      B)
    ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl