awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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 : FaithfullyFlat R S
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
this :
  Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 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₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))
apply :
  Function.Injective (α := S ⊗[R] R) (β := S ⊗[R] T)
    (⇑(LinearMap.lTensor S (Algebra.linearMap R T)) : (a : S ⊗[R] R) → S ⊗[R] T)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)

Tactic:
apply (Module.FaithfullyFlat.lTensor_injective_iff_injective R S (Algebra.linearMap R T)).mp

Premises used: Module.FaithfullyFlat.lTensor_injective_iff_injective, Algebra.linearMap, Iff.mp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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 : FaithfullyFlat R S
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
this :
  Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 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₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))
⊢ Function.Injective (α := S ⊗[R] R) (β := S ⊗[R] T)
    (⇑(LinearMap.lTensor S (Algebra.linearMap R T)) : (a : S ⊗[R] R) → S ⊗[R] T)

Tactic:
simpa [this] using H
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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 : FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
a :
  ∀ (x : S),
    Eq (α := S ⊗[R] T)
      (((((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R T)) : S →ₗ[R] R →ₗ[R] S ⊗[R] T) :
                (a : S) → R →ₗ[R] S ⊗[R] T)
              x :
            R →ₗ[R] S ⊗[R] T) :
          (a : R) → S ⊗[R] T)
        1)
      (((((AlgebraTensorModule.curry
                    ((↑R :
                        {S : Type u_2} →
                          {M : Type (max u_1 u_2)} →
                            {M₂ : Type (max u_2 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₂)
                      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
                        S ⊗[R] R →ₗ[S] S ⊗[R] T)) :
                  S →ₗ[R] R →ₗ[R] S ⊗[R] T) :
                (a : S) → R →ₗ[R] S ⊗[R] T)
              x :
            R →ₗ[R] S ⊗[R] T) :
          (a : R) → S ⊗[R] T)
        1)
⊢ Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 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₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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 : FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
x : S
⊢ Eq (α := S ⊗[R] T)
    (((((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R T)) : S →ₗ[R] R →ₗ[R] S ⊗[R] T) :
              (a : S) → R →ₗ[R] S ⊗[R] T)
            x :
          R →ₗ[R] S ⊗[R] T) :
        (a : R) → S ⊗[R] T)
      1)
    (((((AlgebraTensorModule.curry
                  ((↑R :
                      {S : Type u_2} →
                        {M : Type (max u_1 u_2)} →
                          {M₂ : Type (max u_2 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₂)
                    (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
                      S ⊗[R] R →ₗ[S] S ⊗[R] T)) :
                S →ₗ[R] R →ₗ[R] S ⊗[R] T) :
              (a : S) → R →ₗ[R] S ⊗[R] T)
            x :
          R →ₗ[R] S ⊗[R] T) :
        (a : R) → S ⊗[R] T)
      1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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 : FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 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₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))

Tactic:
have : LinearMap.lTensor S (Algebra.linearMap R T) =
      Algebra.linearMap S (S ⊗[R] T) ∘ₗ (AlgebraTensorModule.rid R S S).toLinearMap := by
    ext; simp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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 : FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
this :
  Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 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₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))
apply :
  Function.Surjective (α := S ⊗[R] R) (β := S ⊗[R] T)
    (⇑(LinearMap.lTensor S (Algebra.linearMap R T)) : (a : S ⊗[R] R) → S ⊗[R] T)
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)

Tactic:
apply (Module.FaithfullyFlat.lTensor_surjective_iff_surjective R S (Algebra.linearMap R T)).mp

Premises used: Module.FaithfullyFlat.lTensor_surjective_iff_surjective, Algebra.linearMap, Iff.mp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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 : FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
this :
  Eq (α := S ⊗[R] R →ₗ[R] S ⊗[R] T) (LinearMap.lTensor S (Algebra.linearMap R T))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_1 u_2)} →
            {M₂ : Type (max u_2 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₂)
      (Algebra.linearMap S (S ⊗[R] T) ∘ₗ (↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) :
        S ⊗[R] R →ₗ[S] S ⊗[R] T))
⊢ Function.Surjective (α := S ⊗[R] R) (β := S ⊗[R] T)
    (⇑(LinearMap.lTensor S (Algebra.linearMap R T)) : (a : S ⊗[R] R) → S ⊗[R] T)

Tactic:
simpa [this] using H
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
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 : FaithfullyFlat R S
H : Function.Bijective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Bijective.{u_1 + 1, u_3 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)

Tactic:
⟨injective_of_tensorProduct H.1, surjective_of_tensorProduct H.2⟩

Premises used: Module.FaithfullyFlat.injective_of_tensorProduct, And.right, And.left, And.intro, Function.Bijective, Module.FaithfullyFlat.surjective_of_tensorProduct
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
apply :
  ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    FaithfullyFlat (algebraMap R S) →
      Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T) →
        Function.Injective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ CodescendsAlong.{u_1}
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Injective (α := R) (β := S) (⇑f : (a : R) → S))
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
apply CodescendsAlong.mk _ injective_respectsIso

Premises used: RingHom.CodescendsAlong.mk, RingHom.injective_respectsIso
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Module.FaithfullyFlat R S

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
h₁ : Module.FaithfullyFlat R S
⊢ Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Module.FaithfullyFlat R S
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Injective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)

Tactic:
h.injective_of_tensorProduct H

Premises used: Module.FaithfullyFlat.injective_of_tensorProduct
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Module.FaithfullyFlat R S
H : Function.Injective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Injective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)

Tactic:
exact h.injective_of_tensorProduct H

Premises used: Module.FaithfullyFlat.injective_of_tensorProduct
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
apply :
  ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    FaithfullyFlat (algebraMap R S) →
      Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T) →
        Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ CodescendsAlong.{u_1}
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S))
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
apply CodescendsAlong.mk _ surjective_respectsIso

Premises used: RingHom.CodescendsAlong.mk, RingHom.surjective_respectsIso
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Module.FaithfullyFlat R S

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : FaithfullyFlat (algebraMap R S)
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
h₁ : Module.FaithfullyFlat R S
⊢ Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)

Tactic:
rw [faithfullyFlat_algebraMap_iff] at h

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Module.FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)

Tactic:
h.surjective_of_tensorProduct H

Premises used: Module.FaithfullyFlat.surjective_of_tensorProduct
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Module.FaithfullyFlat R S
H : Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)

Tactic:
exact h.surjective_of_tensorProduct H

Premises used: Module.FaithfullyFlat.surjective_of_tensorProduct
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Goal:
⊢ CodescendsAlong.{u_1}
    (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S))
    fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
CodescendsAlong.and codescendsAlong_injective codescendsAlong_surjective

Premises used: RingHom.FaithfullyFlat.codescendsAlong_surjective, RingHom.CodescendsAlong.and, Function.Bijective, RingHom.FaithfullyFlat.codescendsAlong_injective
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
⊢ Module.Flat R S

Tactic:
Module.Flat.iff_lTensor_injectiveₛ.mpr fun P _ _ N ↦ ?_

Premises used: Iff.mpr, Module.Flat.iff_lTensor_injectiveₛ
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
refine :
  ∀ (P : Type u_1) (x : AddCommMonoid P) (x_1 : Module R P) (N : Submodule R P),
    Function.Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P) (⇑(lTensor S N.subtype) : (a : S ⊗[R] ↥N) → S ⊗[R] P)
⊢ Module.Flat R S

Tactic:
refine Module.Flat.iff_lTensor_injectiveₛ.mpr fun P _ _ N ↦ ?_

Premises used: Iff.mpr, Module.Flat.iff_lTensor_injectiveₛ
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
P : Type u_1
x : AddCommMonoid P
x_1 : Module R P
N : Submodule R P
⊢ IsBaseChange (N :=
    ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)) S
    (Submodule.toLocalized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)

Tactic:
have h := ((range N.subtype).isLocalizedModule S p (TensorProduct.mk R S P 1)).isBaseChange _ S
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
P : Type u_1
x : AddCommMonoid P
x_1 : Module R P
N : Submodule R P
h :
  IsBaseChange (N :=
    ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)) S
    (Submodule.toLocalized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R]
  ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
a :
  ∀ (x_2 : S) (x_3 : ↥N),
    Eq (α := S ⊗[R] P)
      (((((AlgebraTensorModule.curry (lTensor S N.subtype) : S →ₗ[R] ↥N →ₗ[R] S ⊗[R] P) : (a : S) → ↥N →ₗ[R] S ⊗[R] P)
                x_2 :
              ↥N →ₗ[R] S ⊗[R] P) :
            (a : ↥N) → S ⊗[R] P)
          x_3 :
        S ⊗[R] P)
      (((((AlgebraTensorModule.curry
                      (Submodule.subtype
                          (Submodule.localized₀ p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1)
                            N.subtype.range) ∘ₗ
                        (↑e :
                          S ⊗[R] ↥N →ₗ[R]
                            ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1)
                                N.subtype.range))) :
                    S →ₗ[R] ↥N →ₗ[R] S ⊗[R] P) :
                  (a : S) → ↥N →ₗ[R] S ⊗[R] P)
                x_2 :
              ↥N →ₗ[R] S ⊗[R] P) :
            (a : ↥N) → S ⊗[R] P)
          x_3 :
        S ⊗[R] P)
⊢ lTensor S N.subtype =
    Submodule.subtype
        (Submodule.localized₀ p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range) ∘ₗ
      (↑e :
        S ⊗[R] ↥N →ₗ[R]
          ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range))

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
p : Submonoid R
inst_3 : IsLocalization p S
P : Type u_1
x : AddCommMonoid P
x_1 : Module R P
N : Submodule R P
h :
  IsBaseChange (N :=
    ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)) S
    (Submodule.toLocalized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R]
  ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x_2 : S
x_3 : ↥N
a :
  Eq (α := S ⊗[R] P)
    (((((AlgebraTensorModule.curry (lTensor S N.subtype) : S →ₗ[R] ↥N →ₗ[R] S ⊗[R] P) : (a : S) → ↥N →ₗ[R] S ⊗[R] P)
              x_2 :
            ↥N →ₗ[R] S ⊗[R] P) :
          (a : ↥N) → S ⊗[R] P)
        x_3 :
      S ⊗[R] P)
    ((↑((h.equiv :
              (a : S ⊗[R] ↥N.subtype.range) →
                ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1) N.subtype.range))
            (((↑(LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯)) :
                  S ⊗[R] ↥N →ₗ[R] S ⊗[R] ↥N.subtype.range) :
                (a : S ⊗[R] ↥N) → S ⊗[R] ↥N.subtype.range)
              ((((TensorProduct.mk R S ↥N : (a : S) → ↥N →ₗ[R] S ⊗[R] ↥N) x_2 : ↥N →ₗ[R] S ⊗[R] ↥N) :
                  (a : ↥N) → S ⊗[R] ↥N)
                x_3))) :
        S ⊗[R] P) :
      S ⊗[R] P)
⊢ Eq (α := S ⊗[R] P)
    (((((AlgebraTensorModule.curry (lTensor S N.subtype) : S →ₗ[R] ↥N →ₗ[R] S ⊗[R] P) : (a : S) → ↥N →ₗ[R] S ⊗[R] P)
              x_2 :
            ↥N →ₗ[R] S ⊗[R] P) :
          (a : ↥N) → S ⊗[R] P)
        x_3 :
      S ⊗[R] P)
    (((((AlgebraTensorModule.curry
                    (Submodule.subtype
                        (Submodule.localized₀ p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1)
                          N.subtype.range) ∘ₗ
                      (↑e :
                        S ⊗[R] ↥N →ₗ[R]
                          ↥(Submodule.localized' S p ((TensorProduct.mk R S P : (a : S) → P →ₗ[R] S ⊗[R] P) 1)
                              N.subtype.range))) :
                  S →ₗ[R] ↥N →ₗ[R] S ⊗[R] P) :
                (a : S) → ↥N →ₗ[R] S ⊗[R] P)
              x_2 :
            ↥N →ₗ[R] S ⊗[R] P) :
          (a : ↥N) → S ⊗[R] P)
        x_3 :
      S ⊗[R] P)

Tactic:
change _ = (h.equiv _).1

Premises used: Subtype.val, DFunLike.coe, IsBaseChange.equiv