mathlib-initiative/mathlib-tactics huggingface dataset:
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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ι
hml : m ≠ l
contra : P.root m = P.root ↑i + P.root k
⊢ P.root m = P.root j + (n + 1) • P.root ↑i

Tactic:
contra,

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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ι
hml : m ≠ l
contra : P.root m = P.root ↑i + P.root k
⊢ P.root ↑i + P.root k = P.root j + (n + 1) • P.root ↑i
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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ι
hml : m ≠ l
contra : P.root m = P.root ↑i + P.root k
⊢ P.root m = P.root l

Tactic:
rw [hl, contra, hk₁]

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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
m : ι
hml : m ≠ l
contra : P.root m = P.root ↑i + P.root k
⊢ P.root ↑i + (P.root j + n • P.root ↑i) = P.root j + (n + 1) • P.root ↑i
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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
hij : P.root j + (n + 1) • P.root ↑i ∉ range ⇑P.root
l : ι
contra : P.root l = P.root ↑i + P.root k
⊢ P.root l = P.root j + (n + 1) • P.root ↑i

Tactic:
contra,

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
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
hij : P.root j + (n + 1) • P.root ↑i ∉ range ⇑P.root
l : ι
contra : P.root l = P.root ↑i + P.root k
⊢ P.root ↑i + P.root k = P.root j + (n + 1) • P.root ↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : 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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
A : ↥(lieAlgebra b)
x : ↥b.support ⊕ ι → R
hx : x ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier
⊢ ⁅A, x⁆ ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier

Tactic:
let A' : lieAlgebra b := ⟨ωConj b _, ωConj_mem_of_mem A.property⟩

Goal state after:
ι : 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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
A : ↥(lieAlgebra b)
x : ↥b.support ⊕ ι → R
hx : x ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier
A' : ↥(lieAlgebra b) := ⟨(ωConj b) ↑A, ⋯⟩
⊢ ⁅A, x⁆ ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : 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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
A : ↥(lieAlgebra b)
x : ↥b.support ⊕ ι → R
hx : x ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier
⊢ ⁅A, x⁆ ∈ (comap (Matrix.toLin' (ω b)) ↑N).carrier

Tactic:
by
    let A' : lieAlgebra b := ⟨ωConj b _, ωConj_mem_of_mem A.property⟩
    suffices ⁅A', ω b *ᵥ x⁆ ∈ N by simpa [A', mul_assoc] using this
    exact LieSubmodule.lie_mem _ hx

Goal state after:
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₃ : 2 * (x + 1) + A * (y - 1) ∈ s
⊢ False

Tactic:
replace h₀ : 2 * x + A * y ∈ s := by
    convert! IsG2.pairingIn_mem_zero_one_three P k i hki hki'
    rw [pairingIn_eq_add_of_root_eq_smul_add_smul (j := i) h₀.symm, pairingIn_same,
      Int.zsmul_eq_mul, Int.zsmul_eq_mul]
    ring

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 : ℤ
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₃ : 2 * (x + 1) + A * (y - 1) ∈ s
h₀ : 2 * x + A * y ∈ s
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : 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
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hc :
  (P.pairingIn ℤ i (shortAddLong P), P.pairingIn ℤ (shortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hd :
  (P.pairingIn ℤ i (twoShortAddLong P), P.pairingIn ℤ (twoShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
he :
  (P.pairingIn ℤ i (threeShortAddLong P), P.pairingIn ℤ (threeShortAddLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hf :
  (P.pairingIn ℤ i (threeShortAddTwoLong P), P.pairingIn ℤ (threeShortAddTwoLong P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0

Tactic:
apply isOrthogonal_short_and_long_aux rfl ha hb hc hd he hf <;> simp

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.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)

Tactic:
simp [ω, u, Pi.single_apply, one_apply]

Goal state after:
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.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:
simp [ω, u, Pi.single_apply, one_apply]

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

Goal state before:
pp: case inr
ι : 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
this : chainBotCoeff i m = 1 ∧ chainBotCoeff j (-l) = 0
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j = 0
⊢ False

Tactic:
rw [chainBotCoeff_if_one_zero hjl_mem] at this

Goal state after:
case inr
ι : 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
this : chainBotCoeff i m = 1 ∧ (if P.pairingIn ℤ j (-l) = 0 then 1 else 0) = 0
hmi : P.pairingIn ℤ m i = 0
hlj : P.pairingIn ℤ l j = 0
⊢ False
Module: Mathlib.LinearAlgebra.SesquilinearForm.Star

Goal state before:
pp: R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Fintype n
inst✝ : DecidableEq n
B : M →ₗ⋆[R] M →ₗ[R] R
b : Basis n R M
⊢ B.IsSymm ↔ ((toMatrix₂ b b) B).IsHermitian

Tactic:
by
  rw [isSymm_iff_basis b, Matrix.IsHermitian.ext_iff, forall_comm]
  simp [Eq.comm]

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

Tactic:
simp_rw [toFinsupp_apply]

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
⊢ (fun {i} x1 x2 ↦ x1 < x2) ((toFinsupp s) a) ((toFinsupp t) a)

Tactic:
simp_rw [toFinsupp_apply]

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.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
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 : f ∈ (↑s₁).pi t₁ ∩ (↑s₂).pi t₂
⊢ (t₁' i ∩ t₂' i).Nonempty

Tactic:
rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf

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
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
⊢ (t₁' i ∩ t₂' i).Nonempty
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
this : ∀ (I : Finset ι), (P I) univ = 0
⊢ (P I) S = (P J) T

Tactic:
by
      simp only [Measure.measure_univ_eq_zero] at this
      simp [this]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : accumulate s n ∈ C
⊢ accumulate s (n + 1) ∈ C

Tactic:
rw [accumulate_succ]

Goal state after:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
n : ℕ
hn : accumulate s n ∈ C
⊢ accumulate s n ∪ s (n + 1) ∈ C
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case hC
α : Type u_1
𝒜 : Set (Set α)
s t : Set α
ht : t ∈ generateSetAlgebra 𝒜
h : MeasurableSet t
⊢ MeasurableSet t

Tactic:
| hC t ht h =>

Goal state after:
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
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
s : Set α
hs : s ∈ J
⊢ s ⊆ ⋃ i ∈ ↑J', i

Tactic:
← sUnion_eq_biUnion,

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
s : Set α
hs : s ∈ J
⊢ s ⊆ ⋃₀ ↑J'
Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
hP : IsProjectiveMeasureFamily P
⊢ projectiveFamilyFun P ∅ = 0

Tactic:
projectiveFamilyFun_congr hP (empty_mem_measurableCylinders α) (cylinder_empty ∅).symm
    MeasurableSet.empty,

Goal state after:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
hP : IsProjectiveMeasureFamily P
⊢ (P ∅) ∅ = 0
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
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
⊢ t ⊆ ⋃ i ∈ ↑J, i

Tactic:
← sUnion_eq_biUnion,

Goal state after:
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
J J' : Finset (Set α)
hJ : ↑J ⊆ C
hJdisj : (↑J).PairwiseDisjoint id
hJ' : ↑J' ⊆ C
hJ'disj : (↑J').PairwiseDisjoint id
h : ⋃₀ ↑J = ⋃₀ ↑J'
t : Set α
ht : t ∈ J'
⊢ t ⊆ ⋃₀ ↑J
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : ι
b : WithTop ι
hb : b ∈ Ioi ↑a
⊢ ∃ t ⊆ Ioi ↑a, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ b ∈ t

Tactic:
induction b with

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃ i, disjointed (fun i ↦ ↑(J.equivFin.symm i)) i
⊢ m t ≤ ∑ u ∈ J, m u

Tactic:
set f := disjointed fun j => (J.equivFin.symm j).1

Goal state after:
α : Type u_1
C : Set (Set α)
t : Set α
G : Type u_2
inst✝² : AddCommMonoid G
inst✝¹ : PartialOrder G
inst✝ : CanonicallyOrderedAdd G
m : AddContent G C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
f : Fin #J → Set α := disjointed fun j ↦ ↑(J.equivFin.symm j)
htJ : t ⊆ ⋃ i, f i
⊢ m t ≤ ∑ u ∈ J, m u
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.coe
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : ι
b : WithTop ι
hb : b ∈ Iio ↑a
⊢ ∃ t ⊆ Iio ↑a, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ b ∈ t

Tactic:
induction b with

Goal state after:
Module: Mathlib.MeasureTheory.Function.UniformIntegrable

Goal state before:

Tactic:
eLpNorm (s.indicator (E.indicator (f i))) p μ
      = eLpNorm (E.indicator (s.indicator (f i))) p μ := by
      simp only [indicator_indicator, inter_comm]
    _ ≤ eLpNorm (s.indicator (f i)) p μ := eLpNorm_indicator_le _
    _ ≤ ENNReal.ofReal ε := hε _ _ hs hμs

Goal state after: