mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
r : R
⊢ ∃ a, (algebraMap R ↥⊥) a = ⟨(Algebra.ofId R S).toRingHom r, ⋯⟩

Tactic:
;

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
r : R
⊢ ∃ a, (algebraMap R ↥⊥) a = ⟨(Algebra.ofId R S).toRingHom r, ⋯⟩
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
x✝ : R
⊢ ((algebraMap (↥⊥) S).comp ↑(algebraMap R ↥⊥)) x✝ = ((↑(RingHom.id S)).comp (algebraMap R S)) x✝

Tactic:
;

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsAlgebraic (↥⊥) S
x✝ : R
⊢ ((algebraMap (↥⊥) S).comp ↑(algebraMap R ↥⊥)) x✝ = ((↑(RingHom.id S)).comp (algebraMap R S)) x✝
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
x : R
⊢ IsAlgebraic R ⟨(Algebra.ofId R S).toRingHom x, ⋯⟩

Tactic:
;

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : Nontrivial R
x : R
⊢ IsAlgebraic R ⟨(Algebra.ofId R S).toRingHom x, ⋯⟩
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : (aeval s) r ∈ R[s]
a✝ : ⟨(aeval s) r, ht⟩ ∈ ⊤
⊢ ↑((aeval ⟨s, ⋯⟩).toRingHom r) = ↑⟨(aeval s) r, ht⟩

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : (aeval s) r ∈ R[s]
a✝ : ⟨(aeval s) r, ht⟩ ∈ ⊤
⊢ ↑((aeval ⟨s, ⋯⟩).toRingHom r) = ↑⟨(aeval s) r, ht⟩
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
A : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : NoZeroDivisors S
inst✝⁴ : Algebra R S
alg : Algebra.IsAlgebraic R S
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
inj : Injective ⇑(algebraMap R A)
⊢ Injective ⇑(algebraMap S A)

Tactic:
by
  refine (injective_iff_map_eq_zero _).mpr fun s eq ↦ of_not_not fun ne ↦ ?_
  have ⟨r, ne, dvd⟩ := (alg.1 s).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero ne)
  refine ne (inj <| map_zero (algebraMap R A) ▸ zero_dvd_iff.mp ?_)
  simp_rw [← eq, IsScalarTower.algebraMap_apply R S A, map_dvd (algebraMap S A) dvd]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case mk
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
z : DirectLimit F f
a✝ : (i : ι) × F i
⊢ ∃ i x, Quot.mk (⇑(setoid f)) a✝ = ⟦⟨i, x⟩⟧

Tactic:
;

Goal state after:
case mk
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
z : DirectLimit F f
a✝ : (i : ι) × F i
⊢ ∃ i x, Quot.mk (⇑(setoid f)) a✝ = ⟦⟨i, x⟩⟧
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧
w✝² : ι
w✝¹ w✝ : F w✝²
⊢ C ⟦⟨w✝², w✝¹⟩⟧ ⟦⟨w✝², w✝⟩⟧

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧
w✝² : ι
w✝¹ w✝ : F w✝²
⊢ C ⟦⟨w✝², w✝¹⟩⟧ ⟦⟨w✝², w✝⟩⟧
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧
w✝³ : ι
w✝² w✝¹ w✝ : F w✝³
⊢ C ⟦⟨w✝³, w✝²⟩⟧ ⟦⟨w✝³, w✝¹⟩⟧ ⟦⟨w✝³, w✝⟩⟧

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧
w✝³ : ι
w✝² w✝¹ w✝ : F w✝³
⊢ C ⟦⟨w✝³, w✝²⟩⟧ ⟦⟨w✝³, w✝¹⟩⟧ ⟦⟨w✝³, w✝⟩⟧
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : ih i x = ih i y
⊢ ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧

Tactic:
;

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : ih i x = ih i y
⊢ ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧
Module: Mathlib.Algebra.Colimit.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq (Submodule R M)
N : { N // N.FG }
x✝ : ↥↑N
⊢ (↑(equiv R M) ∘ₗ of R { N // N.FG } (fun i ↦ ↥↑i) (fgSystem R M) N) x✝ = (↑N).subtype x✝

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq (Submodule R M)
N : { N // N.FG }
x✝ : ↥↑N
⊢ (↑(equiv R M) ∘ₗ of R { N // N.FG } (fun i ↦ ↥↑i) (fgSystem R M) N) x✝ = (↑N).subtype x✝
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ι
x✝¹ : G i✝
x✝ : M
⊢ (((mk R (G i✝) M).compr₂ₛₗ
          ((toDirectLimit f M ∘ₗ fromDirectLimit f M) ∘ₗ
            of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i✝))
        x✝¹)
      x✝ =
    (((mk R (G i✝) M).compr₂ₛₗ
          (LinearMap.id ∘ₗ of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i✝))
        x✝¹)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ι
x✝¹ : G i✝
x✝ : M
⊢ (((mk R (G i✝) M).compr₂ₛₗ
          ((toDirectLimit f M ∘ₗ fromDirectLimit f M) ∘ₗ
            of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i✝))
        x✝¹)
      x✝ =
    (((mk R (G i✝) M).compr₂ₛₗ
          (LinearMap.id ∘ₗ of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i✝))
        x✝¹)
      x✝
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 ι
s✝ : R
i✝ j✝ : ι
h✝ : i✝ ≤ j✝
x✝ : G i✝
⊢ Eqv f (s✝ • (DirectSum.lof R ι G i✝) x✝) (s✝ • (DirectSum.lof R ι G j✝) ((f i✝ j✝ h✝) x✝))

Tactic:
;

Goal state after:
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 ι
s✝ : R
i✝ j✝ : ι
h✝ : i✝ ≤ j✝
x✝ : G i✝
⊢ Eqv f (s✝ • (DirectSum.lof R ι G i✝) x✝) (s✝ • (DirectSum.lof R ι G j✝) ((f i✝ j✝ h✝) x✝))
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ι
x✝¹ : G i✝
x✝ : M
⊢ (((mk R (Module.DirectLimit G f) M).compr₂ₛₗ (fromDirectLimit f M ∘ₗ toDirectLimit f M) ∘ₗ of R ι G f i✝) x✝¹) x✝ =
    (((mk R (Module.DirectLimit G f) M).compr₂ₛₗ LinearMap.id ∘ₗ of R ι G f i✝) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
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
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ι
x✝¹ : G i✝
x✝ : M
⊢ (((mk R (Module.DirectLimit G f) M).compr₂ₛₗ (fromDirectLimit f M ∘ₗ toDirectLimit f M) ∘ₗ of R ι G f i✝) x✝¹) x✝ =
    (((mk R (Module.DirectLimit G f) M).compr₂ₛₗ LinearMap.id ∘ₗ of R ι G f i✝) x✝¹) x✝
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: case fst
ι✝ : Type u_1
inst✝² : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j✝ : ι✝
h : i✝ ≤ j✝
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : piLT X i × X i
j : ↑(Iio i)
⊢ ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f)).1 j = f.1 j

pp: case snd
ι✝ : Type u_1
inst✝² : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : piLT X i × X i
⊢ ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f)).2 = f.2

Tactic:
;

Goal state after:
case fst
ι✝ : Type u_1
inst✝² : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j✝ : ι✝
h : i✝ ≤ j✝
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : piLT X i × X i
j : ↑(Iio i)
⊢ ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f)).1 j = f.1 j

case snd
ι✝ : Type u_1
inst✝² : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : piLT X i × X i
⊢ ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f)).2 = f.2
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : G i ⊗[R] M
⊢ f i i ⋯ = LinearMap.id

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : G i ⊗[R] M
⊢ f i i ⋯ = LinearMap.id
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : G i ⊗[R] M
x✝ : G i
⊢ (f i i ⋯) x✝ = LinearMap.id x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : G i ⊗[R] M
x✝ : G i
⊢ (f i i ⋯) x✝ = LinearMap.id x✝
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝⁴ x✝³ x✝² : ι
x✝¹ : x✝² ≤ x✝³
x✝ : x✝³ ≤ x✝⁴
x : G x✝² ⊗[R] M
⊢ f x✝³ x✝⁴ x✝ ∘ₗ f x✝² x✝³ x✝¹ = f x✝² x✝⁴ ⋯

Tactic:
;

Goal state after:
case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝⁴ x✝³ x✝² : ι
x✝¹ : x✝² ≤ x✝³
x✝ : x✝³ ≤ x✝⁴
x : G x✝² ⊗[R] M
⊢ f x✝³ x✝⁴ x✝ ∘ₗ f x✝² x✝³ x✝¹ = f x✝² x✝⁴ ⋯
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝⁵ x✝⁴ x✝³ : ι
x✝² : x✝³ ≤ x✝⁴
x✝¹ : x✝⁴ ≤ x✝⁵
x : G x✝³ ⊗[R] M
x✝ : G x✝³
⊢ (f x✝⁴ x✝⁵ x✝¹ ∘ₗ f x✝³ x✝⁴ x✝²) x✝ = (f x✝³ x✝⁵ ⋯) x✝

Tactic:
;

Goal state after:
case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝⁵ x✝⁴ x✝³ : ι
x✝² : x✝³ ≤ x✝⁴
x✝¹ : x✝⁴ ≤ x✝⁵
x : G x✝³ ⊗[R] M
x✝ : G x✝³
⊢ (f x✝⁴ x✝⁵ x✝¹ ∘ₗ f x✝³ x✝⁴ x✝²) x✝ = (f x✝³ x✝⁵ ⋯) x✝
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : M ⊗[R] G i
⊢ f i i ⋯ = LinearMap.id

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : M ⊗[R] G i
⊢ f i i ⋯ = LinearMap.id
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : M ⊗[R] G i
x✝ : G i
⊢ (f i i ⋯) x✝ = LinearMap.id x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : M ⊗[R] G i
x✝ : G i
⊢ (f i i ⋯) x✝ = LinearMap.id x✝
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝² x✝¹ x✝ : ι
h₁ : x✝ ≤ x✝¹
h₂ : x✝¹ ≤ x✝²
x : M ⊗[R] G x✝
⊢ (LinearMap.lTensor M (f x✝¹ x✝² h₂)) ((LinearMap.lTensor M (f x✝ x✝¹ h₁)) x) = (LinearMap.lTensor M (f x✝ x✝² ⋯)) x

Tactic:
convert! ← (LinearMap.lTensor_comp_apply M _ _ x).symm

Goal state after:
case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝² x✝¹ x✝ : ι
h₁ : x✝ ≤ x✝¹
h₂ : x✝¹ ≤ x✝²
x : M ⊗[R] G x✝
⊢ f x✝¹ x✝² h₂ ∘ₗ f x✝ x✝¹ h₁ = f x✝ x✝² ⋯
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝² x✝¹ x✝ : ι
h₁ : x✝ ≤ x✝¹
h₂ : x✝¹ ≤ x✝²
x : M ⊗[R] G x✝
⊢ f x✝¹ x✝² h₂ ∘ₗ f x✝ x✝¹ h₁ = f x✝ x✝² ⋯

Tactic:
;

Goal state after:
case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝² x✝¹ x✝ : ι
h₁ : x✝ ≤ x✝¹
h₂ : x✝¹ ≤ x✝²
x : M ⊗[R] G x✝
⊢ f x✝¹ x✝² h₂ ∘ₗ f x✝ x✝¹ h₁ = f x✝ x✝² ⋯
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝³ x✝² x✝¹ : ι
h₁ : x✝¹ ≤ x✝²
h₂ : x✝² ≤ x✝³
x : M ⊗[R] G x✝¹
x✝ : G x✝¹
⊢ (f x✝² x✝³ h₂ ∘ₗ f x✝¹ x✝² h₁) x✝ = (f x✝¹ x✝³ ⋯) x✝

Tactic:
;

Goal state after:
case e'_3
R : Type u_1
inst✝⁷ : CommSemiring R
ι : Type u_2
inst✝⁶ : DecidableEq ι
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
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
x✝³ x✝² x✝¹ : ι
h₁ : x✝¹ ≤ x✝²
h₂ : x✝² ≤ x✝³
x : M ⊗[R] G x✝¹
x✝ : G x✝¹
⊢ (f x✝² x✝³ h₂ ∘ₗ f x✝¹ x✝² h₁) x✝ = (f x✝¹ x✝³ ⋯) x✝
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: case mk
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 ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (↑((addConGen (Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun (r • Quot.mk (⇑(moduleCon f).toSetoid) x) =
    (RingHom.id R) r •
      (↑((addConGen (Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun (Quot.mk (⇑(moduleCon f).toSetoid) x)

Tactic:
;

Goal state after:
case mk
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 ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
x✝ : DirectLimit G f
x : DirectSum ι G
⊢ (↑((addConGen (Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun (r • Quot.mk (⇑(moduleCon f).toSetoid) x) =
    (RingHom.id R) r •
      (↑((addConGen (Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun (Quot.mk (⇑(moduleCon f).toSetoid) x)
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 ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
i✝ : ι
x✝ : G i✝
⊢ (lift R ι G f (fun i ↦ F ∘ₗ of R ι G f i) ⋯ ∘ₗ of R ι G f i✝) x✝ = (F ∘ₗ of R ι G f i✝) x✝

Tactic:
;

Goal state after:
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 ι
P : Type u_4
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
F : DirectLimit G f →ₗ[R] P
i✝ : ι
x✝ : G i✝
⊢ (lift R ι G f (fun i ↦ F ∘ₗ of R ι G f i) ⋯ ∘ₗ of R ι G f i✝) x✝ = (F ∘ₗ of R ι G f i✝) x✝
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 ι
i✝ : ι
x✝ : G i✝
⊢ (lift R ι G f (of R ι G f) ⋯ ∘ₗ of R ι G f i✝) x✝ = (LinearMap.id ∘ₗ of R ι G f i✝) x✝

Tactic:
;

Goal state after:
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 ι
i✝ : ι
x✝ : G i✝
⊢ (lift R ι G f (of R ι G f) ⋯ ∘ₗ of R ι G f i✝) x✝ = (LinearMap.id ∘ₗ of R ι G f i✝) x✝