case a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑(cotangentEquivIdeal I)
      (↑(LinearEquiv.symm (cotangentEquivIdeal I))
        { val := ↑(Submodule.mkQ (I ^ 2)) x,
          property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) }) =
    ↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx })
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑(LinearEquiv.symm (cotangentEquivIdeal I))
      { val := ↑(Submodule.mkQ (I ^ 2)) x,
        property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(toCotangent I) { val := x, property := hx }
apply I.cotangentEquivIdeal.injective
case a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ { val := ↑(Submodule.mkQ (I ^ 2)) x,
      property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx })
case a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑(cotangentEquivIdeal I)
      (↑(LinearEquiv.symm (cotangentEquivIdeal I))
        { val := ↑(Submodule.mkQ (I ^ 2)) x,
          property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) }) =
    ↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx })
rw [I.cotangentEquivIdeal.apply_symm_apply]
case a.a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑{ val := ↑(Submodule.mkQ (I ^ 2)) x,
        property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx }))
case a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ { val := ↑(Submodule.mkQ (I ^ 2)) x,
      property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx })
ext
no goals
case a.a
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : R
hx : x ∈ I
⊢ ↑{ val := ↑(Submodule.mkQ (I ^ 2)) x,
        property := (_ : ↑(Submodule.mkQ (I ^ 2)) x ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I) } =
    ↑(↑(cotangentEquivIdeal I) (↑(toCotangent I) { val := x, property := hx }))
rfl