awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Stability (goal)
Goal:
R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring Rp
inst_4 : Algebra R Rp
inst_5 : AddCommMonoid Mp
inst_6 : Module R Mp
inst_7 : Module Rp Mp
inst_8 : IsScalarTower R Rp Mp
inst_9 : Flat R M
S : Submonoid R
inst_10 : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ Flat Rp Mp
have fapply : IsBaseChange Rp f
Tactic: fapply Flat.isBaseChange (R := R) (M := M) (S := Rp) (N := Mp)
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Injective.{u, v} R (CharacterModule M) ↔
    ∀ ⦃N N' : Type v⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N] [inst_6 : Module R N']
      (f : N →ₗ[R] N'),
      Function.Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Function.Injective (α := TensorProduct R N M) (β := TensorProduct R N' M)
          (⇑(rTensor M f) : (a : TensorProduct R N M) → TensorProduct R N' M)
have simp_rw : (∀ ⦃X Y : Type v⦄ [inst_3 : AddCommGroup X] [inst_4 : AddCommGroup Y] [inst_5 : Module R X] [inst_6 : Module R Y]
    (f : X →ₗ[R] Y),
    Function.Injective (α := X) (β := Y) (⇑f : (a : X) → Y) →
      ∀ (g : X →ₗ[R] CharacterModule M),
        ∃ (h : Y →ₗ[R] CharacterModule M),
          ∀ (x : X) (x_1 : M),
            Eq (α := AddCircle (𝕜 := ℚ) 1)
              ((((h : (a : Y) → CharacterModule M) ((f : (a : X) → Y) x) : CharacterModule M) : (a : M) → AddCircle 1)
                  x_1 :
                AddCircle (𝕜 := ℚ) 1)
              ((((g : (a : X) → CharacterModule M) x : CharacterModule M) : (a : M) → AddCircle 1) x_1 :
                AddCircle (𝕜 := ℚ) 1)) ↔
  ∀ ⦃N N' : Type v⦄ [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup N'] [inst_5 : Module R N] [inst_6 : Module R N']
    (f : N →ₗ[R] N'),
    Function.Injective (α := N) (β := N') (⇑f : (a : N) → N') →
      ∀ (b : N →ₗ[R] CharacterModule M),
        ∃ (a : N' →ₗ[R] CharacterModule M),
          ∀ (x : N) (x_1 : M),
            Eq (α := AddCircle (𝕜 := ℚ) 1)
              ((((((lcomp R (CharacterModule M) f : (a : N' →ₗ[R] CharacterModule M) → N →ₗ[R] CharacterModule M) a :
                            N →ₗ[R] CharacterModule M) :
                          (a : N) → CharacterModule M)
                        x :
                      CharacterModule M) :
                    (a : M) → AddCircle 1)
                  x_1 :
                AddCircle (𝕜 := ℚ) 1)
              ((((b : (a : N) → CharacterModule M) x : CharacterModule M) : (a : M) → AddCircle 1) x_1 :
                AddCircle (𝕜 := ℚ) 1)
Tactic: simp_rw [injective_iff, rTensor_injective_iff_lcomp_surjective, Surjective, DFunLike.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (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 ↔ Injective.{u, v} R (CharacterModule M)
have rw : 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'),
    Function.Injective (α := N) (β := N') (⇑f : (a : N) → N') →
      Function.Injective (α := TensorProduct R N M) (β := TensorProduct R N' M)
        (⇑(rTensor M f) : (a : TensorProduct R N M) → TensorProduct R N' M)
Tactic: rw [injective_characterModule_iff_rTensor_preserves_injective_linearMap,
    iff_rTensor_preserves_injective_linearMap']
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (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
rw :
  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'),
      Function.Injective (α := N) (β := N') (⇑f : (a : N) → N') →
        Function.Injective (α := TensorProduct R N M) (β := TensorProduct R N' M)
          (⇑(rTensor M f) : (a : TensorProduct R N M) → TensorProduct R N' M)
⊢ Flat R M ↔ Injective.{u, v} R (CharacterModule M)
have 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'),
    Function.Injective (α := N) (β := N') (⇑f : (a : N) → N') →
      Function.Injective (α := TensorProduct R N M) (β := TensorProduct R N' M)
        (⇑(rTensor M f) : (a : TensorProduct R N M) → TensorProduct R N' 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'),
    Function.Injective (α := N) (β := N') (⇑f : (a : N) → N') →
      Function.Injective (α := TensorProduct R N M) (β := TensorProduct R N' M)
        (⇑(rTensor M f) : (a : TensorProduct R N M) → TensorProduct R N' M)
Tactic: rw [injective_characterModule_iff_rTensor_preserves_injective_linearMap,
    iff_rTensor_preserves_injective_linearMap']
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔ Baer.{u, v} R (CharacterModule M)
have rw : Flat R (ULift.{u, v} M) ↔ Baer.{u, v} R (CharacterModule M)
Tactic: rw [equiv_iff (N := ULift.{u} M) ULift.moduleEquiv.symm, iff_characterModule_injective,
    ← Baer.iff_injective, Baer.congr (CharacterModule.congr ULift.moduleEquiv)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : Flat R (ULift.{u, v} M) ↔ Baer.{u, v} R (CharacterModule M)
⊢ Flat R M ↔ Baer.{u, v} R (CharacterModule M)
have rw₁ : Injective R (CharacterModule (ULift.{u, v} M)) ↔ Baer.{u, v} R (CharacterModule M)
Tactic: rw [equiv_iff (N := ULift.{u} M) ULift.moduleEquiv.symm, iff_characterModule_injective,
    ← Baer.iff_injective, Baer.congr (CharacterModule.congr ULift.moduleEquiv)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : Flat R (ULift.{u, v} M) ↔ Baer.{u, v} R (CharacterModule M)
rw₁ : Injective R (CharacterModule (ULift.{u, v} M)) ↔ Baer.{u, v} R (CharacterModule M)
⊢ Flat R M ↔ Baer.{u, v} R (CharacterModule M)
have rw₂ : Baer R (CharacterModule (ULift.{u, v} M)) ↔ Baer.{u, v} R (CharacterModule M)
Tactic: rw [equiv_iff (N := ULift.{u} M) ULift.moduleEquiv.symm, iff_characterModule_injective,
    ← Baer.iff_injective, Baer.congr (CharacterModule.congr ULift.moduleEquiv)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : Flat R (ULift.{u, v} M) ↔ Baer.{u, v} R (CharacterModule M)
rw₁ : Injective R (CharacterModule (ULift.{u, v} M)) ↔ Baer.{u, v} R (CharacterModule M)
rw₂ : Baer R (CharacterModule (ULift.{u, v} M)) ↔ Baer.{u, v} R (CharacterModule M)
⊢ Flat R M ↔ Baer.{u, v} R (CharacterModule M)
have rw₃ : Baer.{u, v} R (CharacterModule M) ↔ Baer.{u, v} R (CharacterModule M)
Tactic: rw [equiv_iff (N := ULift.{u} M) ULift.moduleEquiv.symm, iff_characterModule_injective,
    ← Baer.iff_injective, Baer.congr (CharacterModule.congr ULift.moduleEquiv)]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
have simp_rw : Baer.{u, v} R (CharacterModule M) ↔
  ∀ (I : Ideal R),
    Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
      (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
Tactic: simp_rw [iff_characterModule_baer, Baer, rTensor_injective_iff_lcomp_surjective,
    Surjective, DFunLike.ext_iff, Subtype.forall, lcomp_apply, Submodule.subtype_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
simp_rw :
  Baer.{u, v} R (CharacterModule M) ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
⊢ Flat R M ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
have simp_rw₁ : (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
    ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
      ∀ (x : R) (mem : x ∈ I),
        Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
          ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
  ∀ (I : Ideal R),
    Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
      (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
Tactic: simp_rw [iff_characterModule_baer, Baer, rTensor_injective_iff_lcomp_surjective,
    Surjective, DFunLike.ext_iff, Subtype.forall, lcomp_apply, Submodule.subtype_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
simp_rw :
  Baer.{u, v} R (CharacterModule M) ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
simp_rw₁ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I),
          Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
            ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
⊢ Flat R M ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
have simp_rw₂ : (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
    ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
      ∀ (x : R) (mem : x ∈ I),
        Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
          ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
  ∀ (I : Ideal R),
    Surjective (α := LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)) (β :=
      LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M))
      (⇑(lcomp R (CharacterModule M) (Submodule.subtype I)) :
        (a : R →ₗ[R] CharacterModule M) → ↥I →ₗ[R] CharacterModule M)
Tactic: simp_rw [iff_characterModule_baer, Baer, rTensor_injective_iff_lcomp_surjective,
    Surjective, DFunLike.ext_iff, Subtype.forall, lcomp_apply, Submodule.subtype_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
simp_rw :
  Baer.{u, v} R (CharacterModule M) ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
simp_rw₁ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I),
          Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
            ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
simp_rw₂ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I),
          Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
            ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
    ∀ (I : Ideal R),
      Surjective (α := LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)) (β :=
        LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M))
        (⇑(lcomp R (CharacterModule M) (Submodule.subtype I)) :
          (a : R →ₗ[R] CharacterModule M) → ↥I →ₗ[R] CharacterModule M)
⊢ Flat R M ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
have simp_rw₃ : (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
    ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
      ∀ (x : R) (mem : x ∈ I),
        Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
          ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
  ∀ (I : Ideal R) (b : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
    ∃ (a : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
      (lcomp R (CharacterModule M) (Submodule.subtype I) : (a : R →ₗ[R] CharacterModule M) → ↥I →ₗ[R] CharacterModule M)
          a =
        b
Tactic: simp_rw [iff_characterModule_baer, Baer, rTensor_injective_iff_lcomp_surjective,
    Surjective, DFunLike.ext_iff, Subtype.forall, lcomp_apply, Submodule.subtype_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Flat R M ↔
    ∀ ⦃I : Ideal R⦄,
      I.FG →
        Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
          (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
have refine : ∀
  (h :
    ∀ ⦃I : Ideal R⦄,
      I.FG →
        Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
          (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M))
  (I : Ideal R) (x : TensorProduct R (↥I) M)
  (hx :
    Eq (α := TensorProduct R R M)
      ((rTensor M (Submodule.subtype I) : (a : TensorProduct R (↥I) M) → TensorProduct R R M) x : TensorProduct R R M)
      (0 : TensorProduct R R M)),
  x = 0
Tactic: refine iff_rTensor_injective'.trans ⟨fun h I _ ↦ h I,
    fun h I ↦ (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  ∀ ⦃I : Ideal R⦄,
    I.FG →
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
I : Ideal R
x : TensorProduct R (↥I) M
hx :
  Eq (α := TensorProduct R R M)
    ((rTensor M (Submodule.subtype I) : (a : TensorProduct R (↥I) M) → TensorProduct R R M) x : TensorProduct R R M)
    (0 : TensorProduct R R M)
⊢ x = 0
have obtain : ∀ (J : Submodule R R) (hfg : J.FG) (hle : J ≤ I) (y : TensorProduct R (↥J) M)
  (hx :
    Eq (α := TensorProduct R R M)
      ((rTensor M (Submodule.subtype I) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
          ((rTensor M (Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R (↥I) M) y) :
        TensorProduct R R M)
      (0 : TensorProduct R R M)),
  Eq (α := TensorProduct R (↥I) M)
    ((rTensor M (Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R (↥I) M) y :
      TensorProduct R (↥I) M)
    (0 : TensorProduct R (↥I) M)
Tactic: obtain ⟨J, hfg, hle, y, rfl⟩ := Submodule.exists_fg_le_eq_rTensor_inclusion x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (hypothesis)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  ∀ ⦃I : Ideal R⦄,
    I.FG →
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
I : Ideal R
J : Submodule R R
hfg : J.FG
hle : J ≤ I
y : TensorProduct R (↥J) M
hx :
  Eq (α := TensorProduct R R M)
    ((rTensor M (Submodule.subtype I) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
        ((rTensor M (Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R (↥I) M) y) :
      TensorProduct R R M)
    (0 : TensorProduct R R M)
⊢ Eq (α := TensorProduct R (↥I) M)
    ((rTensor M (Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R (↥I) M) y :
      TensorProduct R (↥I) M)
    (0 : TensorProduct R (↥I) M)
have hx₁ : Eq (α := TensorProduct R R M)
  ((rTensor M (Submodule.subtype I ∘ₗ Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R R M) y :
    TensorProduct R R M)
  (0 : TensorProduct R R M)
Tactic: rw [← rTensor_comp_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  ∀ ⦃I : Ideal R⦄,
    I.FG →
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
I : Ideal R
J : Submodule R R
hfg : J.FG
hle : J ≤ I
y : TensorProduct R (↥J) M
hx :
  Eq (α := TensorProduct R R M)
    ((rTensor M (Submodule.subtype I ∘ₗ Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R R M)
        y :
      TensorProduct R R M)
    (0 : TensorProduct R R M)
⊢ Eq (α := TensorProduct R (↥I) M)
    ((rTensor M (Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R (↥I) M) y :
      TensorProduct R (↥I) M)
    (0 : TensorProduct R (↥I) M)
have rw : Eq (α := TensorProduct R (↥I) M)
  ((rTensor M (Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R (↥I) M) 0) 0
Tactic: rw [(injective_iff_map_eq_zero _).mp (h hfg) y hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.Tensor (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  ∀ ⦃I : Ideal R⦄,
    I.FG →
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
I : Ideal R
J : Submodule R R
hfg : J.FG
hle : J ≤ I
y : TensorProduct R (↥J) M
hx :
  Eq (α := TensorProduct R R M)
    ((rTensor M (Submodule.subtype I ∘ₗ Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R R M)
        y :
      TensorProduct R R M)
    (0 : TensorProduct R R M)
rw :
  Eq (α := TensorProduct R (↥I) M)
    ((rTensor M (Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R (↥I) M) 0) 0
⊢ Eq (α := TensorProduct R (↥I) M)
    ((rTensor M (Submodule.inclusion hle) : (a : TensorProduct R (↥J) M) → TensorProduct R (↥I) M) y :
      TensorProduct R (↥I) M)
    (0 : TensorProduct R (↥I) M)
have rw₁ : Eq (α := TensorProduct R (↥I) M) 0 0
Tactic: rw [(injective_iff_map_eq_zero _).mp (h hfg) y hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
hr : IsRegular r
inst_3 : Flat R M
⊢ IsSMulRegular M r
have h : Function.Injective (α := R ⊗[R] M) (β := R ⊗[R] M) (⇑(rTensor M (toSpanSingleton R R r)) : (a : R ⊗[R] M) → R ⊗[R] M)
Tactic: have h := Flat.rTensor_preserves_injective_linearMap (M := M)
    (toSpanSingleton R R r) <| hr.right
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
hr : IsRegular r
inst_3 : Flat R M
h :
  Function.Injective (α := R ⊗[R] M) (β := R ⊗[R] M) (⇑(rTensor M (toSpanSingleton R R r)) : (a : R ⊗[R] M) → R ⊗[R] M)
⊢ Eq (α := (x : M) → M) (fun (x : M) ↦ r • x)
    (⇑((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
          rTensor M (toSpanSingleton R R r) ∘ₗ (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)) :
      (a : M) → M)
have h₁ : ∀ (x : M),
  r • x =
    ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
          rTensor M (toSpanSingleton R R r) ∘ₗ (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M) :
        (a : M) → M)
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
hr : IsRegular r
inst_3 : Flat R M
h :
  Function.Injective (α := R ⊗[R] M) (β := R ⊗[R] M) (⇑(rTensor M (toSpanSingleton R R r)) : (a : R ⊗[R] M) → R ⊗[R] M)
⊢ IsSMulRegular M r
have h2 : Eq (α := (x : M) → M) (fun (x : M) ↦ r • x)
  (⇑((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M (toSpanSingleton R R r) ∘ₗ (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)) :
    (a : M) → M)
Tactic: have h2 : (fun (x : M) ↦ r • x) = ((TensorProduct.lid R M) ∘ₗ
            (rTensor M (toSpanSingleton R R r)) ∘ₗ
            (TensorProduct.lid R M).symm) := by ext; simp
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
hr : IsRegular r
inst_3 : Flat R M
h :
  Function.Injective (α := R ⊗[R] M) (β := R ⊗[R] M) (⇑(rTensor M (toSpanSingleton R R r)) : (a : R ⊗[R] M) → R ⊗[R] M)
h2 :
  Eq (α := (x : M) → M) (fun (x : M) ↦ r • x)
    (⇑((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
          rTensor M (toSpanSingleton R R r) ∘ₗ (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)) :
      (a : M) → M)
⊢ IsSMulRegular M r
have rw : Function.Injective (α := M) (β := M)
  (⇑((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M (toSpanSingleton R R r) ∘ₗ (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)) :
    (a : M) → M)
Tactic: rw [IsSMulRegular, h2]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
inst_3 : Flat R M
⊢ IsSMulRegular M r
have hr₁ : IsRegular r
Tactic: apply isSMulRegular_of_isRegular
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
⊢ Eq (α := Submodule R M) (torsion R M) ⊥
have rw : LE.le (α := Submodule R M) (torsion R M) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.TorsionFree (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsBezout R
inst_4 : IsDomain R
⊢ Flat R M ↔ Eq (α := Submodule R M) (torsion R M) ⊥
have refine : Eq (α := Submodule R M) (torsion R M) ⊥ → Flat R M
Tactic: refine ⟨fun _ ↦ torsion_eq_bot, ?_⟩