mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : IsTensorProduct f
f' : M₁ →ₗ[R] M₂ →ₗ[R] M'
x₁ : M₁
x₂ : M₂
⊢ (h.lift f') ((f x₁) x₂) = (f' x₁) x₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ Disjoint (Icc (-↑N) ↑N) {-(↑N + 1), ↑N + 1}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
ih : ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0
⊢ -(↑N + 1) ≠ ↑N + 1

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
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid 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
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
x₁ : M₁
x₂ : M₂
⊢ (hf.map hg i₁ i₂) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ 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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
⊢ j - 1 < k

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
hf : Function.Even f
N : ℕ
⊢ ∏ m ∈ Icc (-↑N) ↑N, f m = (∏ m ∈ range (N + 1), f ↑m) ^ 2 / f 0

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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
⊢ j < k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (range (b - a - 1).toNat) ↔ a < x ∧ x < b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : ℤ → α
l u : ℤ
h : l ≤ u
⊢ ∏ m ∈ Icc l u, f m = (∏ m ∈ Ico l u, f m) * f u

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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
⊢ ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
⊢ ↑(#(range (max a b + 1 - min a b).toNat)) = ↑((b - a).natAbs + 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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
⊢ G ⟨j - 1, ⋯⟩ ∈ ↑F

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b + 1
⊢ ↑(#(Icc a b)) = b + 1 - a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ ↑(#(Ico a b)) = b - a

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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
⊢ G ⟨j, ⋯⟩ ∈ ↑F

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ ↑(#(Ioc a b)) = b - a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a < b
⊢ ↑(#(Ioo a b)) = b - a - 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
n✝ : ℕ
a✝ : ∏ m ∈ Icc (-(↑n✝ + 1)) (↑n✝ + 1), f m = f (↑n✝ + 1) * f (-(↑n✝ + 1)) * ∏ m ∈ Icc (-↑n✝) ↑n✝, f m
⊢ Disjoint (Icc (-↑(n✝ + 1)) ↑(n✝ + 1)) {-(↑(n✝ + 1) + 1), ↑(n✝ + 1) + 1}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a : ℤ
⊢ Icc a (a + 1) = {a, a + 1}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b + 1
⊢ ↑(Fintype.card ↑(Set.Icc a b)) = b + 1 - a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ico a b)) = b - a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ ↑(Fintype.card ↑(Set.Ioc a b)) = b - a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a < b
⊢ ↑(Fintype.card ↑(Set.Ioo a b)) = b - a - 1

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
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive m

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
N : ℕ
⊢ ∏ m ∈ Icc (-(↑N + 1)) (↑N + 1), f m = f (↑N + 1) * f (-(↑N + 1)) * ∏ m ∈ Icc (-↑N) ↑N, f m

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ Disjoint (Ico (-↑b) ↑b) {-(↑b + 1), ↑b}

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
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
⊢ TensorProduct.lift f = ↑e

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ -(↑b + 1) ∉ {↑b}

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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : (G ⟨j, ⋯⟩).1 < (G ⟨j - 1, ⋯⟩).2
⊢ j < k

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
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
⊢ IsTensorProduct f

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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : (G ⟨j, ⋯⟩).1 < (G ⟨j - 1, ⋯⟩).2
⊢ j - 1 < k

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
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid 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
P₁ : Type u_9
P₂ : Type u_10
P : Type u_11
inst✝⁵ : AddCommMonoid P₁
inst✝⁴ : AddCommMonoid P₂
inst✝³ : AddCommMonoid P
inst✝² : Module R P₁
inst✝¹ : Module R P₂
inst✝ : Module R P
p : P₁ →ₗ[R] P₂ →ₗ[R] P
hf : IsTensorProduct f
hg : IsTensorProduct g
hp : IsTensorProduct p
i₁ : N₁ →ₗ[R] P₁
j₁ : M₁ →ₗ[R] N₁
i₂ : N₂ →ₗ[R] P₂
j₂ : M₂ →ₗ[R] N₂
x : M
⊢ (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) 0 = (hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂) 0

Tactic:
by

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

Goal state before:
pp: b : ℕ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
⊢ ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b

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
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid 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
P₁ : Type u_9
P₂ : Type u_10
P : Type u_11
inst✝⁵ : AddCommMonoid P₁
inst✝⁴ : AddCommMonoid P₂
inst✝³ : AddCommMonoid P
inst✝² : Module R P₁
inst✝¹ : Module R P₂
inst✝ : Module R P
p : P₁ →ₗ[R] P₂ →ₗ[R] P
hf : IsTensorProduct f
hg : IsTensorProduct g
hp : IsTensorProduct p
i₁ : N₁ →ₗ[R] P₁
j₁ : M₁ →ₗ[R] N₁
i₂ : N₂ →ₗ[R] P₂
j₂ : M₂ →ₗ[R] N₂
x : M
⊢ ∀ (x : M₁) (y : M₂), (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) ((f x) y) = (hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂) ((f x) y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n = 0 + n % a + a * (n / a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ 0 + n % a + a * (n / a) ≤ i + a + a * (n / a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a + a * (n / a) = i + a * (n / a + 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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : (G ⟨j, ⋯⟩).1 < (G ⟨j - 1, ⋯⟩).2
⊢ ⟨j - 1, ⋯⟩ ≤ ⟨j, ⋯⟩

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
inst✝¹⁷ : AddCommMonoid M₁
inst✝¹⁶ : AddCommMonoid M₂
inst✝¹⁵ : AddCommMonoid 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
P₁ : Type u_9
P₂ : Type u_10
P : Type u_11
inst✝⁵ : AddCommMonoid P₁
inst✝⁴ : AddCommMonoid P₂
inst✝³ : AddCommMonoid P
inst✝² : Module R P₁
inst✝¹ : Module R P₂
inst✝ : Module R P
p : P₁ →ₗ[R] P₂ →ₗ[R] P
hf : IsTensorProduct f
hg : IsTensorProduct g
hp : IsTensorProduct p
i₁ : N₁ →ₗ[R] P₁
j₁ : M₁ →ₗ[R] N₁
i₂ : N₂ →ₗ[R] P₂
j₂ : M₂ →ₗ[R] N₂
x x✝¹ x✝ : M
h₁ : (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) x✝¹ = (hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂) x✝¹
h₂ : (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) x✝ = (hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂) x✝
⊢ (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) (x✝¹ + x✝) = (hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂) (x✝¹ + x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n % a + a * (n / a + 1)

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
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
x : M
⊢ (hf.map hf LinearMap.id LinearMap.id) 0 = LinearMap.id 0

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
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
x : M
⊢ ∀ (x : M₁) (y : M₂), (hf.map hf LinearMap.id LinearMap.id) ((f x) y) = LinearMap.id ((f x) y)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) = n + a

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
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
x x✝¹ x✝ : M
h₁ : (hf.map hf LinearMap.id LinearMap.id) x✝¹ = LinearMap.id x✝¹
h₂ : (hf.map hf LinearMap.id LinearMap.id) x✝ = LinearMap.id x✝
⊢ (hf.map hf LinearMap.id LinearMap.id) (x✝¹ + x✝) = LinearMap.id (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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : (G ⟨j, ⋯⟩).1 < (G ⟨j - 1, ⋯⟩).2
hG : (G ⟨j - 1, ⋯⟩).1 ≤ (G ⟨j, ⋯⟩).1
⊢ j < 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
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
hj₃ : ⟨j - 1, ⋯⟩ ≠ ⟨j, ⋯⟩
G : Fin k ↪o Lex (α × α) := F.orderEmbOfFin h
this : (G ⟨j, ⋯⟩).1 < (G ⟨j - 1, ⋯⟩).2
hG : (G ⟨j - 1, ⋯⟩).1 ≤ (G ⟨j, ⋯⟩).1
⊢ G ⟨j, ⋯⟩ ∈ F

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
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
i : M₁ →ₗ[R] M₁
j : M₂ →ₗ[R] M₂
n : ℕ
⊢ hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)

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
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

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'
this :
  ∀ ⦃j : ℕ⦄,
    j < k + 1 →
      ∀ ⦃j' : ℕ⦄,
        j' < k + 1 →
          j ≠ j' →
            j < j' →
              Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2)
                j j'
hij' : ¬j < j'
⊢ j' < j

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
this : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
s : S
y : M₁
x : M₂
⊢ s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Icc (-(↑m + 1)) (↑n + 1) = Icc (-↑m) ↑n ∪ {-(↑m + 1), ↑n + 1}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ico (-(↑m + 1)) (↑n + 1) = Ico (-↑m) ↑n ∪ {-(↑m + 1), ↑n}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ioc (-(↑m + 1)) (↑n + 1) = Ioc (-↑m) ↑n ∪ {-↑m, ↑n + 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
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
this : (F.intervalGapsWithin h a b ↑j).2 ≤ (F.intervalGapsWithin h a b ↑j').1
⊢ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2 ∩
      Ioc (F.intervalGapsWithin h a b ↑j').1 (F.intervalGapsWithin h a b ↑j').2 =
    ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ioo (-(↑m + 1)) (↑n + 1) = Ioo (-↑m) ↑n ∪ {-↑m, ↑n}

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'
⊢ j' - 1 + 1 = j'

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
this✝ : Module S (M₁ ⊗[R] M₂) := AddEquiv.module S hf.equiv.toAddEquiv
heq : ∀ (s : S) (y : M₁) (x : M₂), s • y ⊗ₜ[R] x = y ⊗ₜ[R] (s • x)
this : IsScalarTower R S (M₁ ⊗[R] M₂)
s : S
x : M₂ ⊗[R] M₁
⊢ (↑(TensorProduct.comm R M₂ M₁)).toFun (s • x) = (RingHom.id S) s • (↑(TensorProduct.comm R M₂ M₁)).toFun 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'
⊢ j' - 1 ∈ Iio k

Tactic:
by

Goal state after: