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_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
h : ⇑(hf.map hg LinearMap.id i) = ⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(hf.map hg LinearMap.id i)

Tactic:
simpa using

Goal state after:
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_8
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₂
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : M₁ →ₗ[R] N₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₂ →ₗ[R] N₂
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₁
h : ⇑(hf.map hg LinearMap.id i) = ⇑hg.equiv ∘ ⇑(LinearMap.lTensor M₁ i) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(LinearMap.lTensor M₁ i)
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
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₁
inst✝¹ : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₂
h : ⇑(hf.map hg i LinearMap.id) = ⇑hg.equiv ∘ ⇑(LinearMap.rTensor M₂ i) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(hf.map hg i LinearMap.id)

Tactic:
simpa using

Goal state after:
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
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : AddCommMonoid N₁
inst✝¹ : Module R N₁
f : M₁ →ₗ[R] M₂ →ₗ[R] M
hf : IsTensorProduct f
g : N₁ →ₗ[R] M₂ →ₗ[R] N
hg : IsTensorProduct g
i : M₁ →ₗ[R] N₁
hi : Function.Injective ⇑i
inst✝ : Module.Flat R M₂
h : ⇑(hf.map hg i LinearMap.id) = ⇑hg.equiv ∘ ⇑(LinearMap.rTensor M₂ i) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(LinearMap.rTensor M₂ i)
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₁
h : ⇑(hf.map hg i₁ i₂) = ⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(hf.map hg i₁ i₂)

Tactic:
simpa using

Goal state after:
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₁
h : ⇑(hf.map hg i₁ i₂) = ⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(TensorProduct.map i₁ i₂)
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₂
h : ⇑(hf.map hg i₁ i₂) = ⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(hf.map hg i₁ i₂)

Tactic:
simpa using

Goal state after:
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₂
h : ⇑(hf.map hg i₁ i₂) = ⇑hg.equiv ∘ ⇑(TensorProduct.map i₁ i₂) ∘ ⇑hf.equiv.symm
⊢ Function.Injective ⇑(TensorProduct.map i₁ i₂)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Bijective f
s : Finset α
⊢ (image f s).dens = s.dens

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Bijective f
s : Finset α
⊢ (image f s).dens = s.dens
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ s.dens ≤ 1

Tactic:
simpa using

Goal state after:
case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ s.dens ≤ 1
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
x✝ : z = 0
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
x✝ : z = 0
⊢ False
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
⊢ False

Tactic:
have h_notReduced : ¬IsReduced (C ⊗[R] D) := by
    simp_rw [isReduced_iff, not_forall]
    exact ⟨z, (IsNilpotent.map_iff h_inj).mp hx.right, (by simpa [·] using hx.1)⟩

Goal state after:
R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
h_notReduced : ¬IsReduced (C ⊗[R] ↥D)
⊢ False
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: case refine_2
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝¹ : CommMonoid β
s : Finset ι
f : ι → κ → β
t : ι → Set κ
g : ι → κ
inst✝ : DecidablePred fun i ↦ g i ∈ t i
⊢ ∏ x ∈ s with g x ∉ t x, (t x).mulIndicator (f x) (g x) = 1

Tactic:
exact prod_eq_one fun x hx ↦ mulIndicator_of_notMem (mem_filter.1 hx).2 _

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ ∀ i ∈ {i ∈ t | q i}, f i = g i

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ ∀ i ∈ t, q i → f i = g i
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ 𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ ∑ x ∈ s, ∑ x_1 ∈ t, (↑(#s))⁻¹ • f x x_1 = ∑ j ∈ t, ∑ x ∈ s, (↑(#s))⁻¹ • f x j
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
f : ι → M
t : Finset κ
inst✝ : DecidableEq ι
m : κ → ι
hm : Set.InjOn m ↑t
⊢ (↑(#(image m t)))⁻¹ • ∑ x ∈ image m t, f x = (↑(#t))⁻¹ • ∑ x ∈ t, f (m x)

Tactic:
card_image_of_injOn hm,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
f : ι → M
t : Finset κ
inst✝ : DecidableEq ι
m : κ → ι
hm : Set.InjOn m ↑t
⊢ (↑(#t))⁻¹ • ∑ x ∈ image m t, f x = (↑(#t))⁻¹ • ∑ x ∈ t, f (m x)
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (i : ι), f i = g (e i)
⊢ Set.SurjOn e ↑univ ↑univ

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (i : ι), f i = g (e i)
⊢ Surjective e
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
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ i ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ (i j : ι), p i → p j → i = j
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 : α
f : α → α → β
p : Fin (k + 1) → α × α := ⋯
⊢ ∏ i ∈ range k, f (p ↑i).2 (p ↑i.succ).1 = ∏ z ∈ F, f z.1 z.2

Tactic:
apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))

Goal state after:
case hi
α : 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, ((p ↑a).2, (p ↑a.succ).1) ∈ F

case i_inj
α : 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, ∀ a₂ ∈ range k, ((p ↑a₁).2, (p ↑a₁.succ).1) = ((p ↑a₂).2, (p ↑a₂.succ).1) → a₁ = a₂

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

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
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
inst✝ : InvolutiveNeg α
f : α → β
hf : Function.Odd f
s : Finset α
hs : Finset.map (Equiv.toEmbedding (Equiv.neg α)) s = s
⊢ s.sum f = 0

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
inst✝ : InvolutiveNeg α
f : α → β
hf : Function.Odd f
s : Finset α
hs : Finset.map (Equiv.toEmbedding (Equiv.neg α)) s = s
⊢ s.sum f = 0
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
this : TensorProduct.lift f = ↑e
⊢ IsTensorProduct f

Tactic:
simpa using

Goal state after:
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
this : TensorProduct.lift f = ↑e
⊢ Function.Bijective ⇑e
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
    change hf.equiv.symm (s • _) = _
    dsimp
    rw [← map_smul]
    apply hf.equiv_symm_apply

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:
simpa using

Goal state after:
n : ℕ
l : List ℕ
h : ∀ x ∈ l, x ≡ 1 [MOD n]
⊢ l.prod ≡ 1 [MOD n]
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:
simpa using

Goal state after:
α : Type u_1
n : ℕ
l : List α
f : α → ℕ
h : ∀ x ∈ l, f x ≡ 0 [MOD n]
⊢ (List.map f l).sum ≡ 0 [MOD n]
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:
simpa using

Goal state after:
n : ℕ
l : List ℕ
h : ∀ x ∈ l, x ≡ 0 [MOD n]
⊢ l.sum ≡ 0 [MOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

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

Tactic:
simpa using

Goal state after:
case mk
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [MOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [MOD n]
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:
simpa using

Goal state after:
α : Type u_1
n : ℕ
f : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 1 [MOD n]
⊢ (Multiset.map f s).prod ≡ 1 [MOD n]
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:
simpa using

Goal state after:
n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 1 [MOD n]
⊢ s.prod ≡ 1 [MOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

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

Tactic:
simpa using

Goal state after:
case mk
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [MOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [MOD n]
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:
simpa using

Goal state after:
α : Type u_1
n : ℕ
f : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ 0 [MOD n]
⊢ (Multiset.map f s).sum ≡ 0 [MOD n]
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:
simpa using

Goal state after:
n : ℕ
s : Multiset ℕ
h : ∀ x ∈ s, x ≡ 0 [MOD n]
⊢ s.sum ≡ 0 [MOD n]
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:
simpa using

Goal state after:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [MOD n]
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:
simpa using

Goal state after:
α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ 0 [MOD n]
⊢ ∑ x ∈ s, f x ≡ 0 [MOD n]
Module: Mathlib.RingTheory.IsTensorProduct

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

Tactic:
| tmul x z =>

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:
simpa using

Goal state after:
n : ℤ
l : List ℤ
h : ∀ x ∈ l, x ≡ 1 [ZMOD n]
⊢ l.prod ≡ 1 [ZMOD n]
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:
simpa using

Goal state after:
α : Type u_1
n : ℤ
l : List α
f : α → ℤ
h : ∀ x ∈ l, f x ≡ 0 [ZMOD n]
⊢ (List.map f l).sum ≡ 0 [ZMOD n]
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:
simpa using

Goal state after:
n : ℤ
l : List ℤ
h : ∀ x ∈ l, x ≡ 0 [ZMOD n]
⊢ l.sum ≡ 0 [ZMOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

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

Tactic:
simpa using

Goal state after:
case mk
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [ZMOD n]
⊢ (List.map f l).prod ≡ (List.map g l).prod [ZMOD n]