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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
M₁ : Type u_5
M₂ : Type u_6
N₁ : Type u_7
N₂ : Type u_8
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₁
inst✝² : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
h₁ : Function.Injective ⇑i₁
h₂ : Function.Injective ⇑i₂
inst✝¹ : Module.Flat R M₁
inst✝ : Module.Flat R N₂
x : M
⊢ ∀ (x : M₁) (y : M₂), (hf.map hg i₁ i₂) ((f x) y) = (⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm) ((f x) y)

Tactic:
simp

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

Goal state before:
pp: case empty
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
hs : (↑∅).PairwiseDisjoint t
⊢ (⋃ i ∈ ∅, t i).mulIndicator f = fun a ↦ ∏ i ∈ ∅, (t i).mulIndicator f a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → AddGroupWithOne (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
n : ℕ
⊢ ⟦⟨Classical.arbitrary ι, (fun x ↦ ↑(Int.negSucc n)) (Classical.arbitrary ι)⟩⟧ =
    ⟦⟨⟨Classical.arbitrary ι, (fun x ↦ ↑(n + 1)) (Classical.arbitrary ι)⟩.fst,
        (fun x x_1 ↦ -x_1) ⟨Classical.arbitrary ι, (fun x ↦ ↑(n + 1)) (Classical.arbitrary ι)⟩.fst
          ⟨Classical.arbitrary ι, (fun x ↦ ↑(n + 1)) (Classical.arbitrary ι)⟩.snd⟩⟧

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
f : ι → M
⊢ #∅ • 𝔼 i ∈ ∅, f i = ∑ i ∈ ∅, f i

Tactic:
simp

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 : α
⊢ MapsTo (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (Iio k) ↑F

Tactic:
intro j

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
⊢ j ∈ Iio k → (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j ∈ ↑F
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
⊢ InjOn (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (Iio k)

Tactic:
intro j

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
⊢ j ∈ Iio k →
    ∀ ⦃x₂ : ℕ⦄,
      x₂ ∈ Iio k →
        (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j =
            (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) x₂ →
          j = x₂
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (𝔼 j, if h : i = j then f j h else 0) = (↑(card ι))⁻¹ • f i ⋯

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (𝔼 j, if h : j = i then f j h else 0) = (↑(card ι))⁻¹ • f i ⋯

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j, if i = j then f j else 0) = (↑(card ι))⁻¹ • f i

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j, if j = i then f j else 0) = (↑(card ι))⁻¹ • f i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (of G f j) ((f i j hij) x) = (of G f i) x

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∀ a ∈ range k, f (p ↑a).2 (p ↑a.succ).1 = f ((p ↑a).2, (p ↑a.succ).1).1 ((p ↑a).2, (p ↑a.succ).1).2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ g (F.intervalGapsWithin h a b ↑k).1 / g (F.intervalGapsWithin h a b ↑0).1 *
      (g (F.intervalGapsWithin h a b ↑k).2 / g (F.intervalGapsWithin h a b ↑k).1) =
    g b / g a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ ∀ (x : M) (y : N), (lift (mk R M N)) (x ⊗ₜ[R] y) = LinearMap.id (x ⊗ₜ[R] y)

Tactic:
simp

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
x₁ : M₁
x₂ : M₂
⊢ (f x₁) x₂ = h.equiv (x₁ ⊗ₜ[R] x₂)

Tactic:
simp

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

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

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

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

Tactic:
simp

Goal state after:
a a✝ : ℤ
⊢ a ≤ a✝ ∧ a✝ ≤ a + 1 ↔ a✝ = a ∨ a✝ = a + 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
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
⊢ ∏ m ∈ Icc (-(↑(n✝ + 1) + 1)) (↑(n✝ + 1) + 1), f m =
    f (↑(n✝ + 1) + 1) * f (-(↑(n✝ + 1) + 1)) * ∏ m ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f m

Tactic:
rw [Icc_succ_succ, prod_union (by simp)]

Goal state after:
case succ
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
⊢ (∏ x ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f x) * ∏ x ∈ {-(↑(n✝ + 1) + 1), ↑(n✝ + 1) + 1}, f x =
    f (↑(n✝ + 1) + 1) * f (-(↑(n✝ + 1) + 1)) * ∏ m ∈ Icc (-↑(n✝ + 1)) ↑(n✝ + 1), f m
Module: Mathlib.Data.Int.Interval

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

Tactic:
simp

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

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

Tactic:
simp

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

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

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

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

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

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
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₂
⊢ hf.map hf i j ^ 0 = hf.map hf (i ^ 0) (j ^ 0)

Tactic:
simp

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:
intro j

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 : ℕ
⊢ j ∈ Iio (k + 1) →
    ∀ ⦃y : ℕ⦄,
      y ∈ Iio (k + 1) →
        j ≠ y →
          Function.onFun Disjoint (fun j ↦ Ioc (F.intervalGapsWithin h a b ↑j).1 (F.intervalGapsWithin h a b ↑j).2) j y
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
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
⊢ (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun (t • 0) =
    (RingHom.id T) t • (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case tmul.zero
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₃
⊢ (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun (t • hf.equiv 0 ⊗ₜ[S] y) =
    (RingHom.id T) t • (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun (hf.equiv 0 ⊗ₜ[S] y)

Tactic:
simp

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

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

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

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

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ ((↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] S ⊗[R] M))).flip ((mk R S M) 1))) s) x = ((mk R S M) s) x

Tactic:
change s • (1 : S) ⊗ₜ[R] x = s ⊗ₜ[R] x

Goal state after:
R : Type u_1
M : Type v₁
S : Type v₃
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : Module R M
s : S
x : M
⊢ s • 1 ⊗ₜ[R] x = s ⊗ₜ[R] x