mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i✝ : ι
x✝ : G i✝
⊢ ((Module.lift R ι G f (of R ι G f) ⋯ ∘ₗ lift R ι G f (Module.of R ι G f) ⋯) ∘ₗ of R ι G f i✝) x✝ =
    (LinearMap.id ∘ₗ of R ι G f i✝) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝¹ : DecidableEq ι
P : Type u_4
inst✝ : AddCommMonoid P
g : (i : ι) → G i →+ P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
F : DirectLimit G f →+ P
i j : ι
hij : i ≤ j
x : G i
⊢ (F.comp (of G f j)) ((f i j hij) x) = (F.comp (of G f i)) x

Tactic:
simp

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

Goal state before:
pp: ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝¹ : DecidableEq ι
P : Type u_4
inst✝ : AddCommMonoid P
F : DirectLimit G f →+ P
i✝ : ι
x✝ : G i✝
⊢ ((lift G f P (fun i ↦ F.comp (of G f i)) ⋯).comp (of G f i✝)) x✝ = (F.comp (of G f i✝)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝¹ : DecidableEq ι
P : Type u_4
inst✝ : AddCommMonoid P
g : (i : ι) → G i →+ P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
i j : ι
hij : i ≤ j
x : G i
⊢ (of G f j) ((f i j hij) x) = (of G f i) x

Tactic:
simp

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

Goal state before:
pp: ι : Type u_2
inst✝² : Preorder ι
G : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ ((lift G f (DirectLimit G f) (of G f) ⋯).comp (of G f i✝)) x✝ =
    ((AddMonoidHom.id (DirectLimit G f)).comp (of G f i✝)) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_2
inst✝² : Preorder ι
G : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝ : DecidableEq ι
i✝ : ι
x✝ : G i✝
⊢ ((map (fun x ↦ AddMonoidHom.id (G x)) ⋯).comp (of G f i✝)) x✝ =
    ((AddMonoidHom.id (DirectLimit G f)).comp (of G f i✝)) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_2
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝² : DecidableEq ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
G'' : ι → Type u_6
inst✝ : (i : ι) → AddCommMonoid (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j
g₁ : (i : ι) → G i →+ G' i
g₂ : (i : ι) → G' i →+ G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i✝ : ι
x✝ : G i✝
⊢ (((map g₂ hg₂).comp (map g₁ hg₁)).comp (of G f i✝)) x✝ = ((map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯).comp (of G f i✝)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : M
⊢ ((AlgebraTensorModule.curry (rTensor Q f ∘ₗ ↑(TensorProduct.comm R Q M))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q N) ∘ₗ lTensor Q f)) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : Q
x✝ : N
⊢ ((AlgebraTensorModule.curry (rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g)) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
s t : Set (σ →₀ ℕ)
x : σ →₀ ℕ
hx : x ∈ s
y : σ →₀ ℕ
hy : y ∈ t
⊢ (monomial (x + y)) 1 = (monomial x) 1 * (monomial y) 1

Tactic:
simp

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ C 1 = 1

Tactic:
simp

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:
simp

Goal state after:
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
⊢ 0 = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) 0).sum

Tactic:
simp

Goal state after:
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
x : M
y : N
⊢ x ⊗ₜ[R] y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) {(x, y)}).sum

Tactic:
simp

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

Goal state before:
pp: case add
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
x y : M ⊗[R] N
Sx : Multiset (M × N)
hx : x = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sx).sum
Sy : Multiset (M × N)
hy : y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) Sy).sum
⊢ ∃ S, x + y = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
exact ⟨Sx + Sy, by rw [Multiset.map_add, Multiset.sum_add, hx, hy]⟩

Goal state after:
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
⊢ 0 = Finsupp.sum 0 fun m n ↦ m ⊗ₜ[R] n

Tactic:
simp

Goal state after:
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
x : M
y : N
⊢ x ⊗ₜ[R] y = (Finsupp.single x y).sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
simp

Goal state after:
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
x y : M ⊗[R] N
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
Sy : M →₀ N
hy : y = Sy.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ (a : M), a ⊗ₜ[R] 0 = 0

Tactic:
simp

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

Goal state before:
pp: case h.hi
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
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, (a, S a) ∈ S.graph

Tactic:
simp

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

Goal state before:
pp: case h.hj
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
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.graph, a.1 ∈ S.support

Tactic:
simp

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

Goal state before:
pp: case h.left_neg
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
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, (a, S a).1 = a

Tactic:
simp

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

Goal state before:
pp: case h.right_neg
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
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.graph, (a.1, S a.1) = a

Tactic:
simp

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

Goal state before:
pp: case h.h
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
x : M ⊗[R] N
S : M →₀ N
h : x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∀ a ∈ S.support, a ⊗ₜ[R] S a = (a, S a).1 ⊗ₜ[R] (a, S a).2

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
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:
simp

Goal state after:
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
⊢ 0 = ∑ j, (fun a ↦ ⋯.elim a) j ⊗ₜ[R] (fun a ↦ ⋯.elim a) j

Tactic:
simp

Goal state after:
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
x : M
y : N
⊢ x ⊗ₜ[R] y = ∑ j, (fun x_1 ↦ x) j ⊗ₜ[R] (fun x ↦ y) j

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ (0 + 1) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: case right
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ 0 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ (0 + 1) = 0 ∧ 0 ^ 0 ≠ 0

Tactic:
constructor <;> simp

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.map (↑includeLeft) (RingHom.ker f) = Ideal.map (↑((map (AlgHom.id R A) g).comp includeLeft)) (RingHom.ker f)

Tactic:
Algebra.TensorProduct.map_comp_includeLeft

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
inst✝¹¹ : Ring A
inst✝¹⁰ : Ring B
inst✝⁹ : Ring C
inst✝⁸ : Ring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : Algebra S A
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
g : C →ₐ[R] D
hf : Function.Surjective ⇑f
hg : Function.Surjective ⇑g
this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)
⊢ Ideal.map (↑includeLeft) (RingHom.ker f) = Ideal.map (↑(includeLeft.comp (AlgHom.id R A))) (RingHom.ker f)
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: case zero
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
b : B
hb0 : ∀ (b_1 : B), b_1 * b = b * b_1
⊢ 0 * includeLeft b = includeLeft b * 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: case zero
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
⊢ 0 * includeRight c = includeRight c * 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: case tmul
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
c : C
hc0 : ∀ (b : C), b * c = c * b
b : B
c' : C
⊢ b ⊗ₜ[K] c' * includeRight c = includeRight c * b ⊗ₜ[K] c'

Tactic:
simp [hc0]

Goal state after:
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}.Finite

Tactic:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Flat R M
e : N ≃ₗ[R] M
⊢ ↑e.symm ∘ₗ ↑e = LinearMap.id

Tactic:
simp

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:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: case ha
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
e : A ≃ₐ[R] B
x✝¹ : A
x✝ : B
⊢ ((((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e))).comp
          Algebra.TensorProduct.includeLeft)
        x✝¹)
      x✝ =
    ((((↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A)).comp Algebra.TensorProduct.includeLeft) x✝¹)
      x✝

Tactic:
simp

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

Goal state before:
pp: case hb
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
e : A ≃ₐ[R] B
x✝¹ : Aᵐᵒᵖ
x✝ : B
⊢ (((AlgHom.restrictScalars R ((AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)))).comp
          Algebra.TensorProduct.includeRight)
        x✝¹)
      x✝ =
    (((AlgHom.restrictScalars R ((↑(LinearEquiv.conjAlgEquiv R ↑e)).comp (AlgHom.mulLeftRight R A))).comp
          Algebra.TensorProduct.includeRight)
        x✝¹)
      x✝

Tactic:
simp

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:
simp

Goal state after:
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:
simp

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

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₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
x : M
⊢ (hf.map hg LinearMap.id i) 0 = (⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm) 0

Tactic:
simp

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

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₁ : Type u_5
M₂ : Type u_6
N₂ : Type u_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
x : M
⊢ ∀ (x : M₁) (y : M₂),
    (hf.map hg LinearMap.id i) ((f x) y) = (⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm) ((f x) y)

Tactic:
simp

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

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₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₁
inst✝¹ : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₂
x : M
⊢ (hf.map hg i LinearMap.id) 0 = (⇑hg.equiv ∘ ⇑(LinearMap.rTensor M₂ i) ∘ ⇑hf.equiv.symm) 0

Tactic:
simp

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

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₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₁
inst✝¹ : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₂
x : M
⊢ ∀ (x : M₁) (y : M₂),
    (hf.map hg i LinearMap.id) ((f x) y) = (⇑hg.equiv ∘ ⇑(LinearMap.rTensor M₂ i) ∘ ⇑hf.equiv.symm) ((f x) y)

Tactic:
simp

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

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₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₁
inst✝² : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective ⇑i₁
h₂ : Function.Injective ⇑i₂
inst✝¹ : Module.Flat R M₂
inst✝ : Module.Flat R N₁
x : M
⊢ (hf.map hg i₁ i₂) 0 = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) 0

Tactic:
simp

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

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₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₁
inst✝² : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective ⇑i₁
h₂ : Function.Injective ⇑i₂
inst✝¹ : Module.Flat R M₂
inst✝ : Module.Flat R N₁
x : M
⊢ ∀ (x : M₁) (y : M₂), (hf.map hg i₁ i₂) ((f x) y) = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) ((f x) y)

Tactic:
simp

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

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₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₁
inst✝² : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective ⇑i₁
h₂ : Function.Injective ⇑i₂
inst✝¹ : Module.Flat R M₁
inst✝ : Module.Flat R N₂
x : M
⊢ (hf.map hg i₁ i₂) 0 = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) 0

Tactic:
simp

Goal state after: