awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Tensor
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)
rw₃ rw₄ : Baer.{u, v} R (CharacterModule M) ↔ Baer.{u, v} R (CharacterModule M)
⊢ Flat R 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)]

Premises used: Module.Baer.iff_injective, CharacterModule.congr, Module.Baer.congr, Module.Flat.iff_characterModule_injective
-- Module: Mathlib.RingTheory.Flat.Tensor
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 M ↥I) (β := TensorProduct R M R)
        (⇑(lTensor M (Submodule.subtype I)) : (a : TensorProduct R M ↥I) → TensorProduct R M R)

Tactic:
simpa [← comm_comp_rTensor_comp_comm_eq] using iff_rTensor_injective'

Premises used: Module.Flat.iff_rTensor_injective', LinearMap.comm_comp_rTensor_comp_comm_eq
-- Module: Mathlib.RingTheory.Flat.Tensor
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)

Tactic:
iff_rTensor_injective'.trans ⟨fun h I _ ↦ h I,
    fun h I ↦ (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_⟩

Premises used: Iff.mpr, injective_iff_map_eq_zero, Iff.intro, Submodule.subtype, Iff.trans, Module.Flat.iff_rTensor_injective', LinearMap.rTensor
-- Module: Mathlib.RingTheory.Flat.Tensor
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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
⊢ 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)

Tactic:
refine iff_rTensor_injective'.trans ⟨fun h I _ ↦ h I,
    fun h I ↦ (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_⟩

Premises used: Iff.mpr, injective_iff_map_eq_zero, Iff.intro, Submodule.subtype, Iff.trans, Module.Flat.iff_rTensor_injective', LinearMap.rTensor
-- Module: Mathlib.RingTheory.Flat.Tensor
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)
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)
⊢ x = 0

Tactic:
obtain ⟨J, hfg, hle, y, rfl⟩ := Submodule.exists_fg_le_eq_rTensor_inclusion x

Premises used: Submodule.exists_fg_le_eq_rTensor_inclusion, rfl
-- Module: Mathlib.RingTheory.Flat.Tensor
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 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

Premises used: LinearMap.rTensor_comp_apply
-- Module: Mathlib.RingTheory.Flat.Tensor
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
rw₁ rw₂ : Eq (α := 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)

Tactic:
rw [(injective_iff_map_eq_zero _).mp (h hfg) y hx, map_zero]

Premises used: map_zero, injective_iff_map_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.Flat.Tensor
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 M ↥I) (β := TensorProduct R M R)
          (⇑(lTensor M (Submodule.subtype I)) : (a : TensorProduct R M ↥I) → TensorProduct R M R)

Tactic:
simpa [← comm_comp_rTensor_comp_comm_eq] using iff_rTensor_injective

Premises used: Module.Flat.iff_rTensor_injective, LinearMap.comm_comp_rTensor_comp_comm_eq
-- Module: Mathlib.RingTheory.Flat.Tensor
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) (β := M)
          (⇑(TensorProduct.lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → M)

Tactic:
simp [iff_rTensor_injective, ← lid_comp_rTensor]

Premises used: Module.Flat.iff_rTensor_injective, LinearMap.lid_comp_rTensor
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
⊢ 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
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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)
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
⊢ 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:
ext
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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)
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:
simp
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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)

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
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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)
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)
⊢ IsSMulRegular M r

Tactic:
rw [IsSMulRegular, h2]

Premises used: IsSMulRegular
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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)
⊢ 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:
simp [h, LinearEquiv.injective]

Premises used: LinearEquiv.injective
-- Module: Mathlib.RingTheory.Flat.TorsionFree
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Flat R M
⊢ IsTorsionFree R M

Tactic:
⟨fun _ hr ↦ isSMulRegular_of_isRegular hr⟩

Premises used: Module.Flat.isSMulRegular_of_isRegular, Module.IsTorsionFree.mk
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
hr₁ : IsRegular r
⊢ IsSMulRegular M r

Tactic:
apply isSMulRegular_of_isRegular

Premises used: Module.Flat.isSMulRegular_of_isRegular
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
⊢ IsRegular r

Tactic:
le_nonZeroDivisors_iff_isRegular.mp (le_refl R⁰) ⟨r, hr⟩

Premises used: le_refl, le_nonZeroDivisors_iff_isRegular, nonZeroDivisors, Subtype.mk, Iff.mp
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
⊢ IsRegular r

Tactic:
exact le_nonZeroDivisors_iff_isRegular.mp (le_refl R⁰) ⟨r, hr⟩

Premises used: le_refl, le_nonZeroDivisors_iff_isRegular, nonZeroDivisors, Subtype.mk, Iff.mp
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
rw : LE.le (α := Submodule R M) (torsion R M) ⊥
⊢ Eq (α := Submodule R M) (torsion R M) ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
m : M
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
h : Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r hr • m = 0
⊢ Eq.{u_2 + 1} (α := M) ((fun (x : M) ↦ r • x) m) ((fun (x : M) ↦ r • x) 0)

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
m : M
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
h : Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) R⁰ x) r hr • m = 0
⊢ Membership.mem (γ := Submodule R M) ⊥ m

Tactic:
exact isSMulRegular_of_nonZeroDivisors hr (by simpa using h)

Premises used: Module.Flat.isSMulRegular_of_nonZeroDivisors
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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) ⊥

Tactic:
⟨fun _ ↦ torsion_eq_bot, ?_⟩

Premises used: Module.Flat.torsion_eq_bot, Iff.intro
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
refine : Eq (α := Submodule R M) (torsion R M) ⊥ → Flat R M
⊢ Flat R M ↔ Eq (α := Submodule R M) (torsion R M) ⊥

Tactic:
refine ⟨fun _ ↦ torsion_eq_bot, ?_⟩
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
rw :
  ∀ ⦃I : Ideal R⦄,
    I.FG →
      Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
⊢ Flat R M

Tactic:
rw [iff_lift_lsmul_comp_subtype_injective]

Premises used: Module.Flat.iff_lift_lsmul_comp_subtype_injective
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
inl :
  ∀ (hFG : Ideal.FG.{u_1} (R := R) ⊥),
    Function.Injective (α := ↥⊥ ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype ⊥)) : (a : ↥⊥ ⊗[R] M) → M)
inr :
  ∀ (h : I ≠ ⊥),
    Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
⊢ Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)

Tactic:
obtain (rfl | h) := eq_or_ne I ⊥

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
hFG : Ideal.FG.{u_1} (R := R) ⊥
x y : ↥⊥ ⊗[R] M
⊢ x = y

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
⊢ Submodule.IsPrincipal I

Tactic:
have hprinc : I.IsPrincipal := IsBezout.isPrincipal_of_FG I hFG
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
rwa : ¬IsPrincipal.generator I = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ¬I = ⊥
⊢ IsPrincipal.generator I ≠ 0

Tactic:
rwa [ne_eq, ← IsPrincipal.eq_bot_iff_generator_eq_zero]

Premises used: ne_eq, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
⊢ IsPrincipal.generator I ≠ 0

Tactic:
have : IsPrincipal.generator I ≠ 0 := by
      rwa [ne_eq, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
apply :
  Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := ↥I ⊗[R] M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
      (⇑(LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)) : (a : R ⊗[R] M) → ↥I ⊗[R] M))
⊢ Function.Injective (α := ↥I ⊗[R] M) (β := M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)

Tactic:
apply Function.Injective.of_comp_right _
      (LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)).surjective

Premises used: Ideal.isoBaseOfIsPrincipal, LinearEquiv.rTensor, LinearEquiv.surjective, Function.Injective.of_comp_right
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
rw :
  Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
      (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))
⊢ Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := ↥I ⊗[R] M) (⇑(lift (lsmul R M ∘ₗ Submodule.subtype I)) : (a : ↥I ⊗[R] M) → M)
      (⇑(LinearEquiv.rTensor M (Ideal.isoBaseOfIsPrincipal h)) : (a : R ⊗[R] M) → ↥I ⊗[R] M))

Tactic:
rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp, LinearEquiv.coe_rTensor, rTensor,
      lift_comp_map, LinearMap.compl₂_id, LinearMap.comp_assoc,
      Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul,
      LinearMap.coe_comp]

Premises used: LinearMap.comp_assoc, TensorProduct.lift_comp_map, LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul, LinearMap.coe_comp, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, LinearEquiv.coe_toLinearMap, LinearMap.compl₂_id, LinearEquiv.coe_rTensor, LinearMap.rTensor
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : Eq (α := Submodule R M) (torsion R M) ⊥
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
rw :
  ∀ (htors : IsTorsionFree R M) ⦃I : Ideal R⦄ (hFG : I.FG) (h : I ≠ ⊥) (hprinc : Submodule.IsPrincipal I)
    (this : IsPrincipal.generator I ≠ 0),
    Function.Injective (α := R ⊗[R] M) (β := M)
      (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
        (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))
⊢ Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
      (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))

Tactic:
rw [← Submodule.isTorsionFree_iff_torsion_eq_bot] at htors

Premises used: Submodule.isTorsionFree_iff_torsion_eq_bot
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
      (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))

Tactic:
Function.Injective.comp (LinearMap.lsmul_injective this) ?_

Premises used: LinearMap.lsmul_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
refine : Function.Injective (α := R ⊗[R] M) (β := M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
⊢ Function.Injective (α := R ⊗[R] M) (β := M)
    (Function.comp (β := M) (⇑((lsmul R M : (a : R) → M →ₗ[R] M) (IsPrincipal.generator I) : M →ₗ[R] M) : (a : M) → M)
      (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M))

Tactic:
refine Function.Injective.comp (LinearMap.lsmul_injective this) ?_

Premises used: LinearMap.lsmul_injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
rw :
  Function.Injective.{u_2 + 1, u_2 + 1} (α := M) (β := M)
    (Function.comp (β := R ⊗[R] M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)
      (⇑(LinearEquiv.toEquiv (LinearEquiv.symm (TensorProduct.lid R M))) : (a : M) → R ⊗[R] M))
⊢ Function.Injective (α := R ⊗[R] M) (β := M) (⇑(lift (lsmul R M)) : (a : R ⊗[R] M) → M)

Tactic:
rw [← Equiv.injective_comp (TensorProduct.lid R M).symm.toEquiv]

Premises used: LinearEquiv.symm, Equiv.injective_comp, LinearEquiv.toEquiv, TensorProduct.lid
-- Module: Mathlib.RingTheory.Flat.TorsionFree
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
htors : IsTorsionFree R M
I : Ideal R
hFG : I.FG
h : I ≠ ⊥
hprinc : Submodule.IsPrincipal I
this : IsPrincipal.generator I ≠ 0
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := M) id

Tactic:
Function.injective_id

Premises used: Function.injective_id