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

Goal state before:
pp: case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) (r, m).1
eq : C ↑m * X - C r = 0
⊢ x = 0

Tactic:
← eq_mk'_iff_mul_eq,

Goal state after:
case inr
R : Type u
S : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
M : Submonoid R
inst✝ : IsLocalization M S
x : S
hx : x ≠ 0
r : R
m : ↥M
h : x = mk' S (r, m).1 (r, m).2
eq : C ↑m * X - C r = 0
⊢ x = 0
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
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (g a)) (map (↑f) q) = 0
⊢ IsAlgebraic R a

Tactic:
refine ⟨q, fun h' ↦ by simp [h'] at h1, hg ?_⟩

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
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (g a)) (map (↑f) q) = 0
⊢ g ((aeval a) q) = g 0
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Subsingleton M
⊢ f = 1 • g

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Subsingleton M
x✝ : M
⊢ f x✝ = (1 • g) x✝
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
⊢ (algebraMap (↥⊥) S).comp ↑(algebraMap R ↥⊥) = (↑(RingHom.id S)).comp (algebraMap R S)

Tactic:
ext

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_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : b ∈ S⁰
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S) r = b * s
⊢ r • a = b * (s * a)

Tactic:
rw [smul_def, h, mul_assoc]

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

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.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 }
⊢ ↑(equiv R M) ∘ₗ of R { N // N.FG } (fun i ↦ ↥↑i) (fgSystem R M) N = (↑N).subtype

Tactic:
ext

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
⊢ toDirectLimit f M ∘ₗ fromDirectLimit f M = LinearMap.id

Tactic:
ext

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.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
⊢ fromDirectLimit f M ∘ₗ toDirectLimit f M = LinearMap.id

Tactic:
ext

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.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:
ext

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

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

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

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: 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
⊢ lift R ι G f (fun i ↦ F ∘ₗ of R ι G f i) ⋯ = F

Tactic:
ext

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 ι
⊢ lift R ι G f (of R ι G f) ⋯ = LinearMap.id

Tactic:
ext

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✝
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 ι
⊢ map (fun x ↦ LinearMap.id) ⋯ = LinearMap.id

Tactic:
ext

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✝
⊢ (map (fun x ↦ LinearMap.id) ⋯ ∘ₗ of R ι G f i✝) x✝ = (LinearMap.id ∘ₗ 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 ι
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
⊢ map g₂ hg₂ ∘ₗ map g₁ hg₁ = map (fun i ↦ g₂ i ∘ₗ g₁ i) ⋯

Tactic:
ext

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 ι
G' : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (G' i)
inst✝² : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
G'' : ι → Type u_6
inst✝¹ : (i : ι) → AddCommMonoid (G'' i)
inst✝ : (i : ι) → Module R (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j
g₁ : (i : ι) → G i →ₗ[R] G' i
g₂ : (i : ι) → G' i →ₗ[R] G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i
hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i
i✝ : ι
x✝ : G i✝
⊢ ((map g₂ hg₂ ∘ₗ map g₁ hg₁) ∘ₗ of R ι G f i✝) x✝ = (map (fun i ↦ g₂ i ∘ₗ g₁ i) ⋯ ∘ₗ of R ι G f i✝) x✝
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : 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✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
⊢ (fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) t) = t

Tactic:
ext

Goal state after:
ι✝ : 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✝ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
equiv : (j : ↑(Iio i)) → F ↑j ≃ piLT X ↑j
nat : IsNatEquiv f equiv
t : ↑(limit f i)
x✝ : ↑(Iio i)
⊢ ↑((fun t ↦ ⟨fun l ↦ (equiv l).symm (↑t l), ⋯⟩) ((fun t ↦ ⟨fun l ↦ (equiv l) (↑t l), ⋯⟩) t)) x✝ = ↑t 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 ι
G' : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (G' i)
inst✝ : (i : ι) → Module R (G' i)
f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j
e : (i : ι) → G i ≃ₗ[R] G' i
he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)
i✝ : ι
g : G' i✝
i j : ι
h : i ≤ j
⊢ ↑(e j).symm ∘ₗ f' i j h = f i j h ∘ₗ ↑(e i).symm

Tactic:
rw [toLinearMap_symm_comp_eq, ← comp_assoc, he i, comp_assoc, comp_coe, symm_trans_self,
      refl_toLinearMap, comp_id]

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)
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)
⊢ lift R ι G f (Module.of R ι G f) ⋯ ∘ₗ Module.lift R ι G f (of R ι G f) ⋯ = LinearMap.id

Tactic:
ext

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 ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i✝ : ι
x✝ : G i✝
⊢ ((lift R ι G f (Module.of R ι G f) ⋯ ∘ₗ Module.lift R ι G f (of R ι G f) ⋯) ∘ₗ Module.of R ι G f i✝) x✝ =
    (LinearMap.id ∘ₗ Module.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 ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
⊢ Module.lift R ι G f (of R ι G f) ⋯ ∘ₗ lift R ι G f (Module.of R ι G f) ⋯ = LinearMap.id

Tactic:
ext

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 ι
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✝
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
⊢ lift G f P (fun i ↦ F.comp (of G f i)) ⋯ = F

Tactic:
ext

Goal state after:
ι : 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✝
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 ι
⊢ lift G f (DirectLimit G f) (of G f) ⋯ = AddMonoidHom.id (DirectLimit G f)

Tactic:
ext

Goal state after:
ι : 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✝
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 ι
⊢ map (fun x ↦ AddMonoidHom.id (G x)) ⋯ = AddMonoidHom.id (DirectLimit G f)

Tactic:
ext

Goal state after:
ι : 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✝
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)
⊢ (map g₂ hg₂).comp (map g₁ hg₁) = map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯

Tactic:
ext

Goal state after:
ι : 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✝
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
⊢ rTensor Q f ∘ₗ ↑(TensorProduct.comm R Q M) = ↑(TensorProduct.comm R Q N) ∘ₗ lTensor Q f

Tactic:
ext

Goal state after:
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✝
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
⊢ rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N) = ↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
⊢ restrictSupport R univ = ⊤

Tactic:
ext

Goal state after:
σ : Type u
R : Type v
inst✝ : CommSemiring R
x✝ : MvPolynomial σ R
⊢ x✝ ∈ restrictSupport R univ ↔ x✝ ∈ ⊤