mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
⊢ (∃ x, ¬((MulAction.toPermHom G ↑(f.rootSet S)) g) x = 1 x) → ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap

Tactic:
]

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
⊢ (∃ x, ¬((MulAction.toPermHom G ↑(f.rootSet S)) g) x = 1 x) → ((MulAction.toPermHom G ↑(f.rootSet S)) g).IsSwap
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, (coeff i) f ∈ I
hg : ∀ i ≤ n, (coeff i) g ∈ J
i : ℕ
hi : i ≤ n
⊢ ∑ p ∈ Finset.antidiagonal i, (coeff p.1) f * (coeff p.2) g ∈ I * J

Tactic:
]

Goal state after:
A : Type u_1
inst✝ : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, (coeff i) f ∈ I
hg : ∀ i ≤ n, (coeff i) g ∈ J
i : ℕ
hi : i ≤ n
⊢ ∑ p ∈ Finset.antidiagonal i, (coeff p.1) f * (coeff p.2) g ∈ I * J
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
⊢ g • g • ↑x ≠ g • ↑x

Tactic:
by simpa [← rootSet.coe_smul]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Morse

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
⊢ g • ↑x ≠ ↑x

Tactic:
by simpa [← rootSet.coe_smul]

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

Goal state before:
pp: R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i : ι
t : F i ⊗[R] N
⊢ (LinearMap.rTensor N (f ⋯)) (LinearMap.id t) = LinearMap.id t

Tactic:
]

Goal state after:
R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i : ι
t : F i ⊗[R] N
⊢ (LinearMap.rTensor N (f ⋯)) (LinearMap.id t) = LinearMap.id t
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : F k ⊗[R] N
⊢ (LinearMap.rTensor N (f h' ∘ₗ f h)) t = (LinearMap.rTensor N (f ⋯)) t

Tactic:
]

Goal state after:
R : Type u
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : F k ⊗[R] N
⊢ (LinearMap.rTensor N (f h' ∘ₗ f h)) t = (LinearMap.rTensor N (f ⋯)) t
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: τ : Type u_1
S : Type u_3
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : MvPowerSeries τ S
hf : HasSubst f
φ : S⟦X⟧
⊢ MvPowerSeries.subst (fun i ↦ (MvPowerSeries.expand p hp) f) φ =
    MvPowerSeries.subst (fun x ↦ (MvPowerSeries.expand p hp) f) φ

Tactic:
]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
⊢ (MvPowerSeries.coeff (Finsupp.single () m)) φ = (MvPowerSeries.coeff (Finsupp.single () m)) φ

Tactic:
]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
| (coeff 0) ((expand p hp) φ)

Tactic:
← mul_zero p,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
| (coeff (p * 0)) ((expand p hp) φ)
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
⊢ 0 = 0

pp: case h
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
⊢ ¬p ∣ (Finsupp.single () m) ()

Tactic:
]

Goal state after:
case h
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
⊢ ¬p ∣ (Finsupp.single () m) ()
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ (fun x ↦ p • x) '' Function.support φ ⊆ (fun x ↦ p • x) '' Function.support φ

Tactic:
]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ (fun x ↦ p • x) '' Function.support φ = (fun x ↦ p • x) '' Function.support φ

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
n q : ℕ
hq : n = p * q
⊢ (coeff q) φ = (coeff q) φ

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ Tendsto ((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) cofinite (𝓝 0) ↔
    Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : NormedRing R
c : ℝ
f : R⟦X⟧
⊢ Tendsto ((fun n ↦ ‖(coeff n) f‖ * c ^ n) ∘ ⇑(Finsupp.uniqueEquiv ())) cofinite (𝓝 0) ↔
    Tendsto (fun t ↦ ‖(coeff t) f‖ * c ^ t) cofinite (𝓝 0)
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i : ι
t : M ⊗[R] F i
⊢ (LinearMap.lTensor M (f ⋯)) (LinearMap.id t) = LinearMap.id t

Tactic:
]

Goal state after:
R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i : ι
t : M ⊗[R] F i
⊢ (LinearMap.lTensor M (f ⋯)) (LinearMap.id t) = LinearMap.id t
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : M ⊗[R] F k
⊢ (LinearMap.lTensor M (f h' ∘ₗ f h)) t = (LinearMap.lTensor M (f ⋯)) t

Tactic:
]

Goal state after:
R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i j k : ι
h : k ≤ j
h' : j ≤ i
t : M ⊗[R] F k
⊢ (LinearMap.lTensor M (f h' ∘ₗ f h)) t = (LinearMap.lTensor M (f ⋯)) t
Module: Mathlib.RingTheory.PowerSeries.Schroder

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

Tactic:
]

Goal state after:
n : ℕ
hn : 0 < n
⊢ ∑ p ∈ antidiagonal n, (coeff p.1) (X * largeSchroderSeries) * (coeff p.2) largeSchroderSeries =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.PowerSeries.Schroder

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

Tactic:
]

Goal state after:
n : ℕ
hn : 0 < n
⊢ ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (coeff (n - x)) largeSchroderSeries +
      (coeff n) (X * largeSchroderSeries) * (coeff (n - n)) largeSchroderSeries =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
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
⊢ ((if 0 < 0 then (0 - 1).largeSchroder * (n - 0).largeSchroder else 0) +
        ∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
]

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
⊢ ((if 0 < 0 then (0 - 1).largeSchroder * (n - 0).largeSchroder else 0) +
        ∑ x ∈ Ico 1 n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) +
      (n - 1).largeSchroder =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case h
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 // P.FG }
t : ↥↑P ⊗[R] N
ht :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃P Q⦄ h ↦ rTensor N (inclusion h)) P) t =
    (FG.rTensor.directLimit R M N).symm u
⊢ u = u

Tactic:
]

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
hx' : 0 < x
⊢ (x - 1).largeSchroder * (n - x).largeSchroder = (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
]

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
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (↑(Int.negSucc n) • f).toFun' S m = (-1 • (↑↑n.succ • f).toFun' S) m

Tactic:
]

Goal state after:
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
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (↑(Int.negSucc n) • f).toFun' S m = (-1 • (↑↑n.succ • f).toFun' S) m
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 = (rTensor N P.subtype) 0
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = 0

Tactic:
]

Goal state after:
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 = (rTensor N P.subtype) 0
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = 0
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
⊢ ∑ k ∈ range (n - 1 + 1 - 1), (1 + k - 1).largeSchroder * (n - 1 + 1 - (1 + k)).largeSchroder +
      (n - 1 + 1 - 1).largeSchroder =
    ∑ x ∈ range (n - 1), x.largeSchroder * (n - 1 + 1 - 1 - x).largeSchroder +
      (n - 1).largeSchroder * (n - 1 + 1 - 1 - (n - 1)).largeSchroder

Tactic:
]

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 - 1), (1 + k - 1).largeSchroder * (n - 1 + 1 - (1 + k)).largeSchroder +
      (n - 1 + 1 - 1).largeSchroder =
    ∑ x ∈ range (n - 1), x.largeSchroder * (n - 1 + 1 - 1 - x).largeSchroder +
      (n - 1).largeSchroder * (n - 1 + 1 - 1 - (n - 1)).largeSchroder
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
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ -↑n • f.toFun' S m + -1 • f.toFun' S m = -↑n • f.toFun' S m + -1 • f.toFun' S m

Tactic:
]

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
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (-f + f).toFun' S m = toFun' 0 S m

Tactic:
simp only [add_def_apply, neg_def, Pi.smul_apply, zero_def, Pi.zero_apply]

Goal state after:
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
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ -1 • f.toFun' S m + f.toFun' S m = 0
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ (n - 1).largeSchroder + ∑ i ≤ n - 1, i.largeSchroder * (n - 1 - i).largeSchroder =
    (n - 1 + 1 - 1).largeSchroder + ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 + 1 - 1 - i).largeSchroder

Tactic:
]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ (n - 1).largeSchroder + ∑ i ≤ n - 1, i.largeSchroder * (n - 1 - i).largeSchroder =
    (n - 1 + 1 - 1).largeSchroder + ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 + 1 - 1 - i).largeSchroder
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder =
    ∑ i ∈ range (n - 1 + 1), i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
]

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
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (-1 + 1) • f.toFun' S m = 0

Tactic:
]

Goal state after:
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
S : Type u
x✝¹ : CommSemiring S
x✝ : Algebra R S
m : S ⊗[R] M
⊢ (-1 + 1) • f.toFun' S m = 0
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (if n + 1 = 0 then 0 else (algebraMap ℚ A) ((-1) ^ (n + 1 + 1) / ↑(n + 1))) * (↑n + 1) = (algebraMap ℚ A) ((-1) ^ n)

Tactic:
]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (if n + 1 = 0 then 0 else (algebraMap ℚ A) ((-1) ^ (n + 1 + 1) / ↑(n + 1))) * (↑n + 1) = (algebraMap ℚ A) ((-1) ^ n)
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 (subst (f - 1) (log A)) = 0

Tactic:
]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
⊢ constantCoeff (subst (f - 1) (log A)) = 0
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
⊢ 0 = 0

Tactic:
]

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] (TensorProduct.lid R N) (f.toFun' R (1 ⊗ₜ[R] x)) = f.toFun' S (1 ⊗ₜ[R] x)

Tactic:
]

Goal state after:
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] (TensorProduct.lid R N) (f.toFun' R (1 ⊗ₜ[R] x)) = f.toFun' S (1 ⊗ₜ[R] x)
Module: Mathlib.RingTheory.PowerSeries.Log

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

Tactic:
]

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

Goal state before:
pp: case e'_3
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] x = 1 ⊗ₜ[R] x

Tactic:
]

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

Goal state before:
pp: case right
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
s : Finset S
hs : span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
hu : u ∈ (rTensor N (Subalgebra.toSubmodule (Algebra.adjoin R ↑s)).subtype ∘ₗ rTensor N (inclusion this)).range
⊢ u ∈ (rTensor N (Algebra.adjoin R ↑s).val.toLinearMap).range

Tactic:
]

Goal state after:
case right
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
s : Finset S
hs : span R ↑s = P
this : P ≤ Subalgebra.toSubmodule (Algebra.adjoin R ↑s)
hu : u ∈ (rTensor N (Subalgebra.toSubmodule (Algebra.adjoin R ↑s)).subtype ∘ₗ rTensor N (inclusion this)).range
⊢ u ∈ (rTensor N (Algebra.adjoin R ↑s).val.toLinearMap).range
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
⊢ m = m

Tactic:
]

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
⊢ Algebra.adjoin R (Set.range fun n ↦ ↑(s.equivFin.symm n)) = Algebra.adjoin R ↑s

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ Algebra.adjoin R (Set.range fun n ↦ ↑(s.equivFin.symm n)) = Algebra.adjoin R ↑s
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
⊢ Subtype.val '' Set.range ⇑s.equivFin.symm = ↑s

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ Subtype.val '' Set.range ⇑s.equivFin.symm = ↑s
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) ((rTensor N j) u) = (rTensor N P₁.subtype) ((rTensor N j') u')

Tactic:
]

Goal state after:
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) ((rTensor N j) u) = (rTensor N P₁.subtype) ((rTensor N j') u')