mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (of R 𝒜 ℬ)
      ((TensorProduct.congr ↑(decomposeAlgEquiv 𝒜) ↑(decomposeAlgEquiv ℬ)).symm
        (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((decompose 𝒜) a₁ ⊗ₜ[R] (DirectSum.of (fun i ↦ ↥(ℬ i)) j₁) b₁))
          ((DirectSum.of (fun i ↦ ↥(𝒜 i)) i₂) a₂ ⊗ₜ[R] (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))

Tactic:
← lof_eq_of R

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ i₂ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 i₂)
b₂ : B
⊢ (of R 𝒜 ℬ)
      ((TensorProduct.congr ↑(decomposeAlgEquiv 𝒜) ↑(decomposeAlgEquiv ℬ)).symm
        (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((decompose 𝒜) a₁ ⊗ₜ[R] (lof R ι (fun i ↦ ↥(ℬ i)) j₁) b₁))
          ((lof R ι (fun i ↦ ↥(𝒜 i)) i₂) a₂ ⊗ₜ[R] (decompose ℬ) b₂))) =
    (-1) ^ (j₁ * i₂) • (of R 𝒜 ℬ) ((a₁ * ↑a₂) ⊗ₜ[R] (↑b₁ * b₂))
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (TensorPower.cast R M ⋯) ((PiTensorProduct.tprod R) (Fin.append (fun x ↦ x₀) x)) =
    (PiTensorProduct.tprod R) (Fin.cons x₀ x)

Tactic:
rw [TensorPower.cast_tprod]

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (PiTensorProduct.tprod R) (Fin.append (fun x ↦ x₀) x ∘ Fin.cast ⋯) = (PiTensorProduct.tprod R) (Fin.cons x₀ x)
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
⊢ A.IsPivotedBy l ↔
    Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c

Tactic:
rw [isPivotedBy_iff]

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : PartialOrder m
inst✝ : LinearOrder n
⊢ (Monotone l ∧
      StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0) ↔
    Monotone l ∧ StrictMonoOn l {i | l i ≠ ⊤} ∧ ∀ (i : m), l i = ⊤ ∧ A i = 0 ∨ ∃ c, l i = ↑c ∧ A.IsLeadingEntry i c
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A
    else reduce (reduceStep A)) =
    (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A

Tactic:
simp_rw [if_pos hc, if_pos ha]

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → CommSemiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R := lift (MultilinearMap.mkPiAlgebra R ι R)
⊢ (Algebra.ofId R (⨂[R] (x : ι), R)).comp (AlgHom.ofLinearMap toFun ⋯ ⋯) = AlgHom.id R (⨂[R] (x : ι), R)

Tactic:
classical ext

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1

Tactic:
nth_rewrite 1 [show D.rep = (⟨D.rep, hD_mem⟩ : s) by rfl]

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ (b.repr ↑⟨D.rep, hD_mem⟩) ⟨D.rep, hD_mem⟩ = 1
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
L : Submodule F (ι → F) := F ∙ v
hA : A ∈ lineStab L
c : F
hcv : ↑(toLin' A) v = c • v
hcomap : F ∙ v ≤ Submodule.comap (↑(toLin' A)) (F ∙ v)
hres : (↑(toLin' A)).restrict hcomap = c • LinearMap.id
hQ : L.mapQ L (↑(toLin' A)) hcomap = LinearMap.id
hdet :
  LinearMap.det ↑(toLin' A) =
    LinearMap.det ((↑(toLin' A)).restrict hcomap) * LinearMap.det (L.mapQ L (↑(toLin' A)) hcomap)
⊢ A • v = v

Tactic:
rw [show LinearMap.det A.toLin'.toLinearMap = 1 by simp [toLin'_to_linearMap],
      hres, hQ, LinearMap.det_smul, finrank_span_singleton hv, pow_one,
      LinearMap.det_id, LinearMap.det_id, mul_one, mul_one] at hdet

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
L : Submodule F (ι → F) := F ∙ v
hA : A ∈ lineStab L
c : F
hcv : ↑(toLin' A) v = c • v
hcomap : F ∙ v ≤ Submodule.comap (↑(toLin' A)) (F ∙ v)
hres : (↑(toLin' A)).restrict hcomap = c • LinearMap.id
hQ : L.mapQ L (↑(toLin' A)) hcomap = LinearMap.id
hdet : 1 = c
⊢ A • v = v
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Goal state after:
case inl
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Subsingleton R
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id

case inr
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
⊢ g ∈ Subgroup.center (SpecialLinearGroup R V) ↔ ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑g = r • LinearMap.id
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
v : ι → K
⊢ ¬LinearIndependent K ![v, f v]

Tactic:
by_cases hv : v = 0

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
v : ι → K
hv : v = 0
⊢ ¬LinearIndependent K ![v, f v]

case neg
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
hm : ∀ (x : ℙ K (ι → K)), m • x = x
f : (ι → K) →ₗ[K] ι → K := ↑(Matrix.SpecialLinearGroup.toLin' m)
hf : f = ↑(Matrix.SpecialLinearGroup.toLin' m)
v : ι → K
hv : ¬v = 0
⊢ ¬LinearIndependent K ![v, f v]
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∀ (x y : M ⧸ N),
    Quotient.lift ⇑Q ⋯ (x + y) =
      Quotient.lift ⇑Q ⋯ x + Quotient.lift ⇑Q ⋯ y + ((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯) x) y

pp: case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker

Tactic:
· simp only [Submodule.Quotient.forall]
    exact QuadraticMap.map_add Q

Goal state after:
case w
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
n : M
hn : n ∈ N
⊢ n ∈ (LinearMap.flip Q.polarBilin).ker
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ {i | 0 < w i}.ncard + {i | w i < 0}.ncard + {i | w i = 0}.ncard = Nat.card ι

Tactic:
calc {i | 0 < w i}.ncard + {i | w i < 0}.ncard + {i | w i = 0}.ncard
  _ = {i | 0 < w i}.ncard + {i | w i ≤ 0}.ncard := by
    rw [add_assoc, add_left_cancel_iff, ← Set.ncard_union_eq]
    · congr! 1
      ext
      grind
    · grind [disjoint_iff_ne]
  _ = Set.univ.ncard := by
    rw [← Set.ncard_union_eq]
    · congr! 1
      ext
      grind [le_iff_lt_or_eq]
    · grind [disjoint_iff_ne]
  _ = Nat.card ι := Set.ncard_univ _

Goal state after:
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 ι
⊢ cartanSubalgebra b ≤ lieAlgebra b

Tactic:
cartanSubalgebra,

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 ι
⊢ { toSubmodule := span R (range h), lie_mem' := ⋯ } ≤ lieAlgebra b
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.IsCrystallographic
inst✝⁵ : P.IsReduced
inst✝⁴ : P.IsIrreducible
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsG2
i j : ι
h : P.root i ≠ P.root j
h' : P.root i ≠ -P.root j
⊢ P.pairingIn ℤ i j ∈ {-3, -1, 0, 1, 3}

Tactic:
by
  suffices ¬ (∀ i j, P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
                     P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨
                     P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j) by
    have aux₁ := P.forall_pairingIn_eq_swap_or.resolve_left this i j
    have aux₂ := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i j h h'
    simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero,
      Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at aux₂ ⊢
    lia
  obtain ⟨k, l, hkl⟩ := exists_pairingIn_neg_three (P := P)
  push Not
  refine ⟨k, l, ?_⟩
  have aux := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed k l
  simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero,
      Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at aux
  omega

Goal state after:
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
this : Module.IsReflexive R M
aux₁ : LinearIndependent R ![P.root i, P.root j]
aux₂ : chainBotCoeff i j + chainTopCoeff i j ≤ 2
aux₃ : 1 ≤ chainTopCoeff i j
⊢ chainBotCoeff i j = if P.pairingIn ℤ i j = 0 then 1 else 0

Tactic:
rcases eq_or_ne (P.chainBotCoeff i j) (P.chainTopCoeff i j) with aux₄ | aux₄ <;>
  simp_rw [P.pairingIn_eq_zero_iff (i := i) (j := j), ← P.chainBotCoeff_sub_chainTopCoeff aux₁,
    sub_eq_zero, Nat.cast_inj, aux₄, reduceIte] <;>
  lia

Goal state after:
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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
hw₀ : genWeightSpace (↥b.support ⊕ ι → K) χ ≠ ⊥
χ' : ↥H →ₗ[K] K := Weight.toLinear K (↥H) (↥b.support ⊕ ι → K) { toFun := χ, genWeightSpace_ne_bot' := hw₀ }
⊢ ∃ l, χ (h' l) ≠ 0

Tactic:
replace hχ : χ' ≠ 0 := by contrapose hχ; ext x; simpa using! LinearMap.congr_fun hχ x

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
χ : ↥H → K
w : ↥b.support ⊕ ι → K
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
hw₀ : genWeightSpace (↥b.support ⊕ ι → K) χ ≠ ⊥
χ' : ↥H →ₗ[K] K := Weight.toLinear K (↥H) (↥b.support ⊕ ι → K) { toFun := χ, genWeightSpace_ne_bot' := hw₀ }
hχ : χ' ≠ 0
⊢ ∃ l, χ (h' l) ≠ 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
⊢ ∃ d, (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ∧ diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b

Tactic:
cartanSubalgebra,

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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
⊢ ∃ d,
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d) ∧ diagonal (0 ⊕ᵥ d) ∈ { toSubmodule := span K (range h), lie_mem' := ⋯ }
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
inst✝ : P.IsIrreducible
i : ι
⊢ i ∈
    {long P, -long P, short P, -short P, shortAddLong P, -shortAddLong P, twoShortAddLong P, -twoShortAddLong P,
      threeShortAddLong P, -threeShortAddLong P, threeShortAddTwoLong P, -threeShortAddTwoLong P}

Tactic:
simpa using mem_allRoots P i

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

Goal state before:
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
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
m : ι
hm : P.root m = P.root ↑i + P.root ↑j
aux₁ : ↑(chainTopCoeff ↑j ↑i) = -P.pairingIn ℤ ↑i ↑j
⊢ ((if ↑i = ↑i then ↑((if i = j then 4 else 0) - P.pairingIn ℤ ↑i ↑j) else 0) -
      if P.root m = P.root ↑i + P.root ↑j ∧ P.root ↑i = P.root m - P.root ↑j then ↑(chainTopCoeff (↑j) m) + 1 else 0) =
    0

Tactic:
have aux₂ := chainTopCoeff_of_add (b.linearIndependent_pair_of_ne hij.symm) hm

Goal state after:
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
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
m : ι
hm : P.root m = P.root ↑i + P.root ↑j
aux₁ : ↑(chainTopCoeff ↑j ↑i) = -P.pairingIn ℤ ↑i ↑j
aux₂ : chainTopCoeff ↑j ↑i = chainTopCoeff (↑j) m + 1
⊢ ((if ↑i = ↑i then ↑((if i = j then 4 else 0) - P.pairingIn ℤ ↑i ↑j) else 0) -
      if P.root m = P.root ↑i + P.root ↑j ∧ P.root ↑i = P.root m - P.root ↑j then ↑(chainTopCoeff (↑j) m) + 1 else 0) =
    0
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 ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j : ι
⊢ j ∈ b.support → ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b j ∈ U → ∃ j, u j ∈ U

Tactic:
hj

Goal state after:
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 ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j : ι
hj : j ∈ b.support
⊢ ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, v b j ∈ U → ∃ j, u j ∈ U
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : Free R M
κ : Type uM
b : Basis κ R M
this✝ : Nonempty κ
this : Nontrivial R
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)

Tactic:
(equivMvPolynomial b).toLinearEquiv.rank_eq,

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : Free R M
κ : Type uM
b : Basis κ R M
this✝ : Nonempty κ
this : Nontrivial R
⊢ Module.rank R (MvPolynomial κ R) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)
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
A : Type u_3
inst✝³ : CommSemiring A
inst✝² : Algebra R A
f : M →ₗ[R] A
A' : Type u_4
inst✝¹ : CommSemiring A'
inst✝ : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG : ↑F ∘ₗ f = ↑G ∘ₗ f
x : M
⊢ (↑(F.comp ↑h.equiv) ∘ₗ SymmetricAlgebra.ι R M) x = (↑(G.comp ↑h.equiv) ∘ₗ SymmetricAlgebra.ι R M) x

Tactic:
simpa using congr($hFG x)

Goal state after:
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
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ (Measure.map (Finset.restrict₂ hJI) (P I)) univ = (P J) univ

Tactic:
hP I J hJI

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
hJI : J ⊆ I
this : univ = Finset.restrict₂ hJI ⁻¹' univ
⊢ (Measure.map (Finset.restrict₂ hJI) (P I)) univ = (Measure.map (Finset.restrict₂ hJI) (P I)) univ
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ eval i ⁻¹' t i = cylinder {i} {f | f ⟨i, ⋯⟩ ∈ t i}

Tactic:
ext1 x

Goal state after:
case a
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
i : ι
t : (i : ι) → Set (α i)
ht : ∀ (i : ι), MeasurableSet (t i)
x : (x : ι) → α x
⊢ x ∈ eval i ⁻¹' t i ↔ x ∈ cylinder {i} {f | f ⟨i, ⋯⟩ ∈ t i}
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
⊢ j ∈ Δ → Measurable fun a ↦ update a.1 i a.2 j

Tactic:
hj

Goal state after:
ι : Type u_2
X : ι → Type u_3
m : (i : ι) → MeasurableSpace (X i)
Δ : Set ι
i : ι
inst✝ : DecidableEq ι
j : ι
hj : j ∈ Δ
⊢ Measurable fun a ↦ update a.1 i a.2 j