mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
Q : { Q // Q.FG }
u : M ⊗[R] ↥↑Q
this :
  ↑(directLimit R M N) ∘ₗ
      Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q =
    lTensor M (↑Q).subtype
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q) u) =
    (lTensor M (↑Q).subtype) u

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a✝ b✝ : R
f✝ g : M →ₚₗ[R] N
a b : R
f : M →ₚₗ[R] N
⊢ (a * b) • f = a • b • f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g✝ f g h : M →ₚₗ[R] N
⊢ f + g + h = f + (g + h)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ 0 + f = f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ f + 0 = f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
Q : { Q // Q.FG }
u : M ⊗[R] ↥↑Q
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q) u) =
    (lTensor M (↑Q).subtype) u

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g f : M →ₚₗ[R] N
⊢ 0 • f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
⊢ 0 < n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ (n + 1) • f = n • f + f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a b : R
f✝ g✝ f g : M →ₚₗ[R] N
⊢ f + g = g + f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
r a✝ b : R
f✝ g✝ : M →ₚₗ[R] N
a : R
f g : M →ₚₗ[R] N
⊢ a • (f + g) = a • f + a • g

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
⊢ 0 • f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : M ⊗[R] N
⊢ ∃ P, P.FG ∧ u ∈ (rTensor N P.subtype).range

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ ↑n.succ • f = ↑n • f + f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
x : ℕ
hx : x ∈ Ico 1 n
⊢ 0 < x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
⊢ (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) =
    ∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h : (rTensor N P.subtype) t = (rTensor N P.subtype) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this✝ :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
this :
  (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) =
    ∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder
⊢ ∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
sum_Ico_eq_sum_range,

Goal state after:
n : ℕ
hn : 0 < n
this✝ :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
this :
  (∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) =
    ∑ x ∈ Ico 1 n, (x - 1).largeSchroder * (n - x).largeSchroder
⊢ ∑ k ∈ range (n - 1), (1 + k - 1).largeSchroder * (n - (1 + k)).largeSchroder + (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ constantCoeff (log A) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
h : (rTensor N P.subtype) t = 0
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ (coeff n) (X * largeSchroderSeries ^ 2) = ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra ℚ A
A' : Type u_2
inst✝¹ : CommRing A'
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (log A) = log A'

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ Int.negSucc n • f = -(↑n.succ • f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff 1) (log A) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : ¬n = 0
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : Nontrivial A
⊢ (coeff 1) (log A) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : Nontrivial A
i : ℕ
hi : i < 1
⊢ (coeff i) (log A) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ↑n + 1 = (algebraMap ℚ A) (↑n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: ⊢ largeSchroderSeries = 1 + X * largeSchroderSeries + X * largeSchroderSeries ^ 2

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f : M →ₚₗ[R] N
⊢ -f + f = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (d⁄dX A) (log A) = mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ constantCoeff (exp A - 1) = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f✝ f g : M →ₚₗ[R] N
⊢ f + g = g + f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
⊢ MvPowerSeries.constantCoeff (f - 1) = 0

Tactic:
rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
⊢ MvPowerSeries.constantCoeff (f - 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t : ↥P ⊗[R] N
P' : Submodule R M
hP' : P'.FG
t' : ↥P' ⊗[R] N
h : (rTensor N P.subtype) t = (rTensor N P'.subtype) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q) (hP'Q : P' ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hP'Q)) t'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
⊢ constantCoeff f.logOf = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (1 + X).logOf = log A

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : S ⊗[R] N
P : Submodule R S
hu : u ∈ (rTensor N P.subtype).range
s : Finset S
hs : span R ↑s = P
⊢ P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] f.ground x = f.toFun' S (1 ⊗ₜ[R] x)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f x y : M →ₚₗ[R] N
⊢ (x + y).ground = x.ground + y.ground

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₚₗ[R] N
r : R
x : M →ₚₗ[R] N
⊢ (r • x).ground = (RingHom.id R) r • x.ground

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
u : S ⊗[R] N
⊢ ∃ A, A.FG ∧ u ∈ (rTensor N A.val.toLinearMap).range

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ id.ground = _root_.id

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ id.ground m = m

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type u_3
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
Q : Type u_4
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
f✝ : M →ₚₗ[R] N
g✝ : N →ₚₗ[R] P
h : P →ₚₗ[R] Q
g : N →ₚₗ[R] P
f : M →ₚₗ[R] N
S✝ : Type u
inst✝³ : CommSemiring S✝
inst✝² : Algebra R S✝
S'✝ : Type u
inst✝¹ : CommSemiring S'✝
inst✝ : Algebra R S'✝
φ : S✝ →ₐ[R] S'✝
⊢ ⇑(rTensor P φ.toLinearMap) ∘ g.toFun' S✝ ∘ f.toFun' S✝ = (g.toFun' S'✝ ∘ f.toFun' S'✝) ∘ ⇑(rTensor M φ.toLinearMap)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g : N →ₚₗ[R] P
⊢ g.comp id = g

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₚₗ[R] N
⊢ id.comp f = f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ (φ R s).range = Algebra.adjoin R ↑s

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
B : Subalgebra R S
hB : B.FG
⊢ (φ R (Exists.choose hB)).range = B

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P
⊢ (Subalgebra.toSubmodule A).subtype p ∈ P₁

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹² : CommSemiring R
M : Type u_1
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
S : Type v
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
f : M →ₚₗ[R] N
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
⊢ (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
p : ↥(Subalgebra.toSubmodule A)
hp : p ∈ P'
⊢ (Subalgebra.toSubmodule A).subtype p ∈ P₁

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: ⊢ primeFactors = Nat.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ radical n = ∏ p ∈ n.primeFactors, p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ 1 < radical n ↔ 1 < n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ radical n ≤ 1 ↔ n ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ radical n = 1 ↔ n ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ radical n ≤ n → n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
h : n ≠ 0
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ n < radical n ↔ n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ (radical n).primeFactors = n.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ radical n ∣ k ↔ n.primeFactors ⊆ k.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n ∣ radical n ^ n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ 0 < radical 100

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
hz : z ≠ 0
p : ℕ
x✝ : Prime ↑p ∧ 0 ≤ ↑p ∧ ↑p ∣ z
pp : Nat.Prime p
dp : p ∣ z.natAbs
⊢ p ∈ z.natAbs.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
hz : z ≠ 0
n : ℕ
pn : Nat.Prime n
dn : n ∣ z.natAbs
⊢ 0 ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ ↑(radical z.natAbs) = radical z

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
⊢ (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ radical z = ↑(∏ p ∈ z.natAbs.primeFactors, p)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ 0 < radical z

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ 1 < radical z ↔ 1 < z.natAbs

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ radical z ≤ 1 ↔ z.natAbs ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ radical z = 1 ↔ z.natAbs ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
⊢ radical ↑n = ↑(radical n)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h✝ : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
this : (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁
P'₁ : Submodule R S
hP₁_le : P₁ ≤ P'₁
hP'₁ : P'₁.FG
h : (rTensor N (inclusion hP₁_le)) u₁ = (rTensor N (inclusion hP₁_le)) u'₁
s : Finset S
hs : span R ↑s = P'₁
w : Finset S
hw : Algebra.adjoin R ↑w = A
B : Subalgebra R S := Algebra.adjoin R ↑(s ∪ w)
⊢ A ≤ B

Tactic:
by

Goal state after: