awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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) (β := ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i))
      (Function.comp (β := P ⊗[R] ⨁ (i : ι), M i)
        (⇑(directSumRight R R P M : (P ⊗[R] ⨁ (i : ι), M i) ≃ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
          (a : P ⊗[R] ⨁ (i : ι), M i) → ⨁ (i : ι), P ⊗[R] 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)
-- 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)
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)
simp_rw₁ :
  (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := ↥N ⊗[R] ⨁ (i : ι), M i) (β := ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i))
        (Function.comp (β := P ⊗[R] ⨁ (i : ι), M i)
          (⇑(directSumRight R R P M : (P ⊗[R] ⨁ (i : ι), M i) ≃ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
            (a : P ⊗[R] ⨁ (i : ι), M i) → ⨁ (i : ι), P ⊗[R] 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)
⊢ 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) (β := ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i))
      (Function.comp (β := P ⊗[R] ⨁ (i : ι), M i)
        (⇑((↑(directSumRight R R P M) : (P ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
              (P ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
          (a : P ⊗[R] ⨁ (i : ι), M i) → ⨁ (i : ι), P ⊗[R] 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)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P_1 : 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_1
inst_6 : Module R P_1
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
S : Type u_4
inst_9 : CommSemiring S
inst_10 : Algebra R S
inst_11 : Module S M
inst_12 : IsScalarTower R S M
inst_13 : Flat S M
inst_14 : Flat R N
P : Type u_4
x : AddCommMonoid P
x_1 : Module S P
I : Submodule S P
this : Module S (RestrictScalars R S P) := RestrictScalars.moduleOrig R S P
⊢ Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := P ⊗[S] (M ⊗[R] N))
    (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → P ⊗[S] (M ⊗[R] N))
have change : ∀ (I : Submodule S (RestrictScalars R S P)),
  Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := P ⊗[S] (M ⊗[R] N))
    (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → P ⊗[S] (M ⊗[R] N))
Tactic: change Submodule S (RestrictScalars R S P) at I
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
N : Type u_1
P_1 : 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_1
inst_6 : Module R P_1
inst_7 : AddCommMonoid Q
inst_8 : Module R Q
S : Type u_4
inst_9 : CommSemiring S
inst_10 : Algebra R S
inst_11 : Module S M
inst_12 : IsScalarTower R S M
inst_13 : Flat S M
inst_14 : Flat R N
P : Type u_4
x : AddCommMonoid P
x_1 : Module S P
this : Module S (RestrictScalars R S P) := RestrictScalars.moduleOrig R S P
I : Submodule S (RestrictScalars R S P)
⊢ Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := P ⊗[S] (M ⊗[R] N))
    (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → P ⊗[S] (M ⊗[R] N))
have change : Injective (α := ↥I ⊗[S] (M ⊗[R] N)) (β := RestrictScalars R S P ⊗[S] (M ⊗[R] N))
  (⇑(rTensor (M ⊗[R] N) I.subtype) : (a : ↥I ⊗[S] (M ⊗[R] N)) → RestrictScalars R S P ⊗[S] (M ⊗[R] N))
Tactic: change Function.Injective (rTensor _ I.subtype)
-- 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
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent S (M := S ⊗[R] M) fun (x : ι) ↦ 1 ⊗ₜ[R] v x
have rw : Injective (α := ι →₀ S) (β := S ⊗[R] M)
  (⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ
        (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R))) :
    (a : ι →₀ S) → S ⊗[R] M)
Tactic: rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
    Finsupp.linearCombination_one_tmul]
-- 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
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent S (M := S ⊗[R] M) fun (x : ι) ↦ 1 ⊗ₜ[R] v x
have classical : Injective (α := ι →₀ S) (β := S ⊗[R] M)
  (⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ
        (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R))) :
    (a : ι →₀ S) → S ⊗[R] M)
Tactic: classical rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
    Finsupp.linearCombination_one_tmul]
-- 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
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
⊢ Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
have h : ∀ (x : M),
  Eq (α := S ⊗[R] M) (((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1 : (a : M) → S ⊗[R] M) x : S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
        (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M) x :
      S ⊗[R] M)
Tactic: ext
-- 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
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
⊢ Injective (α := M) (β := S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
have this : Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
  (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
    (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
Tactic: have : TensorProduct.mk R S M 1 =
      (Algebra.linearMap R S).rTensor M ∘ (TensorProduct.lid R M).symm := by ext; simp
-- 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
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
this :
  Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
⊢ Injective (α := M) (β := S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
have rw : Injective (α := M) (β := S ⊗[R] M)
  (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
    (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
Tactic: rw [this]
-- 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
S : Type u_4
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : FaithfulSMul R S
inst_6 : Flat R M
this :
  Eq (α := (a : M) → S ⊗[R] M) (⇑((TensorProduct.mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
⊢ Injective (α := M) (β := S ⊗[R] M)
    (Function.comp (β := R ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
      (⇑(LinearEquiv.symm (TensorProduct.lid R M)) : (a : M) → R ⊗[R] M))
have refine : Injective (α := R ⊗[R] M) (β := S ⊗[R] M) (⇑(rTensor M (Algebra.linearMap R S)) : (a : R ⊗[R] M) → S ⊗[R] M)
Tactic: refine Injective.comp ?_ (LinearEquiv.injective _)
-- 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
S : Type u_4
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : FaithfulSMul R S
inst_8 : Flat R N
f g : M →ₗ[R] N
h :
  Eq (α := S ⊗[R] M →ₗ[S] S ⊗[R] N)
    ((baseChangeHom R S M N : (a : M →ₗ[R] N) → S ⊗[R] M →ₗ[S] S ⊗[R] N) f : S ⊗[R] M →ₗ[S] S ⊗[R] N)
    ((baseChangeHom R S M N : (a : M →ₗ[R] N) → S ⊗[R] M →ₗ[S] S ⊗[R] N) g : S ⊗[R] M →ₗ[S] S ⊗[R] N)
⊢ f = g
have h₁ : ∀ (m : M), Eq.{u_1 + 1} (α := N) ((f : (a : M) → N) m : N) ((g : (a : M) → N) m : N)
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup 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 : AddCommGroup N] [inst_5 : AddCommGroup 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 : AddCommGroup N] [inst_5 : AddCommGroup 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 : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
exact1 :
  Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := TensorProduct.{u, v, u_2} R M (N' ⧸ f.range))
    (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] (N' ⧸ f.range))
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
    (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')
have rw : Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
  (⇑(lTensor M ι ∘ₗ lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] N'')
Tactic: rw [show g = ι.comp π from rfl, lTensor_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
⊢ Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
    (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')
have suffices : Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := TensorProduct.{u, v, u_2} R M (N' ⧸ f.range))
  (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N') (⇑(lTensor M π) : (a : M ⊗[R] N') → M ⊗[R] (N' ⧸ f.range))
Tactic: suffices exact1 : Function.Exact (f.lTensor M) (π.lTensor M) by
    rw [show g = ι.comp π from rfl, lTensor_comp]
    exact exact1.comp_injective _ (lTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
exact1 :
  Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := TensorProduct.{u, u_2, v} R (N' ⧸ f.range) M)
    (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M) (⇑(rTensor M π) : (a : N' ⊗[R] M) → (N' ⧸ f.range) ⊗[R] M)
⊢ Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
    (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
have rw : Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
  (⇑(rTensor M ι ∘ₗ rTensor M π) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
Tactic: rw [show g = ι.comp π from rfl, rTensor_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
N : Type u_1
N' : Type u_2
N'' : Type u_3
inst_4 : AddCommGroup N
inst_5 : AddCommGroup N'
inst_6 : AddCommGroup N''
inst_7 : Module R N
inst_8 : Module R N'
inst_9 : Module R N''
f : N →ₗ[R] N'
g : N' →ₗ[R] N''
exact : Function.Exact.{u_1, u_2, u_3} (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'')
π : N' →ₗ[R] N' ⧸ f.range := f.range.mkQ
ι : LinearMap.{u, u, u_2, u_3} (RingHom.id R) (N' ⧸ f.range) N'' :=
  g.range.subtype ∘ₗ
    (↑g.quotKerEquivRange : N' ⧸ g.ker →ₗ[R] ↥g.range) ∘ₗ
      (↑(f.range.quotEquivOfEq g.ker ⋯) : N' ⧸ f.range →ₗ[R] N' ⧸ g.ker)
⊢ Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
    (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
have suffices : Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := TensorProduct.{u, u_2, v} R (N' ⧸ f.range) M)
  (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M) (⇑(rTensor M π) : (a : N' ⊗[R] M) → (N' ⧸ f.range) ⊗[R] M)
Tactic: suffices exact1 : Function.Exact (f.rTensor M) (π.rTensor M) by
    rw [show g = ι.comp π from rfl, rTensor_comp]
    exact exact1.comp_injective _ (rTensor_preserves_injective_linearMap ι <| by
      simpa [ι, -Subtype.val_injective] using Subtype.val_injective) (map_zero _)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
          (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')
have refine : ∀
  (H :
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
          (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N''))
  (N' N'' : Type v') (x : AddCommGroup N') (x_1 : AddCommGroup N'') (x_2 : Module R N') (x_3 : Module R N'')
  (L : N' →ₗ[R] N'') (hL : Injective (α := N') (β := N'') (⇑L : (a : N') → N'')) (x_4 : M ⊗[R] N')
  (hx : Eq (α := M ⊗[R] N'') ((lTensor M L : (a : M ⊗[R] N') → M ⊗[R] N'') x_4 : M ⊗[R] N'') (0 : M ⊗[R] N'')),
  Membership.mem (γ := Submodule R (M ⊗[R] N')) ⊥ x_4
Tactic: refine ⟨fun _ ↦ lTensor_exact _, fun H ↦ iff_lTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ L hL ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
    [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
      Function.Exact (M := M ⊗[R] N) (N := M ⊗[R] N') (P := M ⊗[R] N'') (⇑(lTensor M f) : (a : M ⊗[R] N) → M ⊗[R] N')
        (⇑(lTensor M g) : (a : M ⊗[R] N') → M ⊗[R] N'')
N' N'' : Type v'
x_1 : AddCommGroup N'
x_2 : AddCommGroup N''
x_3 : Module R N'
x_4 : Module R N''
L : N' →ₗ[R] N''
hL : Injective (α := N') (β := N'') (⇑L : (a : N') → N'')
x_5 : M ⊗[R] N'
hx : Eq (α := M ⊗[R] N'') ((lTensor M L : (a : M ⊗[R] N') → M ⊗[R] N'') x_5 : M ⊗[R] N'') (0 : M ⊗[R] N'')
x : N'
⊢ Eq (α := N'') ((L : (a : N') → N'') x : N'') (0 : N'') ↔
    Membership.mem (γ := Set N') (Set.range (ι := PUnit.{v' + 1}) (⇑0 : (a : PUnit.{v' + 1}) → N')) x
have simp_rw : Eq (α := N'') ((L : (a : N') → N'') x : N'') (0 : N'') ↔ 0 = x
Tactic: simp_rw [Set.mem_range, LinearMap.zero_apply, exists_const]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{v', u} R
⊢ Flat R M ↔
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
          (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M)
have refine : ∀
  (H :
    ∀ ⦃N N' N'' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : AddCommGroup N'']
      [inst_7 : Module R N] [inst_8 : Module R N'] [inst_9 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
      Function.Exact (M := N) (N := N') (P := N'') (⇑f : (a : N) → N') (⇑g : (a : N') → N'') →
        Function.Exact (M := N ⊗[R] M) (N := N' ⊗[R] M) (P := N'' ⊗[R] M) (⇑(rTensor M f) : (a : N ⊗[R] M) → N' ⊗[R] M)
          (⇑(rTensor M g) : (a : N' ⊗[R] M) → N'' ⊗[R] M))
  (N' N'' : Type v') (x : AddCommGroup N') (x_1 : AddCommGroup N'') (x_2 : Module R N') (x_3 : Module R N'')
  (f : N' →ₗ[R] N'') (hf : Injective (α := N') (β := N'') (⇑f : (a : N') → N'')) (x_4 : N' ⊗[R] M)
  (hx : Eq (α := N'' ⊗[R] M) ((rTensor M f : (a : N' ⊗[R] M) → N'' ⊗[R] M) x_4 : N'' ⊗[R] M) (0 : N'' ⊗[R] M)),
  Membership.mem (γ := Submodule R (N' ⊗[R] M)) ⊥ x_4
Tactic: refine ⟨fun _ ↦ rTensor_exact _, fun H ↦ iff_rTensor_preserves_injective_linearMap'.mpr
    fun N' N'' _ _ _ _ f hf ↦ LinearMap.ker_eq_bot |>.mp <| eq_bot_iff |>.mpr
      fun x (hx : _ = 0) ↦ ?_⟩