mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ a ⊗ₜ[R] ↑b ∈ ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
this

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b ∈ ↑(Submodule.restrictScalars R (map includeRight I))
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)
⊢ RingHom.ker (map f g) = Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.map includeRight (RingHom.ker g)

Tactic:
this

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)
⊢ RingHom.ker ((map f (AlgHom.id R D)).comp (map (AlgHom.id S A) g)) =
    Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.map includeRight (RingHom.ker g)
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))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
eq : (rTensor M f) ((rTensor M N'.subtype) x) = (rTensor M f) ((rTensor M N'.subtype) y)
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y

Tactic:
[

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))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
eq : (rTensor M f) ((rTensor M N'.subtype) x) = (rTensor M f) ((rTensor M N'.subtype) y)
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) 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))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
eq✝ :
  (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) x) =
    (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) y)
P' : Submodule R P
Pfg : P'.FG
le : Submodule.map f N' ≤ P'
eq :
  (rTensor M (inclusion le)) ((rTensor M (f.submoduleMap N')) x) =
    (rTensor M (inclusion le)) ((rTensor M (f.submoduleMap N')) y)
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y

Tactic:
[

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))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
eq✝ :
  (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) x) =
    (rTensor M (Submodule.map f N').subtype) ((rTensor M (f.submoduleMap N')) y)
P' : Submodule R P
Pfg : P'.FG
le : Submodule.map f N' ≤ P'
eq :
  (rTensor M (inclusion le)) ((rTensor M (f.submoduleMap N')) x) =
    (rTensor M (inclusion le)) ((rTensor M (f.submoduleMap N')) y)
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y
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
f : N →ₗ[R] P
hf : Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Injective ⇑(rTensor M f) ↔ Injective ⇑(rTensor M (↑e ∘ₗ f).range.subtype)

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
f : N →ₗ[R] P
hf : Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Injective ⇑(rTensor M f) ↔ Injective ⇑(rTensor M (↑e ∘ₗ f).range.subtype)
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
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(lTensor 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
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(lTensor M f)
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
⊢ Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(lTensor M N.subtype)

Tactic:
[

Goal state after:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(lTensor M N.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat R (M i)

Tactic:
[

Goal state after:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat R (M i)
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
this : ⇑((TensorProduct.mk R S M) 1) = ⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm
⊢ Injective ⇑((TensorProduct.mk R S M) 1)

Tactic:
this

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
this : ⇑((TensorProduct.mk R S M) 1) = ⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm
⊢ Injective (⇑(rTensor M (Algebra.linearMap R S)) ∘ ⇑(TensorProduct.lid R M).symm)
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
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(lTensor 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
⊢ Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(lTensor M f)
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : 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✝³ : (i : ι) → Star (G i)
inst✝² : Star C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), StarHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
i : ι
x : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (star ⟦⟨i, x⟩⟧) = star (DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧)

Tactic:
[

Goal state after:
ι : 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✝³ : (i : ι) → Star (G i)
inst✝² : Star C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), StarHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ : DirectLimit G f
i : ι
x : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (star ⟦⟨i, x⟩⟧) = star (DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, 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
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x✝ : M ⊗[R] N'
hx : (lTensor M L) x✝ = 0
x : N'
⊢ L x = 0 ↔ x ∈ Set.range ⇑0

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
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
L : N' →ₗ[R] N''
hL : Injective ⇑L
x✝ : M ⊗[R] N'
hx : (lTensor M L) x✝ = 0
x : N'
⊢ L x = 0 ↔ x ∈ Set.range ⇑0
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : 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✝³ : (i : ι) → Mul (G i)
inst✝² : Mul C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MulHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ * ⟦⟨i, y⟩⟧) =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ * DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧

Tactic:
[

Goal state after:
ι : 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✝³ : (i : ι) → Mul (G i)
inst✝² : Mul C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MulHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
x✝ y✝ : DirectLimit G f
i : ι
x y : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (⟦⟨i, x⟩⟧ * ⟦⟨i, y⟩⟧) =
    DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, x⟩⟧ * DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, y⟩⟧
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✝² : (i : ι) → Mul (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : Nonempty ι
r s : (i : ι) → G i
⊢ map₀ f (r * s) = map₀ f r * map₀ f s

Tactic:
[

Goal state after:
ι : 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✝² : (i : ι) → Mul (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : Nonempty ι
r s : (i : ι) → G i
⊢ map₀ f (r * s) = map₀ f r * map₀ f s
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
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ x ∈ Set.range ⇑0

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
H :
  ∀ ⦃N N' N'' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : AddCommGroup N'']
    [inst_3 : Module R N] [inst_4 : Module R N'] [inst_5 : Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(rTensor M f) ⇑(rTensor M g)
N' N'' : Type v'
x✝⁴ : AddCommGroup N'
x✝³ : AddCommGroup N''
x✝² : Module R N'
x✝¹ : Module R N''
f : N' →ₗ[R] N''
hf : Injective ⇑f
x✝ : N' ⊗[R] M
hx : (rTensor M f) x✝ = 0
x : N'
⊢ f x = 0 ↔ x ∈ Set.range ⇑0
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✝¹ : (i : ι) → CommMagma (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧ * ⟦⟨i, 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✝¹ : (i : ι) → CommMagma (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧ * ⟦⟨i, 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✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, 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✝¹ : (i : ι) → Semigroup (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, 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✝³ : (i : ι) → Mul (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarMul (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧) = star ⟦⟨i, x✝⟩⟧ * star ⟦⟨i, 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✝³ : (i : ι) → Mul (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarMul (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧) = star ⟦⟨i, x✝⟩⟧ * star ⟦⟨i, 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✝³ : (i : ι) → SMul R (G i)
inst✝² : SMul R C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
inst✝ : ∀ (i : ι), MulActionHomClass (H i) R (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
r : R
x✝ : DirectLimit G f
i : ι
x : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (r • ⟦⟨i, x⟩⟧) = r • DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, 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✝³ : (i : ι) → SMul R (G i)
inst✝² : SMul R C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
inst✝ : ∀ (i : ι), MulActionHomClass (H i) R (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
r : R
x✝ : DirectLimit G f
i : ι
x : G i
⊢ DirectLimit.lift f (fun x ↦ ⇑(g x)) h (r • ⟦⟨i, x⟩⟧) = r • DirectLimit.lift f (fun x ↦ ⇑(g x)) h ⟦⟨i, 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✝⁵ : Star R
inst✝⁴ : (i : ι) → Star (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : (i : ι) → SMul R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
inst✝ : ∀ (i : ι), StarModule R (G i)
r : R
i : ι
x : G i
⊢ star (r • ⟦⟨i, x⟩⟧) = star r • star ⟦⟨i, 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✝⁵ : Star R
inst✝⁴ : (i : ι) → Star (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : (i : ι) → SMul R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
inst✝ : ∀ (i : ι), StarModule R (G i)
r : R
i : ι
x : G i
⊢ star (r • ⟦⟨i, x⟩⟧) = star r • star ⟦⟨i, 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✝² : Monoid R
inst✝¹ : (i : ι) → MulAction R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
x✝² x✝¹ : R
i : ι
x✝ : G i
⊢ (x✝² * x✝¹) • ⟦⟨i, x✝⟩⟧ = x✝² • x✝¹ • ⟦⟨i, 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✝² : Monoid R
inst✝¹ : (i : ι) → MulAction R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
x✝² x✝¹ : R
i : ι
x✝ : G i
⊢ (x✝² * x✝¹) • ⟦⟨i, x✝⟩⟧ = x✝² • x✝¹ • ⟦⟨i, x✝⟩⟧