mathlib-initiative/mathlib-tactics huggingface dataset:
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
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : P.root n = (x + 1) • P.root i + (y - 1) • P.root j
⊢ 2 * (x + 1) + A * (y - 1) = P.pairingIn ℤ n i

Tactic:
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (S := ℤ) (j := i) h₃, pairingIn_same,
      Int.zsmul_eq_mul, Int.zsmul_eq_mul]

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
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₁ : 2 * (x + 1) + A * y ∈ s
h₂ : 2 * x + A * (y - 1) ∈ s
h₃ : P.root n = (x + 1) • P.root i + (y - 1) • P.root j
⊢ 2 * (x + 1) + A * (y - 1) = (x + 1) * 2 + (y - 1) * P.pairingIn ℤ j i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr
ι : 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
k l : ι
⊢ ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)

Tactic:
simp only [h, e, indexNeg_neg, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply,
      Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁, Matrix.zero_apply, Matrix.fromBlocks_apply₁₂,
      Matrix.of_apply, mul_ite, mul_one, mul_zero, ite_self, Finset.sum_const_zero,
      Matrix.fromBlocks_apply₂₂, zero_add, ite_mul, zero_mul, Matrix.smul_apply, smul_ite, smul_add,
      zsmul_eq_mul, smul_zero]

Goal state after:
case inr.inr
ι : 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
k l : ι
⊢ ((∑ a₂,
        if P.root a₂ = P.root ↑i + P.root l then
          Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k a₂ * (↑(chainBotCoeff (↑i) l) + 1)
        else 0) -
      ∑ a₂,
        if P.root k = P.root ↑i + P.root a₂ then
          (↑(chainBotCoeff (↑i) a₂) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) a₂ l
        else 0) =
    if P.root k = P.root ↑i + P.root l then ↑(b.cartanMatrix i j) * ↑(chainBotCoeff (↑i) l) + ↑(b.cartanMatrix i j)
    else 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr
ι : 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
k l : ι
⊢ ∑ x ∈ {k, l},
      ((if P.root x = P.root ↑i + P.root l then
          Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k x * (↑(chainBotCoeff (↑i) l) + 1)
        else 0) -
        if P.root k = P.root ↑i + P.root x then
          (↑(chainBotCoeff (↑i) x) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) x l
        else 0) =
    if P.root k = P.root ↑i + P.root l then ↑(b.cartanMatrix i j) * ↑(chainBotCoeff (↑i) l) + ↑(b.cartanMatrix i j)
    else 0

Tactic:
rcases eq_or_ne k l with rfl | hkl

Goal state after:
case inr.inr.inl
ι : 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
k : ι
⊢ ∑ x ∈ {k, k},
      ((if P.root x = P.root ↑i + P.root k then
          Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k x * (↑(chainBotCoeff (↑i) k) + 1)
        else 0) -
        if P.root k = P.root ↑i + P.root x then
          (↑(chainBotCoeff (↑i) x) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) x k
        else 0) =
    if P.root k = P.root ↑i + P.root k then ↑(b.cartanMatrix i j) * ↑(chainBotCoeff (↑i) k) + ↑(b.cartanMatrix i j)
    else 0

case inr.inr.inr
ι : 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
k l : ι
hkl : k ≠ l
⊢ ∑ x ∈ {k, l},
      ((if P.root x = P.root ↑i + P.root l then
          Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k x * (↑(chainBotCoeff (↑i) l) + 1)
        else 0) -
        if P.root k = P.root ↑i + P.root x then
          (↑(chainBotCoeff (↑i) x) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) x l
        else 0) =
    if P.root k = P.root ↑i + P.root l then ↑(b.cartanMatrix i j) * ↑(chainBotCoeff (↑i) l) + ↑(b.cartanMatrix i j)
    else 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := ⋯
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
k : ι
x : ℕ
hij : ¬↑i = -↑i
hk₁ : P.root ↑i + (chainTopCoeff ↑i ↑i + 1) • P.root ↑i ∈ range ⇑P.root
⊢ (chainTopCoeff ↑i ↑i + 2) • P.root ↑i ∈ range ⇑P.root

Tactic:
convert! hk₁ using 1

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
k : ι
x : ℕ
hij : ¬↑i = -↑i
hk₁ : P.root ↑i + (chainTopCoeff ↑i ↑i + 1) • P.root ↑i ∈ range ⇑P.root
⊢ (chainTopCoeff ↑i ↑i + 2) • P.root ↑i = P.root ↑i + (chainTopCoeff ↑i ↑i + 1) • P.root ↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr.inr.inl
ι : 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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -↑i ≠ ↑i
hx : ∀ (x : ι), ¬(P.root x = P.root l - P.root ↑i ∧ P.root (-↑i) = P.root ↑i + P.root x)
aux : ∀ (x : ι), ¬P.root (-↑i) = P.root x - P.root ↑i
⊢ -(∑ x,
          ↑|b.cartanMatrix i x| *
            Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
              (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
              (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
              (Sum.inl x) (Sum.inr l) +
        ∑ a₂, if P.root a₂ = P.root ↑i + P.root l then 0 else 0) =
    if -↑i = l then ↑(P.pairingIn ℤ (-↑i) ↑i) else 0

Tactic:
rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by aesop)]

Goal state after:
case inr.inr.inr.inl
ι : 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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
l : ι
hki : -↑i ≠ ↑i
hx : ∀ (x : ι), ¬(P.root x = P.root l - P.root ↑i ∧ P.root (-↑i) = P.root ↑i + P.root x)
aux : ∀ (x : ι), ¬P.root (-↑i) = P.root x - P.root ↑i
⊢ -(↑|b.cartanMatrix i i| *
          Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
            (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
            (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
            (Sum.inl i) (Sum.inr l) +
        ∑ a₂, if P.root a₂ = P.root ↑i + P.root l then 0 else 0) =
    if -↑i = l then ↑(P.pairingIn ℤ (-↑i) ↑i) else 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr.inr.inr
ι : 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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
hki : k ≠ ↑i
hki' : k ≠ -↑i
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)

Tactic:
rcases eq_or_ne k l with rfl | hkl

Goal state after:
case inr.inr.inr.inr.inl
ι : 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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k : ι
hki : k ≠ ↑i
hki' : k ≠ -↑i
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr k) = h i (Sum.inr k) (Sum.inr k)

case inr.inr.inr.inr.inr
ι : 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 : ↥b.support
inst✝ : P.IsReduced
this✝¹ : InvolutiveNeg ι := P.indexNeg
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
k l : ι
hki : k ≠ ↑i
hki' : k ≠ -↑i
hkl : k ≠ l
⊢ ⁅e i, f i⁆ (Sum.inr k) (Sum.inr l) = h i (Sum.inr k) (Sum.inr l)
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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
⊢ genWeightSpace (↥U) 0 = ⊤

Tactic:
have : ⨆ (χ : H → K), ⨆ (_ : χ ≠ 0), (⊥ : LieSubmodule K H U) = ⊥ := biSup_const ⟨1, one_ne_zero⟩

Goal state after:
ι : 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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K), χ ≠ 0 → genWeightSpace (↥U) χ = ⊥
this : ⨆ χ, ⨆ (_ : χ ≠ 0), ⊥ = ⊥
⊢ genWeightSpace (↥U) 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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
i✝ : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
i : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b i ∈ U → ∃ j, u j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hi : v b i ∈ ωConjLieSubmodule U
j : ↥b.support
hj : u j ∈ ωConjLieSubmodule U
⊢ u j ∈ U

Tactic:
by simpa [hωu] using! hj

Goal state after:
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: case mul_comm
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
h : TensorAlgebra R M →ₐ[R] A
x✝² x✝¹ : TensorAlgebra R M
h' : (symRingCon R M) x✝² x✝¹
x✝ y✝ : TensorAlgebra R M
x y : M
⊢ (RingCon.ker h.toRingHom) ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)
    ((TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x)

Tactic:
| mul_comm x y
   => 

Goal state after:
case mul_comm
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
h : TensorAlgebra R M →ₐ[R] A
x✝² x✝¹ : TensorAlgebra R M
h' : (symRingCon R M) x✝² x✝¹
x✝ y✝ : TensorAlgebra R M
x y : M
⊢ (RingCon.ker h.toRingHom) ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)
    ((TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x)
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsSymmetricAlgebra (ι R M)

Tactic:
rw [IsSymmetricAlgebra, lift_ι]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Bijective ⇑(AlgHom.id R (SymmetricAlgebra R M))
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

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

Tactic:
exact AddCon.refl _ _

Goal state after:
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: m : ℕ
l : List ℕ
⊢ (↑Finset.univ).Pairwise (Function.onFun Coprime (coprimes fun x ↦ l[x]))

Tactic:
simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _)

Goal state after:
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: l : List ℕ
i : Fin l.length
⊢ (↑Finset.univ).Pairwise (Function.onFun Coprime (coprimes fun x ↦ l[x]))

Tactic:
simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _)

Goal state after:
Module: Mathlib.Logic.Hydra

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

Tactic:
obtain h | h := ha

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

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
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
⊢ IsPiSystem (squareCylinders C)

Tactic:
rintro S₁ ⟨s₁, t₁, h₁, rfl⟩ S₂ ⟨s₂, t₂, h₂, rfl⟩ hst_nonempty

Goal state after:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
⊢ (↑s₁).pi t₁ ∩ (↑s₂).pi t₂ ∈ squareCylinders C
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_2
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
⊢ f i ∈ t₂' i

Tactic:
by_cases hi₂ : i ∈ s₂

Goal state after:
case pos
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
hi₂ : i ∈ s₂
⊢ f i ∈ t₂' i

case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
f : (i : ι) → α i
hf : (∀ i ∈ ↑s₁, f i ∈ t₁' i) ∧ ∀ i ∈ ↑s₂, f i ∈ t₂' i
hi₂ : i ∉ s₂
⊢ f i ∈ t₂' i
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case pos
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₁ : i ∈ s₁
⊢ t₁' i ∈ C i

Tactic:
rw [← h1 i hi₁]
        exact h₁ i (mem_univ _)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_1.refine_2
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
⊢ t₂' i ∈ C i

Tactic:
by_cases hi₂ : i ∈ s₂

Goal state after:
case pos
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₂ : i ∈ s₂
⊢ t₂' i ∈ C i

case neg
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₂ : i ∉ s₂
⊢ t₂' i ∈ C i
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case pos
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
i : ι
this : (t₁' i ∩ t₂' i).Nonempty
hi₂ : i ∈ s₂
⊢ t₂' i ∈ C i

Tactic:
rw [← h2 i hi₂]
        exact h₂ i (mem_univ _)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ MeasurableSpace.comap (eval i) (m i) ≤ generateFrom ((fun t ↦ {i}.pi t) '' univ.pi fun i ↦ {s | MeasurableSet s})

Tactic:
by
  simp only [singleton_pi]
  rw [MeasurableSpace.comap_eq_generateFrom]
  refine MeasurableSpace.generateFrom_mono fun S ↦ ?_
  simp only [mem_ofPred_eq, mem_image, mem_univ_pi, forall_exists_index, and_imp]
  intro t ht h
  classical
  refine ⟨fun j ↦ if hji : j = i then by convert! t else univ, fun j ↦ ?_, ?_⟩
  · by_cases hji : j = i
    · simp only [hji, eq_mpr_eq_cast, dif_pos]
      convert! ht
      simp only [cast_heq]
    · simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]
  · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/
    simp [h]

Goal state after: