mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∈ range ⇑P.root
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

Tactic:
·

Goal state after:
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
h₆ : P.root l + P.root ↑i ∉ range ⇑P.root
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case refine_1
ι : 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
w : ↥b.support ⊕ ι → K
hw : w ∈ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0)
i : ι
⊢ w (Sum.inr i) = 0

pp: case refine_2
ι : 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
⊢ span K (range u) ≤ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0)

Tactic:
·

Goal state after:
case refine_1
ι : 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
w : ↥b.support ⊕ ι → K
hw : w ∈ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0)
i : ι
⊢ w (Sum.inr i) = 0
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
h₂ : ↑p = 0
⊢ ∑ x ∈ Finset.range p, (Ideal.Quotient.mk I) y ^ (x + (p - 1 - x)) =
    ∑ x ∈ Finset.range p, (Ideal.Quotient.mk I) y ^ (p - 1)

pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
h₂ : ↑p = 0
⊢ ∑ x ∈ Finset.range p, (Ideal.Quotient.mk I) y ^ (p - 1) = 0

Tactic:
·

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
h₂ : ↑p = 0
⊢ ∑ x ∈ Finset.range p, (Ideal.Quotient.mk I) y ^ (x + (p - 1 - x)) =
    ∑ x ∈ Finset.range p, (Ideal.Quotient.mk I) y ^ (p - 1)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case refine_2
ι : 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
⊢ span K (range u) ≤ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0)

Tactic:
·

Goal state after:
case refine_2
ι : 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
⊢ span K (range u) ≤ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: case refine_1
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), 0 ≤ (B x) x
x : n → R
⊢ 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x

pp: case refine_2
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x
x : M
⊢ 0 ≤ (B x) x

Tactic:
·

Goal state after:
case refine_1
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : M), 0 ≤ (B x) x
x : n → R
⊢ 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: case refine_2
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x
x : M
⊢ 0 ≤ (B x) x

Tactic:
·

Goal state after:
case refine_2
M : Type u_2
n : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_4
inst✝³ : CommRing R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
h : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ ((toMatrix₂ b b) B).mulVec x
x : M
⊢ 0 ≤ (B x) x
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : ¬P.root k = P.root l + P.root ↑i - P.root ↑j
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : P.root k = P.root l + P.root ↑i - P.root ↑j
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0

Tactic:
·

Goal state after:
case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
h₅ : P.root l + P.root ↑i - P.root ↑j ∈ range ⇑P.root
m : ι
hm : P.root m = P.root l - P.root ↑j
l' : ι
hl' : P.root l' = P.root l + P.root ↑i
hk : ¬P.root k = P.root l + P.root ↑i - P.root ↑j
⊢ (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
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.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) := { toSubmodule := ↑U, lie_mem := ⋯ }
hU : ↑U ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i, c i • u i = x
hCM : c ≠ 0
this : ((Int.castRingHom K).mapMatrix (4 - b.cartanMatrix)).det = 0
⊢ (4 - b.cartanMatrix).det = 0

Tactic:
simpa only [← RingHom.map_det, eq_intCast, Int.cast_eq_zero] using this

Goal state after:
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.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : IsAlgClosed K
h✝ : IsEmpty ι
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)

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.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : IsAlgClosed K
h✝ : Nonempty ι
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)

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.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : IsAlgClosed K
h✝ : IsEmpty ι
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
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.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : IsAlgClosed K
h✝ : Nonempty ι
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)

Tactic:
·

Goal state after:
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.IsRootSystem
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : P.IsReduced
inst✝¹ : P.IsIrreducible
inst✝ : IsAlgClosed K
h✝ : Nonempty ι
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)
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
h : 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
h : 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
h : IsEmpty ι
⊢ (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 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
h : 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.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
h : 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 e'_1
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
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f i) = (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) i_1

pp: case e'_2
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
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f (e i)) =
    (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) (e i_1)

Tactic:
·

Goal state after:
case e'_1
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
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f i) = (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) i_1
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: case e'_2
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
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f (e i)) =
    (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) (e i_1)

Tactic:
·

Goal state after:
case e'_2
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
h : Nonempty ι
i : ι := h.some
⊢ (r • (PiTensorProduct.tprod R) fun i ↦ f (e i)) =
    (PiTensorProduct.tprod R) fun i_1 ↦ Function.update f i (r • f i) (e i_1)
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: case inl
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ m - n
⊢ p ∣ a

pp: case inr
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ a
⊢ p ∣ a

Tactic:
·

Goal state after:
case inl
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ m - n
⊢ p ∣ a
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: case inr
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ a
⊢ p ∣ a

Tactic:
·

Goal state after:
case inr
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this : p ∣ (m - n) * a
hp : p ∣ a
⊢ p ∣ a
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: case inr
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄, i ≠ j → i < j → (Coprime on coprimes a) i j
ltij : j ≤ i
⊢ (Coprime on coprimes a) i j

pp: m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
⊢ (Coprime on coprimes a) i j

Tactic:
·

Goal state after:
case inr
m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
this : ∀ {m : ℕ} (a : Fin m → ℕ) ⦃i j : Fin m⦄, i ≠ j → i < j → (Coprime on coprimes a) i j
ltij : j ≤ i
⊢ (Coprime on coprimes a) i j
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: m✝ m : ℕ
a : Fin m → ℕ
i j : Fin m
hij : i ≠ j
ltij : i < j
hja : ↑j < supOfSeq a
⊢ 0 < ↑j + 1 - (↑i + 1)

Tactic:
by lia

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
⊢ count b s = count b t

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
⊢ count a s < count a t

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
⊢ count b s = count b t
Module: Mathlib.Logic.Hydra

Goal state before:
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
⊢ count a s < count a t

Tactic:
·

Goal state after:
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
⊢ count a s < count a t
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s t : Multiset α
a : α
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a → (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t

pp: case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s t : Multiset α
a : α
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t → (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s t : Multiset α
a : α
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a → (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s t : Multiset α
a : α
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t → (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableEq α
inst✝ : Std.Irrefl r
s' s t : Multiset α
a : α
⊢ (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t → (∀ a' ∈ t, r a' a) ∧ a ∈ s + t ∧ s' = (s + t).erase a
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a

pp: case inr
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₂ + t
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a

Tactic:
·

Goal state after:
case inl
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ ∃ a', GameAdd (CutExpand r) (CutExpand r) a' (s₁, s₂) ∧ a'.1 + a'.2 = (s₁ + s₂ + t).erase a
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case inl.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ s₁.erase a + t + {a} = s₁ + t

pp: case inl.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a

Tactic:
·

Goal state after:
case inl.refine_1
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ s₁.erase a + t + {a} = s₁ + t
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case inl.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a

Tactic:
·

Goal state after:
case inl.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a