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
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 : S) (m : M₁) (n : M₂), (f m) (c • n) = c • (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
ist : IsTensorProduct f
e : M ≃ₗ[R] M'
⊢ IsTensorProduct (f.compr₂ ↑e)

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
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₁
inst✝ : Module R N₂
ist : IsTensorProduct f
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ IsTensorProduct ((f ∘ₗ ↑e₁).compl₂ ↑e₂)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ i ∈ s, f i) ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Odd (∑ i ∈ s, f i) ↔ Odd #({x ∈ s | Odd (f x)})

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
⊢ t ⊆ s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
⊢ ∀ x ∈ s, x ∉ t → Nat.card { a // f a = x } = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
⊢ ∀ b ∈ ↑t, (f ⁻¹' {b}).Finite

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ m ∈ s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
this : {a | f a = m} ⊆ ↑ht.toFinset
a : ι
⊢ a ∈ {a ∈ ht.toFinset | f a = m} ↔ a ∈ ⋯.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module S N
inst✝⁶ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
x : N
⊢ (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun (r • x) =
    (RingHom.id S) r • (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
⊢ Nat.card ↑(f ⁻¹' ↑s) = ∑ b ∈ s, Nat.card { a // f a = b }

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
⊢ (h.lift g) (f x) = g x

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
h₂ :
  ∑ 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
⊢ ∀ (i : ℕ),
    f i • ∑ i ∈ range (i + 1), g i - f (i + 1) • ∑ i ∈ range (i + 1), g i =
      -((f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
⊢ g₁ = g₂

Tactic:
by

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
⊢ IsBaseChange S ((mk R S M) 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x : S ⊗[R] M
⊢ (↑(IsTensorProduct.equiv h)).toFun (r • x) = (RingHom.id S) r • (↑(IsTensorProduct.equiv h)).toFun x

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 n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
m : M
⊢ h.equiv.symm (f m) = 1 ⊗ₜ[R] m

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 ∈ Ioc m n, f i • g i =
    f n • ∑ i ∈ range (n + 1), g i - f (m + 1) • ∑ i ∈ range (m + 1), g i -
      ∑ i ∈ Ioc m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
e : S ⊗[R] M ≃ₗ[S] N
he : ∀ (x : M), e (1 ⊗ₜ[R] x) = f x
⊢ IsBaseChange S f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ (AlgebraTensorModule.rid R S S) (1 ⊗ₜ[R] x) = (Algebra.linearMap R S) x

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
n : ℕ
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ ↑x✝¹.sym2 = ↑x✝.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m : Multiset α
xs : List α
⊢ Multiset.sym2 ⟦xs⟧ = 0 ↔ ⟦xs⟧ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
m : Multiset α
xs : List α
⊢ (map f ⟦xs⟧).sym2 = map (Sym2.map f) (Multiset.sym2 ⟦xs⟧)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m : Multiset α
a b : α
xs : List α
⊢ s(a, b) ∈ Multiset.sym2 ⟦xs⟧ ↔ a ∈ ⟦xs⟧ ∧ b ∈ ⟦xs⟧

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m : Multiset α
z : Sym2 α
xs : List α
⊢ z ∈ Multiset.sym2 ⟦xs⟧ ↔ ∀ y ∈ z, y ∈ ⟦xs⟧

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m : Multiset α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ {z | z ∈ m.sym2} ↔ s(a, b) ∈ {x | x ∈ m}.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m m' : Multiset α
h : m ≤ m'
⊢ m.sym2 ≤ m'.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m : Multiset α
⊢ m.sym2.card = (m.card + 1).choose 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
xs : List α
⊢ (Multiset.sym2 ⟦xs⟧).dedup = (dedup ⟦xs⟧).sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
xs : List α
⊢ (map f xs).sym2 = map (Sym2.map f) xs.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
z : Sym2 α
⊢ z ∈ (x :: xs).sym2 ↔ z = s(x, x) ∨ (∃ y ∈ xs, z = s(x, y)) ∨ z ∈ xs.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
⊢ xs.sym2 = [] ↔ xs = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ a ∈ xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
ha : a ∈ xs
hb : b ∈ xs
⊢ s(a, b) ∈ xs.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a b : α
⊢ s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ a ∈ xs ∧ b ∈ xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
m : Sym2 α
⊢ m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
z : Sym2 α
⊢ z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
m : Finset α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ ↑m.sym2 ↔ s(a, b) ∈ (↑m).sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b a : α
s : Finset α
ha : a ∉ s
⊢ Disjoint (map (Sym2.mkEmbedding a) (cons a s ha)) s.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ {z | z ∈ xs.sym2} ↔ s(a, b) ∈ {x | x ∈ xs}.sym2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module S N
inst✝⁶ : IsScalarTower R S N
f : M →ₗ[R] N
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
f' : P →ₗ[R] Q
eM : M ≃ₗ[R] P
eN : N ≃ₗ[S] Q
comm : f' ∘ₗ ↑eM = ↑(LinearEquiv.restrictScalars R eN) ∘ₗ f
⊢ IsBaseChange S f ↔ IsBaseChange S f'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).sym2 = image (fun b ↦ s(a, b)) (insert a s) ∪ s.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2 = image (Sym2.map f) s.sym2

Tactic:
apply val_injective

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2.val = (image (Sym2.map f) s.sym2).val
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
e : M ≃ₗ[R] P
f : P →ₗ[R] N
isb : IsBaseChange S f
y : M
⊢ (f ∘ₗ ↑e) y = (↑(LinearEquiv.restrictScalars R (LinearEquiv.refl S N)) ∘ₗ f ∘ₗ ↑e) y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).sym2 = image (Sym2.map f) s.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ univ.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
inst : Fintype (Sym2 α)
⊢ univ.sym2 = univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s t : Finset α
h : s ⊆ t
⊢ s.sym2 ⊆ t.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
⊢ Function.Injective Finset.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ m.toFinset.sym2 = m.sym2.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
h : xs.Nodup
⊢ xs.sym2.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2.Nonempty ↔ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s.sym2 = (#s + 1).choose 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.sym2 = image (Function.uncurry Sym2.mk) (s ×ˢ s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
h : x ∈ xs
⊢ map (fun y ↦ s(x, y)) xs <+ xs.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a b : α
h : (a, b) ∈ s.diag
⊢ s(a, b).IsDiag

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
h : x ∉ xs
⊢ (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a b : α
h : (a, b) ∈ s.offDiag
⊢ ¬s(a, b).IsDiag

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ (∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
⊢ Sym2.diag a ∈ s.sym2 ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ image (Function.uncurry Sym2.mk) s.diag ∪ image (Function.uncurry Sym2.mk) s.offDiag = s.sym2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
P : Type u_2
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
A : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra S A
inst✝⁵ : IsScalarTower R S A
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module A N
inst✝¹ : IsScalarTower S A N
inst✝ : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
⊢ IsBaseChange A (AlgebraTensorModule.map f LinearMap.id)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
m : Sym α n
⊢ m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ xs.sym2.dedup = xs.dedup.sym2

Tactic:
induction xs with
  | nil => simp only [List.sym2, dedup_nil]
  | cons x xs ih =>
    simp only [List.sym2, map_cons, cons_append]
    obtain hm | hm := Decidable.em (x ∈ xs)
    · rw [dedup_cons_of_mem hm, ← ih, dedup_cons_of_mem,
        List.Subset.dedup_append_right (map_mk_sublist_sym2 _ _ hm).subset]
      refine mem_append_left _ ?_
      rw [mem_map]
      exact ⟨_, hm, Sym2.eq_swap⟩
    · rw [dedup_cons_of_notMem hm, List.sym2, map_cons, ← ih, dedup_cons_of_notMem, cons_append,
        List.Disjoint.dedup_append, dedup_map_of_injective]
      · exact (Sym2.mkEmbedding _).injective
      · exact map_mk_disjoint_sym2 x xs hm
      · simp [hm, mem_sym2_iff]

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ xs.sym2.dedup = xs.dedup.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
⊢ (map g s).sym n = map { toFun := Sym.map ⇑g, inj' := ⋯ } (s.sym n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
ha : a ∈ s
n : ℕ
b : α
hb : b ∈ Sym.replicate n a
⊢ b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
h : s.sym n = ∅
⊢ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs ys : List α
h : xs ~ ys
⊢ xs.sym2 ~ ys.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
⊢ (s ∩ t).sym n = s.sym n ∩ t.sym n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs ys : List α
h : xs <+ ys
⊢ xs.sym2 <+ ys.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ (Sym.filterNe a ↑m).snd ∈ s.sym (n - ↑(Sym.filterNe a ↑m).fst)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs ys : List α
h : xs <+~ ys
⊢ xs.sym2 <+~ ys.sym2

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
⊢ xs.sym2.length = (xs.length + 1).choose 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
x✝ : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))
i : Fin (n + 1)
m : Sym α (n - ↑i)
hm : m ∈ s.sym (n - ↑i)
⊢ (fun m ↦ ⟨(Sym.filterNe a ↑m).fst, ⟨(Sym.filterNe a ↑m).snd, ⋯⟩⟩)
      ((fun m ↦ ⟨Sym.fill a m.fst ↑m.snd, ⋯⟩) ⟨i, ⟨m, hm⟩⟩) =
    ⟨i, ⟨m, hm⟩⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
⊢ List.sym 1 xs = map (fun x ↦ x ::ₛ Sym.nil) xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ ∀ x ∈ s, x ^ Multiset.count x ↑k = x ^ Multiset.count x ↑k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
⊢ (↑k).prod = ∏ d ∈ s, d ^ Multiset.count d ↑k

Tactic:
by

Goal state after: