mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k : ι
hk : P.root k ∉ allRoots P
aux : P.IsOrthogonal k (short P) ∧ P.IsOrthogonal k (long P)
⊢ P.IsOrthogonal k (long P)

pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k : ι
hk : P.root k ∉ allRoots P
aux : P.IsOrthogonal k (short P) ∧ P.IsOrthogonal k (long P)
⊢ P.IsOrthogonal k (short P)

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k : ι
hk : P.root k ∉ allRoots P
aux : P.IsOrthogonal k (short P) ∧ P.IsOrthogonal k (long P)
⊢ P.IsOrthogonal k (long P)

case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this :
  (∀ (j : ι), P.root j ∉ Submodule.span R {longRoot P, shortRoot P} → ∀ i ∈ {long P, short P}, P.IsOrthogonal j i) →
    Submodule.span R {longRoot P, shortRoot P} = ⊤
k : ι
hk : P.root k ∉ allRoots P
aux : P.IsOrthogonal k (short P) ∧ P.IsOrthogonal k (long P)
⊢ P.IsOrthogonal k (short P)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case inl
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i j : ↥b.support
⊢ (ω b *ᵥ u i) (Sum.inl j) = u i (Sum.inl j)

pp: case inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i : ↥b.support
j : ι
⊢ (ω b *ᵥ u i) (Sum.inr j) = u i (Sum.inr j)

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i j : ↥b.support
⊢ (ω b *ᵥ u i) (Sum.inl j) = u i (Sum.inl j)

case inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i : ↥b.support
j : ι
⊢ (ω b *ᵥ u i) (Sum.inr j) = u i (Sum.inr j)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case inl
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i : ι
j : ↥b.support
⊢ (ω b *ᵥ v b i) (Sum.inl j) = v b (-i) (Sum.inl j)

pp: case inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i j : ι
⊢ (ω b *ᵥ v b i) (Sum.inr j) = v b (-i) (Sum.inr j)

Tactic:
<;>

Goal state after:
case inl
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i : ι
j : ↥b.support
⊢ (ω b *ᵥ v b i) (Sum.inl j) = v b (-i) (Sum.inl j)

case inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i✝ : ι
hi : v b i✝ ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i j : ι
⊢ (ω b *ᵥ v b i) (Sum.inr j) = v b (-i) (Sum.inr j)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h₀
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ (i : ι),
    (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U) →
      ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b ((P.reflectionPerm i) i) ∈ U → ∃ j, u j ∈ U

Tactic:
intro i h U hi
      replace hi : v b i ∈ ωConjLieSubmodule U := by simpa [hωv]
      obtain ⟨j, hj⟩ := h hi
      exact ⟨j, by simpa [hωu] using! hj⟩

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: case hx
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ e₀ i ∈ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)

pp: case hy
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ f₀ i ∈ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)

Tactic:
<;>

Goal state after:
case hx
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ e₀ i ∈ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)

case hy
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ f₀ i ∈ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
⊢ P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ k j = 2

Tactic:
suffices 0 < - P.pairingIn ℤ i j ∧ - P.pairingIn ℤ i j < P.pairingIn ℤ k j ∧
      P.pairingIn ℤ k j ≤ 2 by lia

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝² : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : P.IsNotG2
this : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j ≠ 0
aux₀ : P.pairingIn ℤ j i = P.pairingIn ℤ k i
⊢ 0 < -P.pairingIn ℤ i j ∧ -P.pairingIn ℤ i j < P.pairingIn ℤ k j ∧ P.pairingIn ℤ k j ≤ 2
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
this : ∀ (j : ι), v b j ∈ U
⊢ U = ⊤

Tactic:
simp_rw [← LieSubmodule.toSubmodule_eq_top, eq_top_iff,
      ← (Pi.basisFun K (b.support ⊕ ι)).span_eq, Submodule.span_le, range_subset_iff,
      Pi.basisFun_apply]
    aesop

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case of.perm.left
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
⊢ IsEmpty ι →
    (addConGen (Rel R ι M)) (r • (PiTensorProduct.tprod R) fun i ↦ f i) (r • (PiTensorProduct.tprod R) fun i ↦ f (e i))

pp: case of.perm.right
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
⊢ Nonempty ι →
    (addConGen (Rel R ι M)) (r • (PiTensorProduct.tprod R) fun i ↦ f i) (r • (PiTensorProduct.tprod R) fun i ↦ f (e i))

Tactic:
<;>

Goal state after:
case of.perm.left
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
⊢ IsEmpty ι →
    (addConGen (Rel R ι M)) (r • (PiTensorProduct.tprod R) fun i ↦ f i) (r • (PiTensorProduct.tprod R) fun i ↦ f (e i))

case of.perm.right
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y : ⨂[R] (x : ι), M
e : Perm ι
f : ι → M
⊢ Nonempty ι →
    (addConGen (Rel R ι M)) (r • (PiTensorProduct.tprod R) fun i ↦ f i) (r • (PiTensorProduct.tprod R) fun i ↦ f (e i))
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • x✝) ?trans.y

pp: case trans.a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) ?trans.y (r • z✝)

pp: case trans.y
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ ⨂[R] (x : ι), M

Tactic:
<;>

Goal state after:
case a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • x✝) ?trans.y

case trans.a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) ?trans.y (r • z✝)

case trans.y
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) x✝ y✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • x✝) (r • y✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ ⨂[R] (x : ι), M
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case add.a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y w✝ x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) w✝ x✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • w✝) (r • x✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • w✝) (r • x✝)

pp: case a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y w✝ x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) w✝ x✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • w✝) (r • x✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • y✝) (r • z✝)

Tactic:
<;>

Goal state after:
case add.a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y w✝ x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) w✝ x✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • w✝) (r • x✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • w✝) (r • x✝)

case a
R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x y w✝ x✝ y✝ z✝ : ⨂[R] (x : ι), M
a✝¹ : AddConGen.Rel (Rel R ι M) w✝ x✝
a✝ : AddConGen.Rel (Rel R ι M) y✝ z✝
a_ih✝¹ : (addConGen (Rel R ι M)) (r • w✝) (r • x✝)
a_ih✝ : (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
⊢ (addConGen (Rel R ι M)) (r • y✝) (r • z✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Matrix

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
ι : Type u_7
κ : Type u_8
τ : Type u_9
inst✝¹² : DecidableEq ι
inst✝¹¹ : DecidableEq κ
inst✝¹⁰ : DecidableEq τ
inst✝⁹ : Fintype ι
inst✝⁸ : Fintype κ
inst✝⁷ : Fintype τ
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
⊢ (toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP)))
      ↑(TensorProduct.assoc R M N P) =
    submatrix 1 _root_.id ⇑(Equiv.prodAssoc ι κ τ)

Tactic:
ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩
  simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, assoc_tmul,
    Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ k',
    @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, @eq_comm _ i',
    submatrix_apply, Matrix.one_apply, id_eq, Equiv.prodAssoc_apply, Prod.mk.injEq]

Goal state after:
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
b : α
h : (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) b a
⊢ (toFinsupp s) b = (toFinsupp t) b

pp: case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
⊢ (fun {i} x1 x2 ↦ x1 < x2) ((toFinsupp s) a) ((toFinsupp t) a)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
b : α
h : (rᶜ ⊓ fun x1 x2 ↦ x1 ≠ x2) b a
⊢ (toFinsupp s) b = (toFinsupp t) b

case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s t u : Multiset α
a : α
he : s + {a} = t + u
hr : ∀ (a' : α), ¬r a' a → a' ∉ u
⊢ (fun {i} x1 x2 ↦ x1 < x2) ((toFinsupp s) a) ((toFinsupp t) a)
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case e'_1.e'_3
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ s' + t = t + s'

pp: case e'_1.e'_4
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ s + t = t + s

Tactic:
<;>

Goal state after:
case e'_1.e'_3
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ s' + t = t + s'

case e'_1.e'_4
α : Type u_1
r : α → α → Prop
s' s t : Multiset α
⊢ s + t = t + s
Module: Mathlib.Logic.Hydra

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2

Tactic:
rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩

Goal state after:
α : Type u_1
r : α → α → Prop
s₁ s₂ s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : s + {a} = (fun s ↦ s.1 + s.2) (s₁, s₂) + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ (fun s ↦ s.1 + s.2) a' = s
Module: Mathlib.MeasureTheory.Category.MeasCat

Goal state before:
pp: case hf
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun x ↦ x

pp: case hg
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun m ↦ ∫⁻ (x : ℝ≥0∞), x ∂m

pp: μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ AEMeasurable (fun x ↦ x) μ.join

Tactic:
<;>

Goal state after:
case hf
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun x ↦ x

case hg
μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ Measurable fun m ↦ ∫⁻ (x : ℝ≥0∞), x ∂m

μ : MeasureTheory.Measure (MeasureTheory.Measure ℝ≥0∞)
⊢ AEMeasurable (fun x ↦ x) μ.join
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case pos
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ ⋂ x ∈ ∅, s x ∈ 𝒜

Tactic:
biInter_empty

Goal state after:
case pos
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ univ ∈ 𝒜
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
ι : Type u_3
a : Finset ι
f : ι → Set α
hf : ∀ i ∈ a, f i ∈ C
h_dis : (↑a).PairwiseDisjoint f
h_mem : ⋃ i ∈ a, f i ∈ C
⊢ m (⋃ i ∈ a, f i) = ∑ i ∈ a, m (f i)

Tactic:
by
  have A : ⋃ i ∈ a, f i = ⋃₀ (a.image f) := by simp
  rw [A, addContent_sUnion]; rotate_left
  · grind
  · simpa using! h_dis.image
  · rwa [← A]
  rw [sum_image_of_pairwise_eq_zero]
  refine h_dis.imp ?_
  grind [Set.bot_eq_empty (α := α), addContent_empty]

Goal state after: