awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N] [inst_7 : Module R N']
    (f : N →ₗ[R] N'),
    Injective (α := N) (β := N') (⇑f : (a : N) → N') →
      Injective (α := N ⊗[R] M) (β := N' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
P : Type u
x : AddCommMonoid P
x_1 : Module R P
h_1 : Module.Finite R P
x_2 : Submodule R P
h_2 : x_2.FG
this : Small.{v', u} P
⊢ Injective (α :=
    TensorProduct.{u, v', v} R
      (↥(range ((↑(LinearEquiv.symm (Shrink.linearEquiv R P)) : P →ₗ[R] Shrink.{v', u} P) ∘ₗ x_2.subtype))) M)
    (β := TensorProduct.{u, v', v} R (Shrink.{v', u} P) M)
    (⇑(rTensor M
          (Submodule.subtype
            (range ((↑(LinearEquiv.symm (Shrink.linearEquiv R P)) : P →ₗ[R] Shrink.{v', u} P) ∘ₗ x_2.subtype)))) :
      (a : ↥((↑(Shrink.linearEquiv R P).symm : P →ₗ[R] Shrink.{v', u} P) ∘ₗ x_2.subtype).range ⊗[R] M) →
        Shrink.{v', u} P ⊗[R] M)

Tactic:
h _ Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N] [inst_7 : Module R N']
    (f : N →ₗ[R] N'),
    Injective (α := N) (β := N') (⇑f : (a : N) → N') →
      Injective (α := N ⊗[R] M) (β := N' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
P : Type u
x : AddCommMonoid P
x_1 : Module R P
h_1 : Module.Finite R P
x_2 : Submodule R P
h_2 : x_2.FG
this : Small.{v', u} P
⊢ Injective (α :=
    TensorProduct.{u, v', v} R
      (↥(range ((↑(LinearEquiv.symm (Shrink.linearEquiv R P)) : P →ₗ[R] Shrink.{v', u} P) ∘ₗ x_2.subtype))) M)
    (β := TensorProduct.{u, v', v} R (Shrink.{v', u} P) M)
    (⇑(rTensor M
          (Submodule.subtype
            (range ((↑(LinearEquiv.symm (Shrink.linearEquiv R P)) : P →ₗ[R] Shrink.{v', u} P) ∘ₗ x_2.subtype)))) :
      (a : ↥((↑(Shrink.linearEquiv R P).symm : P →ₗ[R] Shrink.{v', u} P) ∘ₗ x_2.subtype).range ⊗[R] M) →
        Shrink.{v', u} P ⊗[R] M)

Tactic:
exact h _ Subtype.val_injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{v', u} R
simp_rw :
  (∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
      [inst_7 : Module R N'] (f : N →ₗ[R] N'),
      Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Injective (α := N ⊗[R] M) (β := N' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)) ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
      [inst_7 : Module R N'] (f : N →ₗ[R] N'),
      Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Injective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
      [inst_7 : Module R N'] (f : N →ₗ[R] N'),
      Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Injective (α := M ⊗[R] N) (β := M ⊗[R] N') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')

Tactic:
simp_rw [iff_rTensor_preserves_injective_linearMapₛ, LinearMap.lTensor_inj_iff_rTensor_inj]

Premises used: Module.Flat.iff_rTensor_preserves_injective_linearMapₛ, LinearMap.lTensor_inj_iff_rTensor_inj
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M)

Tactic:
⟨fun _ _ _ _ _ ↦ rTensor_preserves_injective_linearMap _ Subtype.val_injective,
    fun h ↦ ⟨fun _ _ _ _ _ _ ↦ h _⟩⟩

Premises used: Subtype.val_injective, Module.Flat.mk, Iff.intro, Submodule.subtype, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
simp_rw :
  (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M)) ↔
    ∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
⊢ Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)

Tactic:
simp_rw [iff_rTensor_injectiveₛ, LinearMap.lTensor_inj_iff_rTensor_inj]

Premises used: Module.Flat.iff_rTensor_injectiveₛ, LinearMap.lTensor_inj_iff_rTensor_inj
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
x : Type u
x_1 : AddCommMonoid x
x_2 : Module R x
h : Module.Finite R x
I : Submodule R x
h_1 : I.FG
rw :
  Injective (α := ↥I) (β := x)
    (Function.comp (β := x ⊗[R] R)
      (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (TensorProduct.rid R x))) : (a : x ⊗[R] R) → x)
      (Function.comp (β := ↥I ⊗[R] R) (⇑(rTensor R I.subtype) : (a : ↥I ⊗[R] R) → x ⊗[R] R)
        (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (LinearEquiv.symm (TensorProduct.rid R ↥I)))) :
          (a : ↥I) → ↥I ⊗[R] R)))
⊢ Injective (α := ↥I ⊗[R] R) (β := x ⊗[R] R) (⇑(rTensor R I.subtype) : (a : ↥I ⊗[R] R) → x ⊗[R] R)

Tactic:
rw [← (TensorProduct.rid R I).symm.injective_comp, ← (TensorProduct.rid R _).comp_injective]

Premises used: LinearEquiv.symm, TensorProduct.rid, Membership.mem, Subtype, LinearEquiv.toAddEquiv, Equiv.injective_comp, Equiv.comp_injective, AddEquiv.toEquiv
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
x : Type u
x_1 : AddCommMonoid x
x_2 : Module R x
h : Module.Finite R x
I : Submodule R x
h_1 : I.FG
⊢ Injective (β := x) fun (a : ↥I) ↦ (↑a : x)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
x : Type u
x_1 : AddCommMonoid x
x_2 : Module R x
h_1 : Module.Finite R x
I : Submodule R x
h_2 : I.FG
h :
  Eq (α := ↥I → x)
    (Function.comp (β := x ⊗[R] R)
      (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (TensorProduct.rid R x))) : (a : x ⊗[R] R) → x)
      (Function.comp (β := ↥I ⊗[R] R) (⇑(rTensor R I.subtype) : (a : ↥I ⊗[R] R) → x ⊗[R] R)
        (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (LinearEquiv.symm (TensorProduct.rid R ↥I)))) :
          (a : ↥I) → ↥I ⊗[R] R)))
    fun (a : ↥I) ↦ (↑a : x)
⊢ Injective (α := ↥I) (β := x)
    (Function.comp (β := x ⊗[R] R)
      (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (TensorProduct.rid R x))) : (a : x ⊗[R] R) → x)
      (Function.comp (β := ↥I ⊗[R] R) (⇑(rTensor R I.subtype) : (a : ↥I ⊗[R] R) → x ⊗[R] R)
        (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (LinearEquiv.symm (TensorProduct.rid R ↥I)))) :
          (a : ↥I) → ↥I ⊗[R] R)))

Tactic:
convert! Subtype.coe_injective using 1

Premises used: Subtype.coe_injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
x : Type u
x_1 : AddCommMonoid x
x_2 : Module R x
h_1 : Module.Finite R x
I : Submodule R x
h_2 : I.FG
h :
  ∀ (x_3 : ↥I),
    Function.comp (β := x ⊗[R] R)
        (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (TensorProduct.rid R x))) : (a : x ⊗[R] R) → x)
        (Function.comp (β := ↥I ⊗[R] R) (⇑(rTensor R I.subtype) : (a : ↥I ⊗[R] R) → x ⊗[R] R)
          (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (LinearEquiv.symm (TensorProduct.rid R ↥I)))) :
            (a : ↥I) → ↥I ⊗[R] R))
        x_3 =
      (↑x_3 : x)
⊢ Eq (α := ↥I → x)
    (Function.comp (β := x ⊗[R] R)
      (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (TensorProduct.rid R x))) : (a : x ⊗[R] R) → x)
      (Function.comp (β := ↥I ⊗[R] R) (⇑(rTensor R I.subtype) : (a : ↥I ⊗[R] R) → x ⊗[R] R)
        (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (LinearEquiv.symm (TensorProduct.rid R ↥I)))) :
          (a : ↥I) → ↥I ⊗[R] R)))
    fun (a : ↥I) ↦ (↑a : x)

Tactic:
ext
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
x : Type u
x_1 : AddCommMonoid x
x_2 : Module R x
h : Module.Finite R x
I : Submodule R x
h_1 : I.FG
x_3 : ↥I
⊢ Function.comp (β := x ⊗[R] R)
      (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (TensorProduct.rid R x))) : (a : x ⊗[R] R) → x)
      (Function.comp (β := ↥I ⊗[R] R) (⇑(rTensor R I.subtype) : (a : ↥I ⊗[R] R) → x ⊗[R] R)
        (⇑(AddEquiv.toEquiv (LinearEquiv.toAddEquiv (LinearEquiv.symm (TensorProduct.rid R ↥I)))) :
          (a : ↥I) → ↥I ⊗[R] R))
      x_3 =
    (↑x_3 : x)

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : Flat R M
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
rw :
  ∀
    (f :
      ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P),
        Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M))
    (i : N →ₗ[R] M) (r : M →ₗ[R] N) (h : r ∘ₗ i = LinearMap.id) ⦃P : Type u⦄ [inst_5 : AddCommMonoid P]
    [inst_6 : Module R P] (N_1 : Submodule R P),
    Injective (α := ↥N_1 ⊗[R] N) (β := P ⊗[R] N) (⇑(rTensor N N_1.subtype) : (a : ↥N_1 ⊗[R] N) → P ⊗[R] N)
⊢ Flat R N

Tactic:
rw [iff_rTensor_injectiveₛ] at *

Premises used: Module.Flat.iff_rTensor_injectiveₛ
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P),
    Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
⊢ ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N_1 : Submodule R P),
    Injective (α := ↥N_1 ⊗[R] N) (β := P ⊗[R] N) (⇑(rTensor N N_1.subtype) : (a : ↥N_1 ⊗[R] N) → P ⊗[R] N)

Tactic:
fun P _ _ Q ↦ .of_comp (f := lTensor P i) ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P),
    Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
refine :
  ∀ (P : Type u) (x : AddCommMonoid P) (x_1 : Module R P) (Q : Submodule R P),
    Injective (α := ↥Q ⊗[R] N) (β := P ⊗[R] M)
      (Function.comp (β := P ⊗[R] N) (⇑(lTensor P i) : (a : P ⊗[R] N) → P ⊗[R] M)
        (⇑(rTensor N Q.subtype) : (a : ↥Q ⊗[R] N) → P ⊗[R] N))
⊢ ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N_1 : Submodule R P),
    Injective (α := ↥N_1 ⊗[R] N) (β := P ⊗[R] N) (⇑(rTensor N N_1.subtype) : (a : ↥N_1 ⊗[R] N) → P ⊗[R] N)

Tactic:
refine fun P _ _ Q ↦ .of_comp (f := lTensor P i) ?_
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P),
    Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x : AddCommMonoid P
x_1 : Module R P
Q : Submodule R P
rw :
  Injective (α := ↥Q ⊗[R] N) (β := P ⊗[R] M)
    (Function.comp (β := ↥Q ⊗[R] M) (⇑(rTensor M Q.subtype) : (a : ↥Q ⊗[R] M) → P ⊗[R] M)
      (⇑(lTensor (↥Q) i) : (a : ↥Q ⊗[R] N) → ↥Q ⊗[R] M))
⊢ Injective (α := ↥Q ⊗[R] N) (β := P ⊗[R] M)
    (Function.comp (β := P ⊗[R] N) (⇑(lTensor P i) : (a : P ⊗[R] N) → P ⊗[R] M)
      (⇑(rTensor N Q.subtype) : (a : ↥Q ⊗[R] N) → P ⊗[R] N))

Tactic:
rw [← coe_comp, lTensor_comp_rTensor, ← rTensor_comp_lTensor, coe_comp]

Premises used: LinearMap.rTensor_comp_lTensor, LinearMap.lTensor_comp_rTensor, LinearMap.coe_comp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P),
    Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x : AddCommMonoid P
x_1 : Module R P
Q : Submodule R P
⊢ Injective (α := ↥Q ⊗[R] N) (β := P ⊗[R] M)
    (Function.comp (β := ↥Q ⊗[R] M) (⇑(rTensor M Q.subtype) : (a : ↥Q ⊗[R] M) → P ⊗[R] M)
      (⇑(lTensor (↥Q) i) : (a : ↥Q ⊗[R] N) → ↥Q ⊗[R] M))

Tactic:
(f Q).comp (Function.RightInverse.injective (g := lTensor Q r) fun x ↦ ?_)

Premises used: Function.Injective.comp, Function.RightInverse.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P),
    Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x : AddCommMonoid P
x_1 : Module R P
Q : Submodule R P
refine :
  ∀ (x_2 : ↥Q ⊗[R] N),
    (lTensor (↥Q) r : (a : ↥Q ⊗[R] M) → ↥Q ⊗[R] N) ((lTensor (↥Q) i : (a : ↥Q ⊗[R] N) → ↥Q ⊗[R] M) x_2) = x_2
⊢ Injective (α := ↥Q ⊗[R] N) (β := P ⊗[R] M)
    (Function.comp (β := ↥Q ⊗[R] M) (⇑(rTensor M Q.subtype) : (a : ↥Q ⊗[R] M) → P ⊗[R] M)
      (⇑(lTensor (↥Q) i) : (a : ↥Q ⊗[R] N) → ↥Q ⊗[R] M))

Tactic:
refine (f Q).comp (Function.RightInverse.injective (g := lTensor Q r) fun x ↦ ?_)

Premises used: Function.Injective.comp, Function.RightInverse.injective
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f :
  ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P),
    Injective (α := ↥N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M N.subtype) : (a : ↥N ⊗[R] M) → P ⊗[R] M)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x_1 : AddCommMonoid P
x_2 : Module R P
Q : Submodule R P
x : ↥Q ⊗[R] N
⊢ (lTensor (↥Q) r : (a : ↥Q ⊗[R] M) → ↥Q ⊗[R] N) ((lTensor (↥Q) i : (a : ↥Q ⊗[R] N) → ↥Q ⊗[R] M) x) = x

Tactic:
simp [← comp_apply, ← lTensor_comp, h]

Premises used: LinearMap.comp_apply, LinearMap.lTensor_comp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Flat R M
e : N ≃ₗ[R] M
⊢ (↑e.symm : M →ₗ[R] N) ∘ₗ (↑e : N →ₗ[R] M) = LinearMap.id

Tactic:
simp
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ Flat R M ↔ Flat R N

Tactic:
⟨fun _ ↦ of_linearEquiv e.symm, fun _ ↦ of_linearEquiv e⟩

Premises used: LinearEquiv.symm, Iff.intro, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
inst_9 : Flat R M
⊢ Flat R (ULift.{v', v} M)

Tactic:
of_linearEquiv ULift.moduleEquiv

Premises used: ULift.moduleEquiv, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Flat R (ULift.{v', v} M)
⊢ Flat R M

Tactic:
of_linearEquiv ULift.moduleEquiv.symm

Premises used: LinearEquiv.symm, ULift.moduleEquiv, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
inst_9 : Small.{v', v} M
inst_10 : Flat R M
⊢ Flat.{u, v'} R (Shrink.{v', v} M)

Tactic:
of_linearEquiv (Shrink.linearEquiv R M)

Premises used: Shrink.linearEquiv, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Small.{v', v} M
inst_4 : Flat.{u, v'} R (Shrink.{v', v} M)
⊢ Flat R M

Tactic:
of_linearEquiv (Shrink.linearEquiv R M).symm

Premises used: LinearEquiv.symm, Shrink.linearEquiv, Module.Flat.of_linearEquiv
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
simp_rw :
  (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P) (i : ι),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat.{u, w} R (M i)

Tactic:
simp_rw [iff_rTensor_injectiveₛ, ← EquivLike.comp_injective _ (directSumRight R R _ _),
    ← LinearEquiv.coe_coe, ← coe_comp, directSumRight_comp_rTensor, coe_comp, LinearEquiv.coe_coe,
    EquivLike.injective_comp, lmap_injective]

Premises used: EquivLike.injective_comp, TensorProduct.directSumRight_comp_rTensor, EquivLike.comp_injective, TensorProduct.directSumRight, LinearMap.coe_comp, Module.Flat.iff_rTensor_injectiveₛ, DirectSum.lmap_injective, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
mp :
  (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P) (i : ι),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)) →
    ∀ (i : ι) ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
mpr :
  (∀ (i : ι) ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)) →
    ∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P) (i : ι),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
⊢ (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P) (i : ι),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P) (i : ι),
    Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
      (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
i : ι
P : Type u
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : Submodule R P
⊢ Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
    (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)

Tactic:
apply h
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst_5 : AddCommMonoid P] [inst_6 : Module R P] (N : Submodule R P),
    Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
      (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
P : Type u
inst_3 : AddCommMonoid P
inst_4 : Module R P
N : Submodule R P
i : ι
⊢ Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
    (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)

Tactic:
apply h
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
inst : CommSemiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
⊢ Flat R (Π₀ (i : ι), M i) ↔ ∀ (i : ι), Flat.{u, w} R (M i)

Tactic:
directSum_iff ..

Premises used: DirectSum, Module.Flat.directSum_iff
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M_1 : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
ι : Type v
M : ι → Type w
inst_9 : (i : ι) → AddCommMonoid (M i)
inst_10 : (i : ι) → Module.{u, w} R (M i)
inst_11 : ∀ (i : ι), Flat.{u, w} R (M i)
⊢ Flat R (⨁ (i : ι), M i)

Tactic:
directSum_iff.mpr ‹_›

Premises used: Iff.mpr, Module.Flat.directSum_iff