awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
a :
  ∀ (x_2 : N) (x_3 : M),
    Eq (α := N ⊗[R] M)
      (((((AlgebraTensorModule.curry (LinearMap.rTensor M LinearMap.id) : N →ₗ[R] M →ₗ[R] N ⊗[R] M) :
                  (a : N) → M →ₗ[R] N ⊗[R] M)
                x_2 :
              M →ₗ[R] N ⊗[R] M) :
            (a : M) → N ⊗[R] M)
          x_3 :
        N ⊗[R] M)
      (((((AlgebraTensorModule.curry 0 : N →ₗ[R] M →ₗ[R] N ⊗[R] M) : (a : N) → M →ₗ[R] N ⊗[R] M) x_2 :
              M →ₗ[R] N ⊗[R] M) :
            (a : M) → N ⊗[R] M)
          x_3 :
        N ⊗[R] M)
⊢ Eq (α := N ⊗[R] M →ₗ[R] N ⊗[R] M) (LinearMap.rTensor M LinearMap.id) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
x_2 : N
x_3 : M
⊢ Eq (α := N ⊗[R] M)
    (((((AlgebraTensorModule.curry (LinearMap.rTensor M LinearMap.id) : N →ₗ[R] M →ₗ[R] N ⊗[R] M) :
                (a : N) → M →ₗ[R] N ⊗[R] M)
              x_2 :
            M →ₗ[R] N ⊗[R] M) :
          (a : M) → N ⊗[R] M)
        x_3 :
      N ⊗[R] M)
    (((((AlgebraTensorModule.curry 0 : N →ₗ[R] M →ₗ[R] N ⊗[R] M) : (a : N) → M →ₗ[R] N ⊗[R] M) x_2 : M →ₗ[R] N ⊗[R] M) :
          (a : M) → N ⊗[R] M)
        x_3 :
      N ⊗[R] M)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
x_2 : N
x_3 : M
⊢ Eq (α := N ⊗[R] M)
    (((((AlgebraTensorModule.curry (LinearMap.rTensor M LinearMap.id) : N →ₗ[R] M →ₗ[R] N ⊗[R] M) :
                (a : N) → M →ₗ[R] N ⊗[R] M)
              x_2 :
            M →ₗ[R] N ⊗[R] M) :
          (a : M) → N ⊗[R] M)
        x_3 :
      N ⊗[R] M)
    (((((AlgebraTensorModule.curry 0 : N →ₗ[R] M →ₗ[R] N ⊗[R] M) : (a : N) → M →ₗ[R] N ⊗[R] M) x_2 : M →ₗ[R] N ⊗[R] M) :
          (a : M) → N ⊗[R] M)
        x_3 :
      N ⊗[R] M)

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
⊢ Eq (α := N →ₗ[R] N) LinearMap.id 0

Tactic:
have := Z (LinearMap.id : N →ₗ[R] N) |>.1 (by ext; exact Subsingleton.elim _ _)
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
this : Eq (α := N →ₗ[R] N) LinearMap.id 0
rw : ∀ (y : N), y = 0
⊢ Subsingleton N

Tactic:
rw [subsingleton_iff_forall_eq 0]

Premises used: subsingleton_iff_forall_eq, OfNat.ofNat
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
this : Eq (α := N →ₗ[R] N) LinearMap.id 0
⊢ ∀ (y : N), y = 0

Tactic:
fun y => congr($this y)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
      [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {N' : Type (max u v)}
    [inst_5 : AddCommGroup N'] [inst_6 : Module R N'] (f : N →ₗ[R] N'),
    Eq (α := N ⊗[R] M →ₗ[R] N' ⊗[R] M) (LinearMap.rTensor M f) 0 ↔ f = 0
N : Type (max u v)
x : AddCommGroup N
x_1 : Module R N
h_1 : Subsingleton (N ⊗[R] M)
this : Eq (α := N →ₗ[R] N) LinearMap.id 0
⊢ ∀ (y : N), y = 0

Tactic:
exact fun y => congr($this y)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
rw :
  Flat R M ∧
    ∀ {N : Type (max u_1 u_3)} [inst_9 : AddCommGroup N] [inst_10 : Module R N] {N' : Type (max u_1 u_3)}
      [inst_11 : AddCommGroup N'] [inst_12 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0 ↔ f = 0
⊢ FaithfullyFlat R M

Tactic:
rw [iff_zero_iff_lTensor_zero]

Premises used: Module.FaithfullyFlat.iff_zero_iff_lTensor_zero
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
eq : f = 0
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M 0) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
refine :
  ∀ (N : Type (max u_1 u_3)) (x : AddCommGroup N) (x_1 : Module R N) (N' : Type (max u_1 u_3)) (x_2 : AddCommGroup N')
    (x_3 : Module R N') (f : N →ₗ[R] N') (aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0), f = 0
⊢ Flat R M ∧
    ∀ {N : Type (max u_1 u_3)} [inst_9 : AddCommGroup N] [inst_10 : Module R N] {N' : Type (max u_1 u_3)}
      [inst_11 : AddCommGroup N'] [inst_12 : Module R N'] (f : N →ₗ[R] N'),
      Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0 ↔ f = 0

Tactic:
refine ⟨Module.Flat.trans R S M, @fun N _ _ N' _ _ f => ⟨fun aux => ?_, fun eq => eq ▸ by simp⟩⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
⊢ Eq (α := S ⊗[R] N →ₗ[R] S ⊗[R] N') (lTensor S f)
    ((↑R :
        {S : Type u_2} →
          {M M₂ : Type (max (max u_1 u_3) u_2)} →
            [inst : Semiring R] →
              [inst_9 : Semiring S] →
                [inst_10 : AddCommMonoid M] →
                  [inst_11 : AddCommMonoid M₂] →
                    [inst_12 : Module R M] →
                      [inst_13 : Module R M₂] →
                        [inst_14 : Module S M] →
                          [inst_15 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S) (AlgebraTensorModule.map LinearMap.id f : S ⊗[R] N →ₗ[S] S ⊗[R] N'))

Tactic:
aesop
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
⊢ Eq (α := S ⊗[R] N →ₗ[R] S ⊗[R] N') 0
    ((↑R :
        {S : Type u_2} →
          {M M₂ : Type (max (max u_1 u_2) u_3)} →
            [inst : Semiring R] →
              [inst_9 : Semiring S] →
                [inst_10 : AddCommMonoid M] →
                  [inst_11 : AddCommMonoid M₂] →
                    [inst_12 : Module R M] →
                      [inst_13 : Module R M₂] →
                        [inst_14 : Module S M] →
                          [inst_15 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S) 0)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
rw :
  Eq (α := M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
    (lTensor M (AlgebraTensorModule.map LinearMap.id f) : M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
    (0 : M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
⊢ f = 0

Tactic:
rw [zero_iff_lTensor_zero (R:= R) (M := S) f,
    show f.lTensor S = (AlgebraTensorModule.map (A:= S) LinearMap.id f).restrictScalars R by aesop,
    show (0 :  S ⊗[R] N →ₗ[R] S ⊗[R] N') = (0 : S ⊗[R] N →ₗ[S] S ⊗[R] N').restrictScalars R by rfl,
    restrictScalars_inj, zero_iff_lTensor_zero (R:= S) (M := M)]

Premises used: Module.FaithfullyFlat.zero_iff_lTensor_zero, LinearMap.restrictScalars_inj
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
a :
  ∀ (m : M) (n : N),
    Eq (α := M ⊗[S] (S ⊗[R] N'))
      ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f)) :
                          M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                        (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                      m) :
                  S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
                (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
              1 :
            (a : N) → M ⊗[S] (S ⊗[R] N'))
          n :
        M ⊗[S] (S ⊗[R] N'))
      ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry 0 : M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                        (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                      m) :
                  S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
                (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
              1 :
            (a : N) → M ⊗[S] (S ⊗[R] N'))
          n :
        M ⊗[S] (S ⊗[R] N'))
⊢ Eq (α := M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
    (lTensor M (AlgebraTensorModule.map LinearMap.id f) : M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))
    (0 : M ⊗[S] (S ⊗[R] N) →ₗ[S] M ⊗[S] (S ⊗[R] N'))

Tactic:
ext m n
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
m : M
n : N
⊢ Function.Injective (α := M ⊗[S] (S ⊗[R] N')) (β := M ⊗[R] N')
    (⇑(AlgebraTensorModule.cancelBaseChange R S S M N' : M ⊗[S] (S ⊗[R] N') ≃ₗ[S] M ⊗[R] N') :
      (a : M ⊗[S] (S ⊗[R] N')) → M ⊗[R] N')

Tactic:
LinearEquiv.injective _

Premises used: LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
m : M
n : N
a :
  Eq (α := M ⊗[R] N')
    (((AlgebraTensorModule.cancelBaseChange R S S M N' : M ⊗[S] (S ⊗[R] N') ≃ₗ[S] M ⊗[R] N') :
          (a : M ⊗[S] (S ⊗[R] N')) → M ⊗[R] N')
        ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f)) :
                          M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                        (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                      m) :
                  S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
                (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
              1 :
            (a : N) → M ⊗[S] (S ⊗[R] N'))
          n) :
      M ⊗[R] N')
    (((AlgebraTensorModule.cancelBaseChange R S S M N' : M ⊗[S] (S ⊗[R] N') ≃ₗ[S] M ⊗[R] N') :
          (a : M ⊗[S] (S ⊗[R] N')) → M ⊗[R] N')
        ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry 0 : M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                        (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                      m) :
                  S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
                (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
              1 :
            (a : N) → M ⊗[S] (S ⊗[R] N'))
          n) :
      M ⊗[R] N')
⊢ Eq (α := M ⊗[S] (S ⊗[R] N'))
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f)) :
                        M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                      (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                    m) :
                S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
              (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
            1 :
          (a : N) → M ⊗[S] (S ⊗[R] N'))
        n :
      M ⊗[S] (S ⊗[R] N'))
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry 0 : M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                      (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                    m) :
                S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
              (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
            1 :
          (a : N) → M ⊗[S] (S ⊗[R] N'))
        n :
      M ⊗[S] (S ⊗[R] N'))

Tactic:
apply_fun AlgebraTensorModule.cancelBaseChange R S S M N' using LinearEquiv.injective _

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FaithfullyFlat R S
inst_8 : FaithfullyFlat S M
N : Type (max u_1 u_3)
x : AddCommGroup N
x_1 : Module R N
N' : Type (max u_1 u_3)
x_2 : AddCommGroup N'
x_3 : Module R N'
f : N →ₗ[R] N'
aux : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N') (lTensor M f) 0
m : M
n : N
⊢ Eq (α := M ⊗[R] N')
    (((AlgebraTensorModule.cancelBaseChange R S S M N' : M ⊗[S] (S ⊗[R] N') ≃ₗ[S] M ⊗[R] N') :
          (a : M ⊗[S] (S ⊗[R] N')) → M ⊗[R] N')
        ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry (lTensor M (AlgebraTensorModule.map LinearMap.id f)) :
                          M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                        (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                      m) :
                  S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
                (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
              1 :
            (a : N) → M ⊗[S] (S ⊗[R] N'))
          n) :
      M ⊗[R] N')
    (((AlgebraTensorModule.cancelBaseChange R S S M N' : M ⊗[S] (S ⊗[R] N') ≃ₗ[S] M ⊗[R] N') :
          (a : M ⊗[S] (S ⊗[R] N')) → M ⊗[R] N')
        ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry 0 : M →ₗ[S] S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N')) :
                        (a : M) → S ⊗[R] N →ₗ[S] M ⊗[S] (S ⊗[R] N'))
                      m) :
                  S →ₗ[S] N →ₗ[R] M ⊗[S] (S ⊗[R] N')) :
                (a : S) → N →ₗ[R] M ⊗[S] (S ⊗[R] N'))
              1 :
            (a : N) → M ⊗[S] (S ⊗[R] N'))
          n) :
      M ⊗[R] N')

Tactic:
simpa using congr($aux (m ⊗ₜ[R] n))
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R M
rw :
  Flat S (S ⊗[R] M) ∧
    ∀ (N : Type (max u_1 v)) [inst_6 : AddCommGroup N] [inst_7 : Module S N],
      Subsingleton (N ⊗[S] (S ⊗[R] M)) → Subsingleton N
⊢ FaithfullyFlat S (S ⊗[R] M)

Tactic:
rw [Module.FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality]

Premises used: Module.FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R M
⊢ Flat S (S ⊗[R] M) ∧
    ∀ (N : Type (max u_1 v)) [inst_6 : AddCommGroup N] [inst_7 : Module S N],
      Subsingleton (N ⊗[S] (S ⊗[R] M)) → Subsingleton N

Tactic:
⟨inferInstance, fun N _ _ hN ↦ ?_⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R M
refine :
  ∀ (N : Type (max u_1 v)) (x : AddCommGroup N) (x_1 : Module S N) (hN : Subsingleton (N ⊗[S] (S ⊗[R] M))),
    Subsingleton N
⊢ Flat S (S ⊗[R] M) ∧
    ∀ (N : Type (max u_1 v)) [inst_6 : AddCommGroup N] [inst_7 : Module S N],
      Subsingleton (N ⊗[S] (S ⊗[R] M)) → Subsingleton N

Tactic:
refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R M
N : Type (max u_1 v)
x : AddCommGroup N
x_1 : Module S N
hN : Subsingleton (N ⊗[S] (S ⊗[R] M))
x_2 : Module R N := compHom N (algebraMap R S)
⊢ IsScalarTower R S N

Tactic:
have : IsScalarTower R S N := IsScalarTower.of_algebraMap_smul fun r ↦ congrFun rfl
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R M
N : Type (max u_1 v)
x : AddCommGroup N
x_1 : Module S N
hN : Subsingleton (N ⊗[S] (S ⊗[R] M))
x_2 : Module R N := compHom N (algebraMap R S)
this : IsScalarTower R S N
⊢ Subsingleton (N ⊗[R] M)

Tactic:
have := (AlgebraTensorModule.cancelBaseChange R S S N M).symm.subsingleton
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R M
N : Type (max u_1 v)
x : AddCommGroup N
x_1 : Module S N
hN : Subsingleton (N ⊗[S] (S ⊗[R] M))
x_2 : Module R N := compHom N (algebraMap R S)
this_1 : IsScalarTower R S N
this : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N

Tactic:
FaithfullyFlat.rTensor_reflects_triviality R M N

Premises used: Module.FaithfullyFlat.rTensor_reflects_triviality
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_1
inst_3 : CommRing S
inst_4 : Algebra R S
inst_5 : FaithfullyFlat R M
N : Type (max u_1 v)
x : AddCommGroup N
x_1 : Module S N
hN : Subsingleton (N ⊗[S] (S ⊗[R] M))
x_2 : Module R N := compHom N (algebraMap R S)
this_1 : IsScalarTower R S N
this : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N

Tactic:
exact FaithfullyFlat.rTensor_reflects_triviality R M N

Premises used: Module.FaithfullyFlat.rTensor_reflects_triviality