awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
this : (h :
    LE.le (α := Submodule R P)
      (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
      (LinearMap.ker (M₂ := S ⊗[P] Ω[P⁄R])
        ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_2)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
          (↑(D R P) : P →ₗ[R] Ω[P⁄R])))) →
  HasQuotient.Quotient P (B := Submodule R P)
      (Submodule.restrictScalars R
        (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) →ₗ[R]
    S ⊗[P] Ω[P⁄R] :=
  Submodule.liftQ (R := R) (M := P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
    (R₂ := R) (M₂ := S ⊗[P] Ω[P⁄R]) (τ₁₂ := RingHom.id R)
    ((↑R :
          {S M : Type u_2} →
            {M₂ : Type (max u_3 u_2)} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
      (↑(D R P) : P →ₗ[R] Ω[P⁄R]))
x : P
hx :
  Membership.mem (γ := Submodule R P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) x
⊢ x ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))

Tactic:
simp only [Submodule.restrictScalars_mem, pow_two] at hx

Premises used: pow_two, Submodule.restrictScalars_mem
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
this : (h :
    LE.le (α := Submodule R P)
      (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
      (LinearMap.ker (M₂ := S ⊗[P] Ω[P⁄R])
        ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_2)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
          (↑(D R P) : P →ₗ[R] Ω[P⁄R])))) →
  HasQuotient.Quotient P (B := Submodule R P)
      (Submodule.restrictScalars R
        (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) →ₗ[R]
    S ⊗[P] Ω[P⁄R] :=
  Submodule.liftQ (R := R) (M := P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
    (R₂ := R) (M₂ := S ⊗[P] Ω[P⁄R]) (τ₁₂ := RingHom.id R)
    ((↑R :
          {S M : Type u_2} →
            {M₂ : Type (max u_3 u_2)} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
      (↑(D R P) : P →ₗ[R] Ω[P⁄R]))
x : P
hx :
  x ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) x : S ⊗[P] Ω[P⁄R]) (0 : S ⊗[P] Ω[P⁄R])

Tactic:
Submodule.smul_induction_on hx ?_ ?_

Premises used: Submodule.smul_induction_on
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
this : (h :
    LE.le (α := Submodule R P)
      (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
      (LinearMap.ker (M₂ := S ⊗[P] Ω[P⁄R])
        ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_2)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
          (↑(D R P) : P →ₗ[R] Ω[P⁄R])))) →
  HasQuotient.Quotient P (B := Submodule R P)
      (Submodule.restrictScalars R
        (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) →ₗ[R]
    S ⊗[P] Ω[P⁄R] :=
  Submodule.liftQ (R := R) (M := P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
    (R₂ := R) (M₂ := S ⊗[P] Ω[P⁄R]) (τ₁₂ := RingHom.id R)
    ((↑R :
          {S M : Type u_2} →
            {M₂ : Type (max u_3 u_2)} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
      (↑(D R P) : P →ₗ[R] Ω[P⁄R]))
x_1 : P
hx_1 :
  x_1 ∈
    HMul.hMul (α := Ideal P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* S) (algebraMap P S))
x y : P
hx : Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) x : S ⊗[P] Ω[P⁄R]) (0 : S ⊗[P] Ω[P⁄R])
hy : Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) y : S ⊗[P] Ω[P⁄R]) (0 : S ⊗[P] Ω[P⁄R])
⊢ Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) (x + y) : S ⊗[P] Ω[P⁄R]) (0 : S ⊗[P] Ω[P⁄R])

Tactic:
simp only [map_add, hx, hy, tmul_add, zero_add]

Premises used: map_add, zero_add, TensorProduct.tmul_add
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
this : (h :
    LE.le (α := Submodule R P)
      (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
      (LinearMap.ker (M₂ := S ⊗[P] Ω[P⁄R])
        ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_2)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
          (↑(D R P) : P →ₗ[R] Ω[P⁄R])))) →
  HasQuotient.Quotient P (B := Submodule R P)
      (Submodule.restrictScalars R
        (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) →ₗ[R]
    S ⊗[P] Ω[P⁄R] :=
  Submodule.liftQ (R := R) (M := P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
    (R₂ := R) (M₂ := S ⊗[P] Ω[P⁄R]) (τ₁₂ := RingHom.id R)
    ((↑R :
          {S M : Type u_2} →
            {M₂ : Type (max u_3 u_2)} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
      (↑(D R P) : P →ₗ[R] Ω[P⁄R]))
refine_2 : Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) 1) 0
⊢ Eq (α := S ⊗[P] Ω[P⁄R]) ((this ⋯ : (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R]) 1) 0

Tactic:
change (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P 1 = 0

Premises used: KaehlerDifferential.D, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
this : (h :
    LE.le (α := Submodule R P)
      (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
      (LinearMap.ker (M₂ := S ⊗[P] Ω[P⁄R])
        ((↑R :
              {S M : Type u_2} →
                {M₂ : Type (max u_3 u_2)} →
                  [inst : Semiring R] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module R M] →
                            [inst_11 : Module R M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
          (↑(D R P) : P →ₗ[R] Ω[P⁄R])))) →
  HasQuotient.Quotient P (B := Submodule R P)
      (Submodule.restrictScalars R
        (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)) →ₗ[R]
    S ⊗[P] Ω[P⁄R] :=
  Submodule.liftQ (R := R) (M := P)
    (Submodule.restrictScalars R (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
    (R₂ := R) (M₂ := S ⊗[P] Ω[P⁄R]) (τ₁₂ := RingHom.id R)
    ((↑R :
          {S M : Type u_2} →
            {M₂ : Type (max u_3 u_2)} →
              [inst : Semiring R] →
                [inst_7 : Semiring S] →
                  [inst_8 : AddCommMonoid M] →
                    [inst_9 : AddCommMonoid M₂] →
                      [inst_10 : Module R M] →
                        [inst_11 : Module R M₂] →
                          [inst_12 : Module S M] →
                            [inst_13 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (S := P) ((mk P S Ω[P⁄R] : (a : S) → Ω[P⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) 1) ∘ₗ
      (↑(D R P) : P →ₗ[R] Ω[P⁄R]))
⊢ Eq (α := S ⊗[P] Ω[P⁄R]) (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) 1) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
x : P
⊢ Eq (α := S ⊗[P] Ω[P⁄R])
    (((derivationQuotKerSq R P S :
            Derivation R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
              (S ⊗[P] Ω[P⁄R])) :
          (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → S ⊗[P] Ω[P⁄R])
        ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
            (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
          x) :
      S ⊗[P] Ω[P⁄R])
    (1 ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) x : S ⊗[P] Ω[P⁄R])

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
s : S
t : P
change :
  HSMul.hSMul (β := S ⊗[P] Ω[P⁄R]) s
      (((Derivation.liftKaehlerDifferential (R := R) (S :=
                P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) (M :=
                S ⊗[P] Ω[P⁄R]) (derivationQuotKerSq R P S) :
              LinearMap (R := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
                (RingHom.id (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
                Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R]
                (S ⊗[P] Ω[P⁄R])) :
            (a : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
          ((D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
            ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
                (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
              t)) :
        S ⊗[P] Ω[P⁄R]) =
    s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t
⊢ Eq (α := S ⊗[P] Ω[P⁄R])
    ((tensorKaehlerQuotKerSqEquiv R P S :
          (a : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
        (s ⊗ₜ[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2]
          (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
            ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
                (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
              t)) :
      S ⊗[P] Ω[P⁄R])
    (s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t : S ⊗[P] Ω[P⁄R])

Tactic:
change s • (derivationQuotKerSq R P S).liftKaehlerDifferential
    (.D _ _ (Ideal.Quotient.mk _ t)) = _

Premises used: Derivation.liftKaehlerDifferential, Ideal.Quotient.mk, derivationQuotKerSq, KaehlerDifferential.D, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
s : S
t : P
⊢ HSMul.hSMul (β := S ⊗[P] Ω[P⁄R]) s
      (((Derivation.liftKaehlerDifferential (R := R) (S :=
                P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) (M :=
                S ⊗[P] Ω[P⁄R]) (derivationQuotKerSq R P S) :
              LinearMap (R := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2)
                (RingHom.id (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2))
                Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R]
                (S ⊗[P] Ω[P⁄R])) :
            (a : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
          ((D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
            ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
                (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
              t)) :
        S ⊗[P] Ω[P⁄R]) =
    s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t

Tactic:
simp [smul_tmul']

Premises used: TensorProduct.smul_tmul'
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
s : S
t : P
a :
  Eq (α := S ⊗[P] Ω[P⁄R])
    ((tensorKaehlerQuotKerSqEquiv R P S :
          (a : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
        ((LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P S) :
            (a : S ⊗[P] Ω[P⁄R]) → S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
          (s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t)) :
      S ⊗[P] Ω[P⁄R])
    ((tensorKaehlerQuotKerSqEquiv R P S :
          (a : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
        (s ⊗ₜ[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2]
          (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
            ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
                (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
              t)) :
      S ⊗[P] Ω[P⁄R])
⊢ Eq (α :=
    TensorProduct.{u_2, u_3, u_2}
      (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
      Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R])
    ((LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P S) :
          (a : S ⊗[P] Ω[P⁄R]) → S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
        (s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t) :
      TensorProduct.{u_2, u_3, u_2}
        (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
        Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R])
    (s ⊗ₜ[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2]
        (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
            (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
          ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
            t) :
      TensorProduct.{u_2, u_3, u_2}
        (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) S
        Ω[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2⁄R])

Tactic:
apply (tensorKaehlerQuotKerSqEquiv R P S).injective

Premises used: LinearEquiv.injective, tensorKaehlerQuotKerSqEquiv
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
s : S
t : P
⊢ Eq (α := S ⊗[P] Ω[P⁄R])
    ((tensorKaehlerQuotKerSqEquiv R P S :
          (a : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
        ((LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P S) :
            (a : S ⊗[P] Ω[P⁄R]) → S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
          (s ⊗ₜ[P] (D R P : (a : P) → Ω[P⁄R]) t)) :
      S ⊗[P] Ω[P⁄R])
    ((tensorKaehlerQuotKerSqEquiv R P S :
          (a : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) → S ⊗[P] Ω[P⁄R])
        (s ⊗ₜ[P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2]
          (D R (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
              (a : P ⧸ RingHom.ker (algebraMap P S) ^ 2) → Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])
            ((Ideal.Quotient.mk (HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2) :
                (a : P) → P ⧸ RingHom.ker (algebraMap P S) ^ 2)
              t)) :
      S ⊗[P] Ω[P⁄R])

Tactic:
simp
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)

Tactic:
have h₁ : Surjective (algebraMap P' S) := Function.Surjective.of_comp (g := algebraMap P P') hf