awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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) (β := 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)
have 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) sorry) : N →ₗ[R] ↥((↑e : P →ₗ[R] Q) ∘ₗ f).range))) :
      (a : N ⊗[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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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)
have 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)
Tactic: refine rTensor_injective_of_fg fun N P Nfg Pfg le ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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
⊢ 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)
have Nfg₁ : Module.Finite.{u, u_1} R ↥N
Tactic: rw [← Finite.iff_fg] at Nfg Pfg
Cleared hypotheses: Nfg, Pfg, le
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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
⊢ 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)
have Pfg₁ : Module.Finite.{u, u_2} R ↥P
Tactic: rw [← Finite.iff_fg] at Nfg Pfg
Cleared hypotheses: Nfg, Pfg, le
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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
⊢ 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)
have this : Small.{u, u_2} ↥P
Tactic: have := Finite.small R P
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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)
⊢ 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)
have this₁ : Module.Finite R (Shrink.{u, u_2} ↥P)
Tactic: have := Module.Finite.equiv se
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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 (α := 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)
have 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)
Tactic: rw [rTensor_injective_iff_subtype (fun _ _ ↦ (Subtype.ext <| hf <| Subtype.ext_iff.mp ·)) se]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (hypothesis)
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
⊢ Injective (α := ↥x_2 ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M x_2.subtype) : (a : ↥x_2 ⊗[R] M) → P ⊗[R] M)
have this : Small.{v', u} P
Tactic: have := Finite.small.{v'} R P
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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 (α := ↥x_2 ⊗[R] M) (β := P ⊗[R] M) (⇑(rTensor M x_2.subtype) : (a : ↥x_2 ⊗[R] M) → P ⊗[R] M)
have 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)
Tactic: rw [rTensor_injective_iff_subtype Subtype.val_injective (Shrink.linearEquiv R P).symm]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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
⊢ 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')
have 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')
Tactic: simp_rw [iff_rTensor_preserves_injective_linearMapₛ, LinearMap.lTensor_inj_iff_rTensor_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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 (α := M ⊗[R] ↥N) (β := M ⊗[R] P) (⇑(lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
have 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)
Tactic: simp_rw [iff_rTensor_injectiveₛ, LinearMap.lTensor_inj_iff_rTensor_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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 (α := ↥I ⊗[R] R) (β := x ⊗[R] R) (⇑(rTensor R I.subtype) : (a : ↥I ⊗[R] R) → x ⊗[R] R)
have 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)))
Tactic: rw [← (TensorProduct.rid R I).symm.injective_comp, ← (TensorProduct.rid R _).comp_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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 (α := ↥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)))
have 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)
Tactic: convert! Subtype.coe_injective using 1
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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
⊢ Flat R N
have 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)
Tactic: rw [iff_rTensor_injectiveₛ] at *
Cleared hypotheses: f, i, r, h
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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)
have 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))
Tactic: refine fun P _ _ Q ↦ .of_comp (f := lTensor P i) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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 (β := P ⊗[R] N) (⇑(lTensor P i) : (a : P ⊗[R] N) → P ⊗[R] M)
      (⇑(rTensor N Q.subtype) : (a : ↥Q ⊗[R] N) → P ⊗[R] N))
have 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))
Tactic: rw [← coe_comp, lTensor_comp_rTensor, ← rTensor_comp_lTensor, coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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))
have 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
Tactic: refine (f Q).comp (Function.RightInverse.injective (g := lTensor Q r) fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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)
⊢ (∀ ⦃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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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)
⊢ (∀ ⦃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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
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)
have simp_rw : (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
    Injective (α := ↥N ⊗[R] ⨁ (i : ι), M i) (β := P ⊗[R] ⨁ (i : ι), M i)
      (⇑(rTensor (⨁ (i : ι), M i) N.subtype) : (a : ↥N ⊗[R] ⨁ (i : ι), M i) → P ⊗[R] ⨁ (i : ι), 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: classical
  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]
  constructor <;> (intro h; intros; apply h)