mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ ↑Q ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ ↑Q ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Small.{u, u_1} R
P : Submodule R M
hP : P.FG
⊢ Small.{u, u_2} ↥P

Tactic:
rw [fg_iff_exists_fin_generating_family] at hP
  obtain ⟨n, s, rfl⟩ := hP
  rw [← Fintype.range_linearCombination]
  apply small_range

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case e'_2
R : Type u_1
inst✝² : CommRing R
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
I : Ideal R
x✝ : Q
⊢ ((AlgebraTensorModule.curry ((TensorProduct.mk R (R ⧸ I) Q) 1 ∘ₗ ↑(TensorProduct.lid R Q))) 1) x✝ =
    ((AlgebraTensorModule.curry (rTensor Q (mkQ I))) 1) x✝

Tactic:
;

Goal state after:
case e'_2
R : Type u_1
inst✝² : CommRing R
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
I : Ideal R
x✝ : Q
⊢ ((AlgebraTensorModule.curry ((TensorProduct.mk R (R ⧸ I) Q) 1 ∘ₗ ↑(TensorProduct.lid R Q))) 1) x✝ =
    ((AlgebraTensorModule.curry (rTensor Q (mkQ I))) 1) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(mapIncl M' N').range
hM : Submodule.map M₁.subtype M' ≤ M₁
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range

Tactic:
have hN := map_subtype_le N₁ N'

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(mapIncl M' N').range
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
⊢ ∃ M' N',
    ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁),
      Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(map (inclusion hM) (inclusion hN)).range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(map M'.subtype N'.subtype).range
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥M'
⊢ ↑(M'.subtype x✝) = ↑((inclusion hM ∘ₗ M₁.subtype.submoduleMap M') x✝)

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
h : s ⊆ ↑(map M'.subtype N'.subtype).range
hM : Submodule.map M₁.subtype M' ≤ M₁
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥M'
⊢ ↑(M'.subtype x✝) = ↑((inclusion hM ∘ₗ M₁.subtype.submoduleMap M') x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
h : s ⊆ ↑(map (inclusion hM ∘ₗ M₁.subtype.submoduleMap M') N'.subtype).range
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥N'
⊢ ↑(N'.subtype x✝) = ↑((inclusion hN ∘ₗ N₁.subtype.submoduleMap N') x✝)

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
M' : Submodule R ↥M₁
N' : Submodule R ↥N₁
left✝¹ : Module.Finite R ↥M'
left✝ : Module.Finite R ↥N'
hM : Submodule.map M₁.subtype M' ≤ M₁
h : s ⊆ ↑(map (inclusion hM ∘ₗ M₁.subtype.submoduleMap M') N'.subtype).range
hN : Submodule.map N₁.subtype N' ≤ N₁
x✝ : ↥N'
⊢ ↑(N'.subtype x✝) = ↑((inclusion hN ∘ₗ N₁.subtype.submoduleMap N') x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
w✝¹ : Submodule R M
N' : Submodule R N
w✝ : w✝¹ ≤ M₁
hN : N' ≤ N₁
left✝ : Module.Finite R ↥w✝¹
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(map (inclusion w✝) (inclusion hN)).range
⊢ s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN)).range

Tactic:
rw [← LinearMap.lTensor_comp_rTensor] at h

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
M₁ : Submodule R M
N₁ : Submodule R N
s : Set (↥M₁ ⊗[R] ↥N₁)
hs : s.Finite
w✝¹ : Submodule R M
N' : Submodule R N
w✝ : w✝¹ ≤ M₁
hN : N' ≤ N₁
left✝ : Module.Finite R ↥w✝¹
hfin : Module.Finite R ↥N'
h : s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN) ∘ₗ LinearMap.rTensor (↥N') (inclusion w✝)).range
⊢ s ⊆ ↑(LinearMap.lTensor (↥M₁) (inclusion hN)).range
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : s = univ
⊢ sInf {k | x ^ k = 0} = 0

Tactic:
;

Goal state after:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : s = univ
⊢ sInf {k | x ^ k = 0} = 0
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : {k | x ^ k = 0} = univ
⊢ sInf {k | x ^ k = 0} = 0

Tactic:
;

Goal state after:
R : Type u_1
x : R
inst✝² : Zero R
inst✝¹ : Pow R ℕ
inst✝ : Subsingleton R
s : Set ℕ := {k | x ^ k = 0}
this : {k | x ^ k = 0} = univ
⊢ sInf {k | x ^ k = 0} = 0
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
x y : N ⊗[R] M
eq : (rTensor M f) x = (rTensor M f) y
⊢ x = y

Tactic:
have ⟨N', Nfg, sub⟩ := Submodule.exists_fg_le_subset_range_rTensor_subtype {x, y} (by simp)

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
x y : N ⊗[R] M
eq : (rTensor M f) x = (rTensor M f) y
N' : Submodule R N
Nfg : N'.FG
sub : {x, y} ⊆ ↑(rTensor M N'.subtype).range
⊢ x = y
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
x y : N ⊗[R] M
eq : (rTensor M f) x = (rTensor M f) y
N' : Submodule R N
Nfg : N'.FG
sub : {x, y} ⊆ ↑(rTensor M N'.subtype).range
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := sub (.inl rfl)

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
y : N ⊗[R] M
N' : Submodule R N
Nfg : N'.FG
x : ↥N' ⊗[R] M
eq : (rTensor M f) ((rTensor M N'.subtype) x) = (rTensor M f) y
sub : {(rTensor M N'.subtype) x, y} ⊆ ↑(rTensor M N'.subtype).range
⊢ (rTensor M N'.subtype) x = y
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Small.{v', u} R
a✝ : Flat R M
N N' : Type v'
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N
inst✝ : Module R N'
f : N →ₗ[R] N'
⊢ Injective ⇑f → Injective ⇑(rTensor M f)

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Small.{v', u} R
a✝ : Flat R M
N N' : Type v'
inst✝³ : AddCommMonoid N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N
inst✝ : Module R N'
f : N →ₗ[R] N'
⊢ Injective ⇑f → Injective ⇑(rTensor M f)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁵ : Type u
x✝⁴ : AddCommMonoid x✝⁵
x✝³ : Module R x✝⁵
x✝² : Module.Finite R x✝⁵
I : Submodule R x✝⁵
x✝¹ : I.FG
x✝ : ↥I
⊢ (⇑(TensorProduct.rid R x✝⁵).toAddEquiv.toEquiv ∘
        ⇑(rTensor R I.subtype) ∘ ⇑(TensorProduct.rid R ↥I).symm.toAddEquiv.toEquiv)
      x✝ =
    ↑x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁵ : Type u
x✝⁴ : AddCommMonoid x✝⁵
x✝³ : Module R x✝⁵
x✝² : Module.Finite R x✝⁵
I : Submodule R x✝⁵
x✝¹ : I.FG
x✝ : ↥I
⊢ (⇑(TensorProduct.rid R x✝⁵).toAddEquiv.toEquiv ∘
        ⇑(rTensor R I.subtype) ∘ ⇑(TensorProduct.rid R ↥I).symm.toAddEquiv.toEquiv)
      x✝ =
    ↑x✝
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mp
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)

Tactic:
;

Goal state after:
case mp
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
i✝ : ι
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
⊢ Injective ⇑(rTensor (M i✝) N✝.subtype)

Tactic:
;

Goal state after:
case mp
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
i✝ : ι
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
⊢ Injective ⇑(rTensor (M i✝) N✝.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)

Tactic:
;

Goal state after:
case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
i✝ : ι
⊢ Injective ⇑(rTensor (M i✝) N✝.subtype)

Tactic:
;

Goal state after:
case mpr
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
i✝ : ι
⊢ Injective ⇑(rTensor (M i✝) N✝.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P✝ : Type u_2
Q : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P✝
inst✝⁸ : Module R P✝
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R Q
S : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : Flat S M
inst✝ : Flat R N
P : Type u_4
x✝¹ : AddCommMonoid P
x✝ : Module S P
I : Submodule S P
⊢ Injective ⇑(rTensor (M ⊗[R] N) I.subtype)

Tactic:
by
    let := RestrictScalars.moduleOrig R S P
    change Submodule S (RestrictScalars R S P) at I
    change Function.Injective (rTensor _ I.subtype)
    simpa [AlgebraTensorModule.rTensor_tensor] using!
      rTensor_preserves_injective_linearMap (.restrictScalars R <| I.subtype.rTensor M)
      (rTensor_preserves_injective_linearMap _ I.injective_subtype)

Goal state after:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R M
x✝ : M
⊢ ((TensorProduct.mk R S M) 1) x✝ = (⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm) x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_4
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : Flat R M
x✝ : M
⊢ ((TensorProduct.mk R S M) 1) x✝ = (⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm) x✝
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Small.{v', u} R
a✝ : Flat R M
N N' : Type v'
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N
inst✝ : Module R N'
f : N →ₗ[R] N'
⊢ Injective ⇑f → Injective ⇑(rTensor M f)

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Small.{v', u} R
a✝ : Flat R M
N N' : Type v'
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N
inst✝ : Module R N'
f : N →ₗ[R] N'
⊢ Injective ⇑f → Injective ⇑(rTensor M f)
Module: Mathlib.Algebra.Azumaya.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x✝ : Rᵐᵒᵖ
⊢ (((AlgHom.restrictScalars R ↑(tensorEquivEnd R)).comp Algebra.TensorProduct.includeRight) x✝) 1 =
    (((AlgHom.restrictScalars R (AlgHom.mulLeftRight R R)).comp Algebra.TensorProduct.includeRight) x✝) 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
x✝ : Rᵐᵒᵖ
⊢ (((AlgHom.restrictScalars R ↑(tensorEquivEnd R)).comp Algebra.TensorProduct.includeRight) x✝) 1 =
    (((AlgHom.restrictScalars R (AlgHom.mulLeftRight R R)).comp Algebra.TensorProduct.includeRight) x✝) 1
Module: Mathlib.Algebra.Azumaya.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Bijective ⇑↑(tensorEquivEnd R)

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Bijective ⇑↑(tensorEquivEnd R)
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
⊢ map₀ f 1 = 1

Tactic:
by rw [map₀, Pi.one_apply, one_def]

Goal state after:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
x✝ : A
⊢ includeLeft x✝ = (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : Module.Flat R A
hb : Function.Injective ⇑(algebraMap R B)
x✝ : A
⊢ includeLeft x✝ = (⇑(LinearMap.lTensor A (Algebra.linearMap R B)) ∘ ⇑(_root_.TensorProduct.rid R A).symm) x✝
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
x✝ : B
⊢ includeRight x✝ = (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) ∘ ⇑(_root_.TensorProduct.lid R B).symm) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Flat R B
ha : Function.Injective ⇑(algebraMap R A)
x✝ : B
⊢ includeRight x✝ = (⇑(LinearMap.rTensor B (Algebra.linearMap R A)) ∘ ⇑(_root_.TensorProduct.lid R B).symm) x✝
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst✝ : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
i : ι × κ
⊢ ((Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2) ∘ₗ Finsupp.lsingle i) 1 =
    ((map (Finsupp.linearCombination R v) (Finsupp.linearCombination R w) ∘ₗ ↑(finsuppTensorFinsupp' R ι κ).symm) ∘ₗ
        Finsupp.lsingle i)
      1

Tactic:
simp [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Goal state after:
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
a✝ : Nontrivial R
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
;

Goal state after:
R : Type u_1
n : Type u_2
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
a✝ : Nontrivial R
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: case hd
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
s : Finset α
inst✝ : Fintype β
f : α ↪ β
h✝ : Nonempty α
⊢ 0 < ↑(Fintype.card α)

Tactic:
exact mod_cast Fintype.card_pos

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x ^ ↑n.succ⟩⟧ = ⟦⟨i, x ^ ↑n * x⟩⟧

Tactic:
;

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x ^ ↑n.succ⟩⟧ = ⟦⟨i, x ^ ↑n * x⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ x ^ ↑n.succ = x ^ ↑n * x

Tactic:
;

Goal state after:
R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ x ^ ↑n.succ = x ^ ↑n * x