awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
t : T
x : ↥P.ker
⊢ HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((LinearEquiv.restrictScalars T (LinearEquiv.symm cotangentEquivCotangentKer) :
            (a : P.baseChange.ker.Cotangent) → P.baseChange.Cotangent)
          (((Ideal.toCotangent (ker P.baseChange) :
                LinearMap (R := TensorProduct.{u_1, u_3, u} R T P.Ring)
                  (RingHom.id (TensorProduct.{u_1, u_3, u} R T P.Ring))
                  (↥(ker P.baseChange : Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange)))
                  (Ideal.Cotangent (R := TensorProduct.{u_1, u_3, u} R T P.Ring)
                    (ker P.baseChange : Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange)))) :
              (a : ↥P.baseChange.ker) → P.baseChange.ker.Cotangent)
            (((LinearEquiv.ofEq
                    (Ideal.map (F := P.Ring →+* TensorProduct.{u_1, u_3, u} R T P.Ring)
                      (AlgHom.toRingHom TensorProduct.includeRight) P.ker)
                    (ker P.baseChange) ⋯ :
                  ↥(Ideal.map (F := P.Ring →+* TensorProduct.{u_1, u_3, u} R T P.Ring)
                        (AlgHom.toRingHom TensorProduct.includeRight) P.ker) ≃ₗ[TensorProduct.{u_1, u_3, u} R T P.Ring]
                    ↥(ker P.baseChange : Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange))) :
                (a : ↥(Ideal.map TensorProduct.includeRight.toRingHom P.ker)) → ↥P.baseChange.ker)
              (Subtype.mk (p := fun (x : TensorProduct.{u_1, u_3, u} R T P.Ring) ↦
                Membership.mem (γ := Ideal (TensorProduct.{u_1, u_3, u} R T P.Ring))
                  (Ideal.map (F := P.Ring →+* TensorProduct.{u_1, u_3, u} R T P.Ring)
                    (AlgHom.toRingHom TensorProduct.includeRight) P.ker)
                  x)
                (1 ⊗ₜ[R] (↑x : P.Ring)) ⋯))) :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) =
    HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((Cotangent.mk : (a : ↥P.baseChange.ker) → P.baseChange.Cotangent)
          (Subtype.mk (p := fun (x : Ring (R := T) (S := T ⊗[R] S) P.baseChange) ↦
            Membership.mem (γ := Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange)) (ker P.baseChange) x)
            ((Hom.toRingHom (toBaseChange T) : (a : P.Ring) → P.baseChange.Ring) (↑x : P.Ring)) ⋯) :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
x : P.H1Cotangent
⊢ (↑((P.tensorToH1Cotangent T : (a : T ⊗[R] P.H1Cotangent) → P.baseChange.H1Cotangent) (t ⊗ₜ[R] x)) :
      P.baseChange.Cotangent) =
    HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((Cotangent.map (toBaseChange T) : (a : P.Cotangent) → P.baseChange.Cotangent) (↑x : P.Cotangent) :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, rfl, Algebra.Extension.Cotangent.of
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Eq (α := Unit →ₗ[R] Unit) (0 ∘ₗ 0) (0 ∘ₗ 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Eq (α := Unit →ₗ[R] Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (0 ∘ₗ 0)
    ((↑R :
          {S : Type u_3} →
            {M M₂ : Type (max u u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (P.tensorToH1Cotangent T) ∘ₗ
      0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
hf₂ :
  Function.Injective (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (β :=
    TensorProduct.{u_1, u_3, u} R T P.Cotangent)
    (⇑(LinearMap.lTensor T
            ((↑R :
                {S : Type u_2} →
                  {M M₂ : Type u} →
                    [inst : Semiring R] →
                      [inst_6 : Semiring S] →
                        [inst_7 : AddCommMonoid M] →
                          [inst_8 : AddCommMonoid M₂] →
                            [inst_9 : Module R M] →
                              [inst_10 : Module R M₂] →
                                [inst_11 : Module S M] →
                                  [inst_12 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              h1Cotangentι) :
          TensorProduct.{u_1, u_3, u} R T P.H1Cotangent →ₗ[R] TensorProduct.{u_1, u_3, u} R T P.Cotangent) :
      (a : T ⊗[R] P.H1Cotangent) → T ⊗[R] P.Cotangent)
⊢ Function.Exact (M := Unit) (N := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (P :=
    TensorProduct.{u_1, u_3, u} R T P.Cotangent) (⇑0 : (a : Unit) → T ⊗[R] P.H1Cotangent)
    (⇑(LinearMap.lTensor T
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u} →
                  [inst : Semiring R] →
                    [inst_6 : Semiring S] →
                      [inst_7 : AddCommMonoid M] →
                        [inst_8 : AddCommMonoid M₂] →
                          [inst_9 : Module R M] →
                            [inst_10 : Module R M₂] →
                              [inst_11 : Module S M] →
                                [inst_12 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            h1Cotangentι)) :
      (a : T ⊗[R] P.H1Cotangent) → T ⊗[R] P.Cotangent)

Tactic:
simp only [LinearMap.exact_zero_iff_injective]

Premises used: LinearMap.exact_zero_iff_injective
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
hf₂ :
  Function.Injective.{u + 1, u + 1} (α := P.H1Cotangent) (β := P.Cotangent)
    (⇑((↑R :
            {S : Type u_2} →
              {M M₂ : Type u} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι) :
      (a : P.H1Cotangent) → P.Cotangent)
⊢ Function.Injective (α := TensorProduct.{u_1, u_3, u} R T P.H1Cotangent) (β :=
    TensorProduct.{u_1, u_3, u} R T P.Cotangent)
    (⇑(LinearMap.lTensor T
            ((↑R :
                {S : Type u_2} →
                  {M M₂ : Type u} →
                    [inst : Semiring R] →
                      [inst_6 : Semiring S] →
                        [inst_7 : AddCommMonoid M] →
                          [inst_8 : AddCommMonoid M₂] →
                            [inst_9 : Module R M] →
                              [inst_10 : Module R M₂] →
                                [inst_11 : Module S M] →
                                  [inst_12 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              h1Cotangentι) :
          TensorProduct.{u_1, u_3, u} R T P.H1Cotangent →ₗ[R] TensorProduct.{u_1, u_3, u} R T P.Cotangent) :
      (a : T ⊗[R] P.H1Cotangent) → T ⊗[R] P.Cotangent)

Tactic:
apply Module.Flat.lTensor_preserves_injective_linearMap

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Injective.{u + 1, u + 1} (α := P.H1Cotangent) (β := P.Cotangent)
    (⇑((↑R :
            {S : Type u_2} →
              {M M₂ : Type u} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι) :
      (a : P.H1Cotangent) → P.Cotangent)

Tactic:
h1Cotangentι_injective

Premises used: Algebra.Extension.h1Cotangentι_injective, Algebra.Extension.H1Cotangent
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Injective.{u + 1, u + 1} (α := P.H1Cotangent) (β := P.Cotangent)
    (⇑((↑R :
            {S : Type u_2} →
              {M M₂ : Type u} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι) :
      (a : P.H1Cotangent) → P.Cotangent)

Tactic:
exact h1Cotangentι_injective

Premises used: Algebra.Extension.h1Cotangentι_injective
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Exact (M := P.H1Cotangent) (N := P.Cotangent) (P := P.CotangentSpace)
    (⇑((↑R :
            {S : Type u_2} →
              {M M₂ : Type u} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι) :
      (a : P.H1Cotangent) → P.Cotangent)
    (⇑((↑R :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u u_2)} →
                  [inst : Semiring R] →
                    [inst_6 : Semiring S] →
                      [inst_7 : AddCommMonoid M] →
                        [inst_8 : AddCommMonoid M₂] →
                          [inst_9 : Module R M] →
                            [inst_10 : Module R M₂] →
                              [inst_11 : Module S M] →
                                [inst_12 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          P.cotangentComplex) :
      (a : P.Cotangent) → P.CotangentSpace)

Tactic:
P.exact_hCotangentι_cotangentComplex

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.Extension.exact_hCotangentι_cotangentComplex, Algebra.Extension.H1Cotangent
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Exact (M := P.H1Cotangent) (N := P.Cotangent) (P := P.CotangentSpace)
    (⇑((↑R :
            {S : Type u_2} →
              {M M₂ : Type u} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι) :
      (a : P.H1Cotangent) → P.Cotangent)
    (⇑((↑R :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type (max u u_2)} →
                  [inst : Semiring R] →
                    [inst_6 : Semiring S] →
                      [inst_7 : AddCommMonoid M] →
                        [inst_8 : AddCommMonoid M₂] →
                          [inst_9 : Module R M] →
                            [inst_10 : Module R M₂] →
                              [inst_11 : Module S M] →
                                [inst_12 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          P.cotangentComplex) :
      (a : P.Cotangent) → P.CotangentSpace)

Tactic:
exact P.exact_hCotangentι_cotangentComplex

Premises used: Algebra.Extension.exact_hCotangentι_cotangentComplex
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
hg₂ :
  Function.Injective (α := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (β :=
    Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑((↑R :
            {S : Type (max u_2 u_3)} →
              {M M₂ : Type (max u u_3)} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι) :
      (a : P.baseChange.H1Cotangent) → P.baseChange.Cotangent)
⊢ Function.Exact (M := Unit) (N := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (P :=
    Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) (⇑0 : (a : Unit) → P.baseChange.H1Cotangent)
    (⇑((↑R :
            {S : Type (max u_2 u_3)} →
              {M M₂ : Type (max u u_3)} →
                [inst : Semiring R] →
                  [inst_6 : Semiring S] →
                    [inst_7 : AddCommMonoid M] →
                      [inst_8 : AddCommMonoid M₂] →
                        [inst_9 : Module R M] →
                          [inst_10 : Module R M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          h1Cotangentι) :
      (a : P.baseChange.H1Cotangent) → P.baseChange.Cotangent)

Tactic:
rw [LinearMap.exact_zero_iff_injective]

Premises used: LinearMap.exact_zero_iff_injective
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
hi₁ hi₂ hi₃ hi₄ hi₅ hi₆ hi₇ hi₈ : ∀ (b : Unit), ∃ (a : Unit), (0 : (a : Unit) → Unit) a = b
⊢ Function.Surjective (α := Unit) (β := Unit) (⇑0 : (a : Unit) → Unit)

Tactic:
tauto
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Bijective (α := Unit) (β := Unit) (⇑0 : (a : Unit) → Unit)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Bijective (α := TensorProduct.{u_1, u_3, u} R T P.Cotangent) (β :=
    Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) : T ⊗[R] P.Cotangent →ₗ[R] P.baseChange.Cotangent) :
      (a : T ⊗[R] P.Cotangent) → P.baseChange.Cotangent)

Tactic:
(P.tensorCotangentOfFlat T).bijective

Premises used: LinearEquiv.bijective, Quotient.liftOn', AddCon.liftOn, Algebra.Extension.tensorCotangentOfFlat, Algebra.Extension.Cotangent.of
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Bijective (α := TensorProduct.{u_1, u_3, u} R T P.Cotangent) (β :=
    Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) : T ⊗[R] P.Cotangent →ₗ[R] P.baseChange.Cotangent) :
      (a : T ⊗[R] P.Cotangent) → P.baseChange.Cotangent)

Tactic:
exact (P.tensorCotangentOfFlat T).bijective

Premises used: LinearEquiv.bijective, Algebra.Extension.tensorCotangentOfFlat
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Injective (α := T ⊗[R] P.CotangentSpace) (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T)) :
          T ⊗[R] P.CotangentSpace →ₗ[R] P.baseChange.CotangentSpace) :
      (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)

Tactic:
(P.tensorCotangentSpace T).injective

Premises used: Quotient.liftOn', Algebra.Extension.tensorCotangentSpace, AddCon.liftOn, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
⊢ Function.Injective (α := T ⊗[R] P.CotangentSpace) (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (⇑(↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T)) :
          T ⊗[R] P.CotangentSpace →ₗ[R] P.baseChange.CotangentSpace) :
      (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)

Tactic:
exact (P.tensorCotangentSpace T).injective

Premises used: Algebra.Extension.tensorCotangentSpace, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
t : T
x : P.H1Cotangent
⊢ (P.tensorH1CotangentOfFlat T : (a : T ⊗[R] P.H1Cotangent) → P.baseChange.H1Cotangent) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((H1Cotangent.map (toBaseChange T) : (a : P.H1Cotangent) → P.baseChange.H1Cotangent) x :
        Extension.H1Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
t : T
x : H1Cotangent R S
simp :
  HSMul.hSMul (β := H1Cotangent T (T ⊗[R] S)) t
      ((sorry :
            (a : (Generators.baseChange T (Generators.self R S)).toExtension.H1Cotangent) → H1Cotangent T (T ⊗[R] S))
          ((sorry :
              (a : (Generators.self R S).toExtension.baseChange.H1Cotangent) →
                (Generators.baseChange T (Generators.self R S)).toExtension.H1Cotangent)
            ((Extension.H1Cotangent.map (Extension.toBaseChange T) :
                (a : (Generators.self R S).toExtension.H1Cotangent) →
                  (Generators.self R S).toExtension.baseChange.H1Cotangent)
              x)) :
        H1Cotangent T (T ⊗[R] S)) =
    HSMul.hSMul (β := H1Cotangent T (T ⊗[R] S)) t
      ((H1Cotangent.map R T S (T ⊗[R] S) : (a : H1Cotangent R S) → H1Cotangent T (T ⊗[R] S)) x :
        H1Cotangent T (T ⊗[R] S))
⊢ (tensorH1CotangentOfFlat R S T : (a : T ⊗[R] H1Cotangent R S) → H1Cotangent T (T ⊗[R] S)) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := H1Cotangent T (T ⊗[R] S)) t
      ((H1Cotangent.map R T S (T ⊗[R] S) : (a : H1Cotangent R S) → H1Cotangent T (T ⊗[R] S)) x :
        H1Cotangent T (T ⊗[R] S))

Tactic:
simp only [tensorH1CotangentOfFlat, LinearEquiv.trans_apply,
    Extension.tensorH1CotangentOfFlat_tmul, map_smul, LinearEquiv.restrictScalars_apply,
    Extension.H1Cotangent.equiv, LinearEquiv.coe_mk, Generators.equivH1Cotangent,
    Generators.H1Cotangent.equiv]

Premises used: Algebra.Extension.tensorH1CotangentOfFlat_tmul, LinearEquiv.restrictScalars_apply, LinearEquiv.coe_mk, Algebra.Generators.H1Cotangent.equiv, Algebra.Extension.H1Cotangent.equiv, LinearEquiv.trans_apply, Algebra.Generators.equivH1Cotangent, Algebra.tensorH1CotangentOfFlat, map_smul
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
x : ↥P.ker
⊢ Eq (α := P.CotangentSpace)
    ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) :
      P.CotangentSpace)
    (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (↑x : P.Ring) :
      TensorProduct.{w, v, w} P.Ring S Ω[P.Ring⁄R])

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.tmul, AddCon.toQuotient, rfl