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

Goal state before:
pp: R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ (assocAux f hf g hg).symm (x₁ ⊗ₜ[R] (g x₂) x₃) = (f x₁) x₂ ⊗ₜ[S] x₃

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ (F.intervalGapsWithin h a b ↑j').1

Tactic:
grw [← this]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ (F.intervalGapsWithin h a b ↑(j' - 1)).2
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ j < k

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_9
S : Type u_10
inst✝²⁰ : CommSemiring R
inst✝¹⁹ : CommSemiring S
inst✝¹⁸ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid M₃
inst✝¹⁴ : AddCommMonoid M₁₂
inst✝¹³ : AddCommMonoid M₂₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module S M₂
inst✝⁹ : IsScalarTower R S M₂
inst✝⁸ : Module R M₃
inst✝⁷ : Module S M₃
inst✝⁶ : IsScalarTower R S M₃
inst✝⁵ : Module R M₁₂
inst✝⁴ : Module S M₁₂
inst✝³ : IsScalarTower R S M₁₂
inst✝² : Module R M₂₃
inst✝¹ : Module S M₂₃
inst✝ : IsScalarTower R S M₂₃
f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
x₁ : M₁
x₂ : M₂
x₃ : M₃
⊢ (assocAux f hf g hg) ((f x₁) x₂ ⊗ₜ[S] x₃) = x₁ ⊗ₜ[R] (g x₂) x₃

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ j' - 1 < k

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
⊢ ⟨j, ⋯⟩ ≤ ⟨j' - 1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ (Iio (k + 1)).PairwiseDisjoint fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝⁴² : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁴¹ : AddCommMonoid M₁✝
inst✝⁴⁰ : AddCommMonoid M₂✝
inst✝³⁹ : AddCommMonoid M
inst✝³⁸ : AddCommMonoid M'
inst✝³⁷ : Module R✝ M₁✝
inst✝³⁶ : Module R✝ M₂✝
inst✝³⁵ : Module R✝ M
inst✝³⁴ : Module R✝ M'
f✝¹ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝³³ : AddCommMonoid N₁
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid N
inst✝³⁰ : Module R✝ N₁
inst✝²⁹ : Module R✝ N₂
inst✝²⁸ : Module R✝ N
g✝¹ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝²⁴ : AddCommMonoid M₁
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid M₁₂
inst✝²⁰ : AddCommMonoid M₂₃
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module S M₂
inst✝¹⁶ : IsScalarTower R S M₂
inst✝¹⁵ : Module R M₃
inst✝¹⁴ : Module S M₃
inst✝¹³ : IsScalarTower R S M₃
inst✝¹² : Module R M₁₂
inst✝¹¹ : Module S M₁₂
inst✝¹⁰ : IsScalarTower R S M₁₂
inst✝⁹ : Module R M₂₃
inst✝⁸ : Module S M₂₃
inst✝⁷ : IsScalarTower R S M₂₃
f✝ : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y : M₃
x : M₁
z : M₂
⊢ t • (f x) z = (f (t • x)) z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ t ∈ (cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a ↑t ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
s : Finset α
f : Finset α → β
⊢ ∏ t ∈ s.powerset, f t = ∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
f : α → ℕ
h : ∀ x ∈ l, f x ≡ 1 [MOD n]
⊢ (List.map (fun x ↦ 1) l).prod ≡ 1 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
s : Finset α
f : ℕ → β
⊢ ∏ t ∈ powersetCard n s, f #t = f n ^ (#s).choose n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℕ
l : List ℕ
h : ∀ x ∈ l, x ≡ 1 [MOD n]
⊢ l.prod ≡ 1 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
f : α → ℕ
h : ∀ x ∈ l, f x ≡ 0 [MOD n]
⊢ (List.map f l).sum ≡ 0 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℕ
l : List ℕ
h : ∀ x ∈ l, x ≡ 0 [MOD n]
⊢ l.sum ≡ 0 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ (Multiset.map f s).prod ≡ (Multiset.map g s).prod [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [MOD n]
⊢ (Multiset.map f s).prod ≡ 1 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 1 [MOD n]
⊢ s.prod ≡ 1 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [MOD n]
⊢ (Multiset.map f s).sum ≡ 0 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 0 [MOD n]
⊢ s.sum ≡ 0 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ 0 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 1 [MOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ f a [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [MOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ f a [MOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
l : List α
f : α → ℤ
h : ∀ x ∈ l, f x ≡ 1 [ZMOD n]
⊢ (List.map (fun x ↦ 1) l).prod ≡ 1 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℤ
l : List ℤ
h : ∀ x ∈ l, x ≡ 1 [ZMOD n]
⊢ l.prod ≡ 1 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
l : List α
f : α → ℤ
h : ∀ x ∈ l, f x ≡ 0 [ZMOD n]
⊢ (List.map f l).sum ≡ 0 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℤ
l : List ℤ
h : ∀ x ∈ l, x ≡ 0 [ZMOD n]
⊢ l.sum ≡ 0 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f s).prod ≡ (Multiset.map g s).prod [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ (Multiset.map f s).prod ≡ 1 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 1 [ZMOD n]
⊢ s.prod ≡ 1 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝⁴² : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁴¹ : AddCommMonoid M₁✝
inst✝⁴⁰ : AddCommMonoid M₂✝
inst✝³⁹ : AddCommMonoid M
inst✝³⁸ : AddCommMonoid M'
inst✝³⁷ : Module R✝ M₁✝
inst✝³⁶ : Module R✝ M₂✝
inst✝³⁵ : Module R✝ M
inst✝³⁴ : Module R✝ M'
f✝¹ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝³³ : AddCommMonoid N₁
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid N
inst✝³⁰ : Module R✝ N₁
inst✝²⁹ : Module R✝ N₂
inst✝²⁸ : Module R✝ N
g✝¹ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝²⁴ : AddCommMonoid M₁
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid M₁₂
inst✝²⁰ : AddCommMonoid M₂₃
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module S M₂
inst✝¹⁶ : IsScalarTower R S M₂
inst✝¹⁵ : Module R M₃
inst✝¹⁴ : Module S M₃
inst✝¹³ : IsScalarTower R S M₃
inst✝¹² : Module R M₁₂
inst✝¹¹ : Module S M₁₂
inst✝¹⁰ : IsScalarTower R S M₁₂
inst✝⁹ : Module R M₂₃
inst✝⁸ : Module S M₂₃
inst✝⁷ : IsScalarTower R S M₂₃
f✝ : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
x : M₁₂ ⊗[S] M₃
⊢ (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun (t • x) =
    (RingHom.id T) t • (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [ZMOD n]
⊢ (Multiset.map f s).sum ≡ 0 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: n : ℤ
s : Multiset ℤ
h : ∀ x ∈ s, x ≡ 0 [ZMOD n]
⊢ s.sum ≡ 0 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 1 [ZMOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ f a [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
⊢ ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ if a ∈ s then f a else 0 [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
a : α
ha : a ∉ s → f a ≡ 0 [ZMOD n]
hf : ∀ x ∈ s, x ≠ a → f x ≡ 0 [ZMOD n]
⊢ ∑ x ∈ s, f x ≡ f a [ZMOD n]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝⁴² : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁴¹ : AddCommMonoid M₁✝
inst✝⁴⁰ : AddCommMonoid M₂✝
inst✝³⁹ : AddCommMonoid M
inst✝³⁸ : AddCommMonoid M'
inst✝³⁷ : Module R✝ M₁✝
inst✝³⁶ : Module R✝ M₂✝
inst✝³⁵ : Module R✝ M
inst✝³⁴ : Module R✝ M'
f✝² : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝³³ : AddCommMonoid N₁
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid N
inst✝³⁰ : Module R✝ N₁
inst✝²⁹ : Module R✝ N₂
inst✝²⁸ : Module R✝ N
g✝² : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝²⁴ : AddCommMonoid M₁
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid M₁₂
inst✝²⁰ : AddCommMonoid M₂₃
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module S M₂
inst✝¹⁶ : IsScalarTower R S M₂
inst✝¹⁵ : Module R M₃
inst✝¹⁴ : Module S M₃
inst✝¹³ : IsScalarTower R S M₃
inst✝¹² : Module R M₁₂
inst✝¹¹ : Module S M₁₂
inst✝¹⁰ : IsScalarTower R S M₁₂
inst✝⁹ : Module R M₂₃
inst✝⁸ : Module S M₂₃
inst✝⁷ : IsScalarTower R S M₂₃
f✝¹ : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf✝¹ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝¹)
g✝¹ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝¹ : IsTensorProduct g✝¹
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f✝ : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ : ∀ (t : T) (x : M₁) (y : M₂), (f (t • x)) y = t • (f x) y
h₂ : ∀ (s : S) (x : M₁) (y : M₂), (f x) (s • y) = s • (f x) y
⊢ ∀ (m₁ m₂ : M₁) (n : M₂), (f (m₁ + m₂)) n = (f m₁) n + (f m₂) n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝⁴² : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁴¹ : AddCommMonoid M₁✝
inst✝⁴⁰ : AddCommMonoid M₂✝
inst✝³⁹ : AddCommMonoid M
inst✝³⁸ : AddCommMonoid M'
inst✝³⁷ : Module R✝ M₁✝
inst✝³⁶ : Module R✝ M₂✝
inst✝³⁵ : Module R✝ M
inst✝³⁴ : Module R✝ M'
f✝² : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝³³ : AddCommMonoid N₁
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid N
inst✝³⁰ : Module R✝ N₁
inst✝²⁹ : Module R✝ N₂
inst✝²⁸ : Module R✝ N
g✝² : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝²⁴ : AddCommMonoid M₁
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid M₁₂
inst✝²⁰ : AddCommMonoid M₂₃
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module S M₂
inst✝¹⁶ : IsScalarTower R S M₂
inst✝¹⁵ : Module R M₃
inst✝¹⁴ : Module S M₃
inst✝¹³ : IsScalarTower R S M₃
inst✝¹² : Module R M₁₂
inst✝¹¹ : Module S M₁₂
inst✝¹⁰ : IsScalarTower R S M₁₂
inst✝⁹ : Module R M₂₃
inst✝⁸ : Module S M₂₃
inst✝⁷ : IsScalarTower R S M₂₃
f✝¹ : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf✝¹ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝¹)
g✝¹ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝¹ : IsTensorProduct g✝¹
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f✝ : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ : ∀ (t : T) (x : M₁) (y : M₂), (f (t • x)) y = t • (f x) y
h₂ : ∀ (s : S) (x : M₁) (y : M₂), (f x) (s • y) = s • (f x) y
⊢ ∀ (c : T) (m : M₁) (n : M₂), (f (c • m)) n = c • (f m) n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
⊢ ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R✝ : Type u_1
inst✝⁴² : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁴¹ : AddCommMonoid M₁✝
inst✝⁴⁰ : AddCommMonoid M₂✝
inst✝³⁹ : AddCommMonoid M
inst✝³⁸ : AddCommMonoid M'
inst✝³⁷ : Module R✝ M₁✝
inst✝³⁶ : Module R✝ M₂✝
inst✝³⁵ : Module R✝ M
inst✝³⁴ : Module R✝ M'
f✝² : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝³³ : AddCommMonoid N₁
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid N
inst✝³⁰ : Module R✝ N₁
inst✝²⁹ : Module R✝ N₂
inst✝²⁸ : Module R✝ N
g✝² : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝²⁴ : AddCommMonoid M₁
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid M₁₂
inst✝²⁰ : AddCommMonoid M₂₃
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module S M₂
inst✝¹⁶ : IsScalarTower R S M₂
inst✝¹⁵ : Module R M₃
inst✝¹⁴ : Module S M₃
inst✝¹³ : IsScalarTower R S M₃
inst✝¹² : Module R M₁₂
inst✝¹¹ : Module S M₁₂
inst✝¹⁰ : IsScalarTower R S M₁₂
inst✝⁹ : Module R M₂₃
inst✝⁸ : Module S M₂₃
inst✝⁷ : IsScalarTower R S M₂₃
f✝¹ : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf✝¹ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝¹)
g✝¹ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝¹ : IsTensorProduct g✝¹
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f✝ : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂
hf : IsTensorProduct f
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
h₁ : ∀ (t : T) (x : M₁) (y : M₂), (f (t • x)) y = t • (f x) y
h₂ : ∀ (s : S) (x : M₁) (y : M₂), (f x) (s • y) = s • (f x) y
⊢ ∀ (m : M₁) (n₁ n₂ : M₂), (f m) (n₁ + n₂) = (f m) n₁ + (f m) n₂

Tactic:
by

Goal state after: