awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum (↑T : Type u)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (Hom.hom g).toAlgebra
algInst_2 : Algebra (↑S : Type u) (↑P : Type u) := (Hom.hom inl).toAlgebra
algInst_3 : Algebra (↑T : Type u) (↑P : Type u) := (Hom.hom inr).toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑P : Type u) := ((Hom.hom inl).comp (Hom.hom f)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑P : Type u) := ⋯
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ IsScalarTower.{u, u, u} (↑R : Type u) (↑T : Type u) (↑P : Type u)

Tactic:
have : IsScalarTower R T P := .of_algebraMap_eq' <| congr($(h.1.1).hom)
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum (↑T : Type u)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (Hom.hom g).toAlgebra
algInst_2 : Algebra (↑S : Type u) (↑P : Type u) := (Hom.hom inl).toAlgebra
algInst_3 : Algebra (↑T : Type u) (↑P : Type u) := (Hom.hom inr).toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑P : Type u) := ((Hom.hom inl).comp (Hom.hom f)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑P : Type u) := ⋯
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
this : IsScalarTower.{u, u, u} (↑R : Type u) (↑T : Type u) (↑P : Type u)
⊢ Algebra.IsPushout.{u, u, u, u} (↑R : Type u) (↑S : Type u) (↑T : Type u) (↑P : Type u)

Tactic:
have : Algebra.IsPushout R S T P := CommRingCat.isPushout_iff_isPushout.mp h
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum (↑T : Type u)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (Hom.hom g).toAlgebra
algInst_2 : Algebra (↑S : Type u) (↑P : Type u) := (Hom.hom inl).toAlgebra
algInst_3 : Algebra (↑T : Type u) (↑P : Type u) := (Hom.hom inr).toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑P : Type u) := ((Hom.hom inl).comp (Hom.hom f)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑P : Type u) := ⋯
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
this_1 : IsScalarTower.{u, u, u} (↑R : Type u) (↑T : Type u) (↑P : Type u)
this : Algebra.IsPushout.{u, u, u, u} (↑R : Type u) (↑S : Type u) (↑T : Type u) (↑P : Type u)
⊢ (Hom.hom inr).finrank x = (Hom.hom f).finrank (PrimeSpectrum.comap (Hom.hom g) x)

Tactic:
Algebra.rankAtStalk_eq_of_isPushout R S T P x

Premises used: CommRingCat.carrier, Algebra.rankAtStalk_eq_of_isPushout, RingHom.finrank
-- Module: Mathlib.RingTheory.Flat.Rank
Goal:
R S T P : CommRingCat
f : R ⟶ S
g : R ⟶ T
inl : S ⟶ P
inr : T ⟶ P
h : CategoryTheory.IsPushout f g inl inr
hf : (Hom.hom f).Flat
hfin : (Hom.hom f).Finite
x : PrimeSpectrum (↑T : Type u)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (Hom.hom g).toAlgebra
algInst_2 : Algebra (↑S : Type u) (↑P : Type u) := (Hom.hom inl).toAlgebra
algInst_3 : Algebra (↑T : Type u) (↑P : Type u) := (Hom.hom inr).toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑P : Type u) := ((Hom.hom inl).comp (Hom.hom f)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑P : Type u) := ⋯
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
this_1 : IsScalarTower.{u, u, u} (↑R : Type u) (↑T : Type u) (↑P : Type u)
this : Algebra.IsPushout.{u, u, u, u} (↑R : Type u) (↑S : Type u) (↑T : Type u) (↑P : Type u)
⊢ (Hom.hom inr).finrank x = (Hom.hom f).finrank (PrimeSpectrum.comap (Hom.hom g) x)

Tactic:
exact Algebra.rankAtStalk_eq_of_isPushout R S T P x

Premises used: CommRingCat.carrier, Algebra.rankAtStalk_eq_of_isPushout
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
rw :
  ∀ ⦃P : Type u⦄ [inst_9 : AddCommMonoid P] [inst_10 : Module R P] (N : Submodule R P),
    Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)
⊢ Flat R M

Tactic:
rw [Flat.iff_lTensor_injectiveₛ]

Premises used: Module.Flat.iff_lTensor_injectiveₛ
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
rw :
  Injective (α := M ⊗[S] (S ⊗[R] ↥N)) (β := M ⊗[S] (S ⊗[R] P))
    (⇑(((AlgebraTensorModule.lTensor S M :
                (S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) →ₗ[S] M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
              (a : S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) → M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P))
            (((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
                (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
              N.subtype) :
          M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
      (a : M ⊗[S] (S ⊗[R] ↥N)) → M ⊗[S] (S ⊗[R] P))
⊢ Injective (α := M ⊗[R] ↥N) (β := M ⊗[R] P) (⇑(LinearMap.lTensor M N.subtype) : (a : M ⊗[R] ↥N) → M ⊗[R] P)

Tactic:
rw [← coe_lTensor (A := S), ← EquivLike.injective_comp (cancelBaseChange R S S _ _),
    ← LinearEquiv.coe_coe, ← LinearMap.coe_comp, lTensor_comp_cancelBaseChange,
    LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_injective]

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange, EquivLike.injective_comp, TensorProduct.AlgebraTensorModule.coe_lTensor, EquivLike.comp_injective, LinearMap.coe_comp, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
hf :
  Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P)
    (⇑(((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
              (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
            N.subtype :
          S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
      (a : S ⊗[R] ↥N) → S ⊗[R] P)
⊢ Injective (α := M ⊗[S] (S ⊗[R] ↥N)) (β := M ⊗[S] (S ⊗[R] P))
    (⇑(((AlgebraTensorModule.lTensor S M :
                (S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) →ₗ[S] M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
              (a : S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) → M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P))
            (((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
                (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
              N.subtype) :
          M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
      (a : M ⊗[S] (S ⊗[R] ↥N)) → M ⊗[S] (S ⊗[R] P))

Tactic:
apply Flat.lTensor_preserves_injective_linearMap

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
hf : Injective (α := ↥N) (β := P) (⇑N.subtype : (a : ↥N) → P)
⊢ Injective (α := S ⊗[R] ↥N) (β := S ⊗[R] P)
    (⇑(((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
              (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
            N.subtype :
          S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
      (a : S ⊗[R] ↥N) → S ⊗[R] P)

Tactic:
apply Flat.lTensor_preserves_injective_linearMap

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
hf : Injective (α := ↥N) (β := P) (⇑N.subtype : (a : ↥N) → P)
⊢ Injective (α := M ⊗[S] (S ⊗[R] ↥N)) (β := M ⊗[S] (S ⊗[R] P))
    (⇑(((AlgebraTensorModule.lTensor S M :
                (S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) →ₗ[S] M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
              (a : S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) → M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P))
            (((AlgebraTensorModule.lTensor S S : (↥N →ₗ[R] P) →ₗ[R] S ⊗[R] ↥N →ₗ[S] S ⊗[R] P) :
                (a : ↥N →ₗ[R] P) → S ⊗[R] ↥N →ₗ[S] S ⊗[R] P)
              N.subtype) :
          M ⊗[S] (S ⊗[R] ↥N) →ₗ[S] M ⊗[S] (S ⊗[R] P)) :
      (a : M ⊗[S] (S ⊗[R] ↥N)) → M ⊗[S] (S ⊗[R] P))

Tactic:
iterate 2 apply Flat.lTensor_preserves_injective_linearMap

Premises used: Module.Flat.lTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
⊢ Injective (α := ↥N) (β := P) (⇑N.subtype : (a : ↥N) → P)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Flat R S
inst_8 : Flat S M
P : Type u
inst_9 : AddCommMonoid P
inst_10 : Module R P
N : Submodule R P
⊢ Injective (α := ↥N) (β := P) (⇑N.subtype : (a : ↥N) → P)

Tactic:
exact Subtype.val_injective

Premises used: Subtype.val_injective
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Flat (ULift.{t, u} R) M ↔ Flat R M

Tactic:
⟨fun h ↦ .trans _ (ULift R) _, fun h ↦ ?_⟩

Premises used: ULift, Module.Flat.trans, Iff.intro
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
refine : ∀ (h : Flat R M), Flat (ULift.{t, u} R) M
⊢ Flat (ULift.{t, u} R) M ↔ Flat R M

Tactic:
refine ⟨fun h ↦ .trans _ (ULift R) _, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Flat R M
⊢ Flat (ULift.{t, u} R) R

Tactic:
have : Module.Flat (ULift.{t} R) R := .of_ulift
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Flat R M
this : Flat (ULift.{t, u} R) R
x : (R A : Type u) → [inst : CommSemiring R] → [inst_3 : Semiring A] → [Algebra R A] → Algebra (ULift.{t, u} R) A :=
  ULift.algebra'
⊢ Flat (ULift.{t, u} R) M

Tactic:
.trans _ R _

Premises used: Module.Flat.trans
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Flat R M
this : Flat (ULift.{t, u} R) R
x : (R A : Type u) → [inst : CommSemiring R] → [inst_3 : Semiring A] → [Algebra R A] → Algebra (ULift.{t, u} R) A :=
  ULift.algebra'
⊢ Flat (ULift.{t, u} R) M

Tactic:
exact .trans _ R _
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Flat R (ULift.{t, w} M) ↔ Flat R M

Tactic:
Flat.equiv_iff ULift.moduleEquiv

Premises used: ULift.moduleEquiv, Module.Flat.equiv_iff
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Flat R M
⊢ Flat S (S ⊗[R] M)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Flat.Stability
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Flat R M
N : Type t
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : Module S N
inst_9 : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
⊢ Flat S N

Tactic:
of_linearEquiv (IsBaseChange.equiv h).symm

Premises used: LinearEquiv.symm, Module.Flat.of_linearEquiv, IsBaseChange.equiv
-- Module: Mathlib.RingTheory.Flat.Stability
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
apply : IsBaseChange (N := LocalizedModule S M) (Localization (M := R) S) (LocalizedModule.mkLinearMap S M)
⊢ Flat (Localization (M := R) S) (LocalizedModule S M)

Tactic:
apply Flat.isBaseChange (R := R) (S := Localization S)
    (f := LocalizedModule.mkLinearMap S M)

Premises used: Localization, Module.Flat.isBaseChange
-- Module: Mathlib.RingTheory.Flat.Stability
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
rw : IsLocalizedModule (M' := LocalizedModule S M) S (LocalizedModule.mkLinearMap S M)
⊢ IsBaseChange (N := LocalizedModule S M) (Localization (M := R) S) (LocalizedModule.mkLinearMap S M)

Tactic:
rw [← isLocalizedModule_iff_isBaseChange S]

Premises used: isLocalizedModule_iff_isBaseChange
-- Module: Mathlib.RingTheory.Flat.Stability
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
⊢ IsLocalizedModule (M' := LocalizedModule S M) S (LocalizedModule.mkLinearMap S M)

Tactic:
localizedModuleIsLocalizedModule S

Premises used: localizedModuleIsLocalizedModule
-- Module: Mathlib.RingTheory.Flat.Stability
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
⊢ IsLocalizedModule (M' := LocalizedModule S M) S (LocalizedModule.mkLinearMap S M)

Tactic:
exact localizedModuleIsLocalizedModule S

Premises used: localizedModuleIsLocalizedModule
-- Module: Mathlib.RingTheory.Flat.Stability
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
fapply : IsBaseChange Rp f
fapply₁ : M →ₗ[R] Mp
⊢ Flat Rp Mp

Tactic:
fapply Flat.isBaseChange (R := R) (M := M) (S := Rp) (N := Mp)

Premises used: Module.Flat.isBaseChange
-- Module: Mathlib.RingTheory.Flat.Stability
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
⊢ IsBaseChange Rp f

Tactic:
(isLocalizedModule_iff_isBaseChange S Rp f).mp h

Premises used: isLocalizedModule_iff_isBaseChange, Iff.mp
-- Module: Mathlib.RingTheory.Flat.Stability
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
A : Type u_3
inst_9 : CommSemiring A
inst_10 : Algebra R A
inst_11 : Flat R A
S : Submonoid R
⊢ Flat.{u, u_3} (Localization (M := R) S) (Localization (M := A) (Algebra.algebraMapSubmonoid A S))

Tactic:
of_isLocalizedModule _ S (IsScalarTower.toAlgHom R A _).toLinearMap

Premises used: AlgHom.toLinearMap, IsScalarTower.toAlgHom, Module.Flat.of_isLocalizedModule
-- Module: Mathlib.RingTheory.Flat.Tensor
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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)
⊢ 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)

Tactic:
simp_rw [injective_iff, rTensor_injective_iff_lcomp_surjective, Surjective, DFunLike.ext_iff]

Premises used: rTensor_injective_iff_lcomp_surjective, DFunLike.ext_iff, Module.injective_iff, Function.Surjective
-- Module: Mathlib.RingTheory.Flat.Tensor
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ (∀ ⦃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:
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
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)
rw₁ 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)
⊢ Flat R M ↔ Injective.{u, v} R (CharacterModule M)

Tactic:
rw [injective_characterModule_iff_rTensor_preserves_injective_linearMap,
    iff_rTensor_preserves_injective_linearMap']

Premises used: Module.Flat.iff_rTensor_preserves_injective_linearMap', Module.Flat.injective_characterModule_iff_rTensor_preserves_injective_linearMap