awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
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
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
y : N ⊗[R] M
N' : Submodule R N
Nfg : N'.FG
x : TensorProduct.{u, u_1, v} R (↥N') M
eq :
  Eq (α := P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x) : P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) y : P ⊗[R] M)
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M) {y} ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
obtain :
  ∀ (y : TensorProduct.{u, u_1, v} R (↥N') M)
    (eq :
      Eq (α := P ⊗[R] M)
        ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x) : P ⊗[R] M)
        ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y) : P ⊗[R] M))
    (sub :
      insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
          (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
        (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))),
    Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
⊢ (rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x = y

Tactic:
obtain ⟨y, rfl⟩ := sub (.inr rfl)

Premises used: Or.inr, rfl
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
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
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
x y : TensorProduct.{u, u_1, v} R (↥N') M
eq :
  Eq (α := P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x) : P ⊗[R] M)
    ((rTensor M f : (a : N ⊗[R] M) → P ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y) : P ⊗[R] M)
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
⊢ Eq (α := P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      P ⊗[R] M)

Tactic:
simp_rw [← rTensor_comp_apply, show f ∘ₗ N'.subtype = (N'.map f).subtype ∘ₗ f.submoduleMap N'
    from rfl, rTensor_comp_apply] at eq

Premises used: LinearMap.rTensor_comp_apply, rfl
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
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
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
x y : TensorProduct.{u, u_1, v} R (↥N') M
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
eq :
  Eq (α := P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      P ⊗[R] M)
have :
  ∀ (P' : Submodule R P) (Pfg : P'.FG) (le : Submodule.map f N' ≤ P')
    (eq :
      Eq (α := TensorProduct.{u, u_2, v} R (↥P') M)
        ((rTensor M (inclusion le) : (a : ↥(Submodule.map f N') ⊗[R] M) → ↥P' ⊗[R] M)
            ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
          TensorProduct.{u, u_2, v} R (↥P') M)
        ((rTensor M (inclusion le) : (a : ↥(Submodule.map f N') ⊗[R] M) → ↥P' ⊗[R] M)
            ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
          TensorProduct.{u, u_2, v} R (↥P') M)),
    Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
⊢ Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)

Tactic:
have ⟨P', Pfg, le, eq⟩ := (Nfg.map _).exists_rTensor_fg_inclusion_eq eq
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
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
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
x y : TensorProduct.{u, u_1, v} R (↥N') M
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
eq_1 :
  Eq (α := P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      P ⊗[R] M)
P' : Submodule R P
Pfg : P'.FG
le : Submodule.map f N' ≤ P'
eq :
  Eq (α := TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le) : (a : ↥(Submodule.map f N') ⊗[R] M) → ↥P' ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le) : (a : ↥(Submodule.map f N') ⊗[R] M) → ↥P' ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      TensorProduct.{u, u_2, v} R (↥P') M)
⊢ Eq (α := TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le ∘ₗ f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M) x :
      TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le ∘ₗ f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M) y :
      TensorProduct.{u, u_2, v} R (↥P') M)

Tactic:
simp_rw [← rTensor_comp_apply] at eq

Premises used: LinearMap.rTensor_comp_apply
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
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
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG →
      P'.FG →
        ∀ (h : N' ≤ comap f P'),
          Injective (α := TensorProduct.{u, u_1, v} R (↥N') M) (β := TensorProduct.{u, u_2, v} R (↥P') M)
            (⇑(rTensor M (f.restrict h)) : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M)
N' : Submodule R N
Nfg : N'.FG
x y : TensorProduct.{u, u_1, v} R (↥N') M
sub :
  insert (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
      (singleton (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)) ⊆
    (↑(range (rTensor M N'.subtype)) : Set (N ⊗[R] M))
eq_1 :
  Eq (α := P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) x) :
      P ⊗[R] M)
    ((rTensor M (Submodule.map f N').subtype : (a : ↥(Submodule.map f N') ⊗[R] M) → P ⊗[R] M)
        ((rTensor M (f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥(Submodule.map f N') ⊗[R] M) y) :
      P ⊗[R] M)
P' : Submodule R P
Pfg : P'.FG
le : Submodule.map f N' ≤ P'
eq :
  Eq (α := TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le ∘ₗ f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M) x :
      TensorProduct.{u, u_2, v} R (↥P') M)
    ((rTensor M (inclusion le ∘ₗ f.submoduleMap N') : (a : ↥N' ⊗[R] M) → ↥P' ⊗[R] M) y :
      TensorProduct.{u, u_2, v} R (↥P') M)
rw rw₁ :
  Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)
⊢ Eq (α := N ⊗[R] M) ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) x : N ⊗[R] M)
    ((rTensor M N'.subtype : (a : ↥N' ⊗[R] M) → N ⊗[R] M) y : N ⊗[R] M)

Tactic:
rw [h _ _ Nfg Pfg (map_le_iff_le_comap.mp le) eq]

Premises used: Iff.mp, Submodule.map_le_iff_le_comap
-- 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
f : N →ₗ[R] P
hf : Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
e : P ≃ₗ[R] Q
simp_rw :
  Injective (α := N ⊗[R] M) (β := Q ⊗[R] M) (⇑(rTensor M ((↑e : P →ₗ[R] Q) ∘ₗ f)) : (a : N ⊗[R] M) → Q ⊗[R] M) ↔
    Injective (α := N ⊗[R] M) (β := Q ⊗[R] M)
      (⇑(rTensor M
            (((↑e : P →ₗ[R] Q) ∘ₗ f).range.subtype ∘ₗ
              (↑(LinearEquiv.ofInjective ((↑e : P →ₗ[R] Q) ∘ₗ f) ⋯) : N →ₗ[R] ↥((↑e : P →ₗ[R] Q) ∘ₗ f).range))) :
        (a : N ⊗[R] M) → Q ⊗[R] M)
⊢ Injective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M) ↔
    Injective (α := TensorProduct.{u, u_3, v} R (↥((↑e : P →ₗ[R] Q) ∘ₗ f).range) M) (β := Q ⊗[R] M)
      (⇑(rTensor M ((↑e : P →ₗ[R] Q) ∘ₗ f).range.subtype) : (a : ↥((↑e : P →ₗ[R] Q) ∘ₗ f).range ⊗[R] M) → Q ⊗[R] M)

Tactic:
simp_rw [← EquivLike.injective_comp <| (LinearEquiv.ofInjective (e.toLinearMap ∘ₗ f)
    (e.injective.comp hf)).rTensor M, ← EquivLike.comp_injective _ (e.rTensor M),
    ← LinearEquiv.coe_coe, ← coe_comp, LinearEquiv.coe_rTensor, ← rTensor_comp]

Premises used: EquivLike.injective_comp, LinearEquiv.rTensor, EquivLike.comp_injective, LinearMap.comp, LinearEquiv.toLinearMap, Function.Injective.comp, LinearEquiv.ofInjective, LinearMap.coe_comp, LinearMap.rTensor_comp, LinearEquiv.injective, LinearEquiv.coe_coe, LinearEquiv.coe_rTensor
-- 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
f : N →ₗ[R] P
hf : Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
e : P ≃ₗ[R] Q
⊢ Injective (α := N ⊗[R] M) (β := Q ⊗[R] M) (⇑(rTensor M ((↑e : P →ₗ[R] Q) ∘ₗ f)) : (a : N ⊗[R] M) → Q ⊗[R] M) ↔
    Injective (α := N ⊗[R] M) (β := Q ⊗[R] M)
      (⇑(rTensor M
            (((↑e : P →ₗ[R] Q) ∘ₗ f).range.subtype ∘ₗ
              (↑(LinearEquiv.ofInjective ((↑e : P →ₗ[R] Q) ∘ₗ f) ⋯) : N →ₗ[R] ↥((↑e : P →ₗ[R] Q) ∘ₗ f).range))) :
        (a : N ⊗[R] M) → Q ⊗[R] M)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
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 : Flat R M
f : N →ₗ[R] P
hf : Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Injective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M)

Tactic:
rTensor_injective_of_fg fun N P Nfg Pfg le ↦ ?_

Premises used: LinearMap.rTensor_injective_of_fg
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
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 : Flat R M
f : N →ₗ[R] P
hf : Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
refine :
  ∀ (N_1 : Submodule R N) (P_1 : Submodule R P) (Nfg : N_1.FG) (Pfg : P_1.FG) (le : N_1 ≤ comap f P_1),
    Injective (α := TensorProduct.{u, u_1, v} R (↥N_1) M) (β := TensorProduct.{u, u_2, v} R (↥P_1) M)
      (⇑(rTensor M (f.restrict le)) : (a : ↥N_1 ⊗[R] M) → ↥P_1 ⊗[R] M)
⊢ Injective (α := N ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → P ⊗[R] M)

Tactic:
refine rTensor_injective_of_fg fun N P Nfg Pfg le ↦ ?_

Premises used: LinearMap.rTensor_injective_of_fg
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N_1 : Type u_1
P_1 : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N_1
inst_4 : Module R N_1
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : Flat R M
f : N_1 →ₗ[R] P_1
hf : Injective.{u_1 + 1, u_2 + 1} (α := N_1) (β := P_1) (⇑f : (a : N_1) → P_1)
N : Submodule R N_1
P : Submodule R P_1
Nfg : N.FG
Pfg : P.FG
le : N ≤ comap f P
⊢ Module.Finite.{u, u_1} R ↥N

Tactic:
rw [← Finite.iff_fg] at Nfg Pfg

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N_1 : Type u_1
P_1 : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N_1
inst_4 : Module R N_1
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : Flat R M
f : N_1 →ₗ[R] P_1
hf : Injective.{u_1 + 1, u_2 + 1} (α := N_1) (β := P_1) (⇑f : (a : N_1) → P_1)
N : Submodule R N_1
P : Submodule R P_1
Nfg : N.FG
Pfg : P.FG
le : N ≤ comap f P
Nfg₁ : Module.Finite.{u, u_1} R ↥N
⊢ Module.Finite.{u, u_2} R ↥P

Tactic:
rw [← Finite.iff_fg] at Nfg Pfg

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N_1 : Type u_1
P_1 : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N_1
inst_4 : Module R N_1
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : Flat R M
f : N_1 →ₗ[R] P_1
hf : Injective.{u_1 + 1, u_2 + 1} (α := N_1) (β := P_1) (⇑f : (a : N_1) → P_1)
N : Submodule R N_1
P : Submodule R P_1
Nfg : N.FG
Pfg : P.FG
le : N ≤ comap f P
Nfg₁ : Module.Finite.{u, u_1} R ↥N
Pfg₁ : Module.Finite.{u, u_2} R ↥P
⊢ N ≤ comap f P

Tactic:
rw [← Finite.iff_fg] at Nfg Pfg

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N_1 : Type u_1
P_1 : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N_1
inst_4 : Module R N_1
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : Flat R M
f : N_1 →ₗ[R] P_1
hf : Injective.{u_1 + 1, u_2 + 1} (α := N_1) (β := P_1) (⇑f : (a : N_1) → P_1)
N : Submodule R N_1
P : Submodule R P_1
Nfg : Module.Finite.{u, u_1} R ↥N
Pfg : Module.Finite.{u, u_2} R ↥P
le : N ≤ comap f P
⊢ Small.{u, u_2} ↥P

Tactic:
have := Finite.small R P
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N_1 : Type u_1
P_1 : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N_1
inst_4 : Module R N_1
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : Flat R M
f : N_1 →ₗ[R] P_1
hf : Injective.{u_1 + 1, u_2 + 1} (α := N_1) (β := P_1) (⇑f : (a : N_1) → P_1)
N : Submodule R N_1
P : Submodule R P_1
Nfg : Module.Finite.{u, u_1} R ↥N
Pfg : Module.Finite.{u, u_2} R ↥P
le : N ≤ comap f P
this : Small.{u, u_2} ↥P
se : LinearEquiv.{u, u, u_2, u} (RingHom.id R) (↥P) (Shrink.{u, u_2} ↥P) := LinearEquiv.symm (Shrink.linearEquiv R ↥P)
⊢ Module.Finite R (Shrink.{u, u_2} ↥P)

Tactic:
have := Module.Finite.equiv se
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N_1 : Type u_1
P_1 : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N_1
inst_4 : Module R N_1
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : Flat R M
f : N_1 →ₗ[R] P_1
hf : Injective.{u_1 + 1, u_2 + 1} (α := N_1) (β := P_1) (⇑f : (a : N_1) → P_1)
N : Submodule R N_1
P : Submodule R P_1
Nfg : Module.Finite.{u, u_1} R ↥N
Pfg : Module.Finite.{u, u_2} R ↥P
le : N ≤ comap f P
this_1 : Small.{u, u_2} ↥P
se : LinearEquiv.{u, u, u_2, u} (RingHom.id R) (↥P) (Shrink.{u, u_2} ↥P) := LinearEquiv.symm (Shrink.linearEquiv R ↥P)
this : Module.Finite R (Shrink.{u, u_2} ↥P)
rw :
  Injective (α := ↥((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range ⊗[R] M) (β := Shrink.{u, u_2} ↥P ⊗[R] M)
    (⇑(rTensor M ((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range.subtype) :
      (a : ↥((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range ⊗[R] M) → Shrink.{u, u_2} ↥P ⊗[R] M)
⊢ Injective (α := TensorProduct.{u, u_1, v} R (↥N) M) (β := TensorProduct.{u, u_2, v} R (↥P) M)
    (⇑(rTensor M (f.restrict le)) : (a : ↥N ⊗[R] M) → ↥P ⊗[R] M)

Tactic:
rw [rTensor_injective_iff_subtype (fun _ _ ↦ (Subtype.ext <| hf <| Subtype.ext_iff.mp ·)) se]

Premises used: LinearMap.rTensor_injective_iff_subtype, Subtype.ext
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N_1 : Type u_1
P_1 : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N_1
inst_4 : Module R N_1
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : Flat R M
f : N_1 →ₗ[R] P_1
hf : Injective.{u_1 + 1, u_2 + 1} (α := N_1) (β := P_1) (⇑f : (a : N_1) → P_1)
N : Submodule R N_1
P : Submodule R P_1
Nfg : Module.Finite.{u, u_1} R ↥N
Pfg : Module.Finite.{u, u_2} R ↥P
le : N ≤ comap f P
this_1 : Small.{u, u_2} ↥P
se : LinearEquiv.{u, u, u_2, u} (RingHom.id R) (↥P) (Shrink.{u, u_2} ↥P) := LinearEquiv.symm (Shrink.linearEquiv R ↥P)
this : Module.Finite R (Shrink.{u, u_2} ↥P)
⊢ Injective (α := ↥((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range ⊗[R] M) (β := Shrink.{u, u_2} ↥P ⊗[R] M)
    (⇑(rTensor M ((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range.subtype) :
      (a : ↥((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range ⊗[R] M) → Shrink.{u, u_2} ↥P ⊗[R] M)

Tactic:
(flat_iff R M).mp ‹_› _ (Finite.iff_fg.mp inferInstance)

Premises used: inferInstance, Iff.mp, Module.Finite.iff_fg, Module.flat_iff
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N_1 : Type u_1
P_1 : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N_1
inst_4 : Module R N_1
inst_5 : AddCommMonoid P_1
inst_6 : Module R P_1
inst_7 : Flat R M
f : N_1 →ₗ[R] P_1
hf : Injective.{u_1 + 1, u_2 + 1} (α := N_1) (β := P_1) (⇑f : (a : N_1) → P_1)
N : Submodule R N_1
P : Submodule R P_1
Nfg : Module.Finite.{u, u_1} R ↥N
Pfg : Module.Finite.{u, u_2} R ↥P
le : N ≤ comap f P
this_1 : Small.{u, u_2} ↥P
se : LinearEquiv.{u, u, u_2, u} (RingHom.id R) (↥P) (Shrink.{u, u_2} ↥P) := LinearEquiv.symm (Shrink.linearEquiv R ↥P)
this : Module.Finite R (Shrink.{u, u_2} ↥P)
⊢ Injective (α := ↥((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range ⊗[R] M) (β := Shrink.{u, u_2} ↥P ⊗[R] M)
    (⇑(rTensor M ((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range.subtype) :
      (a : ↥((↑se : ↥P →ₗ[R] Shrink.{u, u_2} ↥P) ∘ₗ f.restrict le).range ⊗[R] M) → Shrink.{u, u_2} ↥P ⊗[R] M)

Tactic:
exact (flat_iff R M).mp ‹_› _ (Finite.iff_fg.mp inferInstance)

Premises used: inferInstance, Iff.mp, Module.Finite.iff_fg, Module.flat_iff
-- Module: Mathlib.RingTheory.Flat.Basic
Goal:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
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 : Flat R M
f : N →ₗ[R] P
hf : Injective.{u_1 + 1, u_2 + 1} (α := N) (β := P) (⇑f : (a : N) → P)
⊢ Injective (α := M ⊗[R] N) (β := M ⊗[R] P) (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] P)

Tactic:
(f.lTensor_inj_iff_rTensor_inj M).2 (rTensor_preserves_injective_linearMap f hf)

Premises used: Iff.mpr, LinearMap.lTensor_inj_iff_rTensor_inj, 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
inst_3 : Small.{v', u} R
h : 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 (α := N ⊗[R] M) (β := N' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)

Tactic:
apply rTensor_preserves_injective_linearMap

Premises used: 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
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
⊢ Small.{v', u} P

Tactic:
have := Finite.small.{v'} R P
-- 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
rw :
  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)
⊢ Injective (α := ↥x_2 ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M x_2.subtype) : (a : ↥x_2 ⊗[R] M) → P ⊗[R] M)

Tactic:
rw [rTensor_injective_iff_subtype Subtype.val_injective (Shrink.linearEquiv R P).symm]

Premises used: LinearEquiv.symm, LinearMap.rTensor_injective_iff_subtype, Shrink.linearEquiv