mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case inr.inl
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑↑n - ↑(chainTopCoeff (⇑α) β)
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
← Int.cast_natCast (chainTopCoeff α β),

Goal state after:
case inr.inl
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H✝ : LieSubalgebra K L
inst✝¹ : H✝.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H✝) L
α β : Weight K (↥H✝) L
hα : α.IsNonZero
k : K
h : ⇑β = k • ⇑α
h✝ : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = ↑↑n - ↑↑(chainTopCoeff (⇑α) β)
⊢ k = -1 ∨ k = 0 ∨ k = 1
Module: Mathlib.RepresentationTheory.Submodule

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
g : G
v : V
⊢ v ∈ (Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q) →
    v ∈ Submodule.comap (ρ g) ((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q))

Tactic:
hv

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
g : G
v : V
hv : v ∈ (Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q)
⊢ v ∈ Submodule.comap (ρ g) ((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm (Submodule.restrictScalars k q))
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
hSQ : span K (⇑P.root '' {i | P.root i ∈ Q}) ≤ Q
⊢ Q ≤ span K (⇑P.root '' {i | P.root i ∈ Q})

Tactic:
set S := span K (P.root '' {i | P.root i ∈ Q})

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
⊢ Q ≤ S
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
v : M
⊢ v ∈ Q → v ∈ S

Tactic:
hv

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
K : Type u_5
inst✝⁴ : Field K
inst✝³ : NeZero 2
inst✝² : Module K M
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsRootSystem
q : ↥P.invtRootSubmodule
Q : Submodule K M := ↑q
S : Submodule K M := span K (⇑P.root '' {i | P.root i ∈ Q})
hSQ : S ≤ Q
T : Submodule K M := span K (⇑P.root '' {i | P.root i ∉ Q})
h_sup : S ⊔ T = ⊤
v : M
hv : v ∈ Q
⊢ v ∈ S
Module: Mathlib.Data.Int.ConditionallyCompleteOrder

Goal state before:
pp: s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ sSup s ∈ s

Tactic:
convert! (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1

Goal state after:
s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ sSup s = ↑((Classical.choose h2).greatestOfBdd ⋯ h1)

s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ DecidablePred (Membership.mem s)
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ Bijective ⇑(↑f).weightMap

Tactic:
refine bijective_iff_has_inverse.mpr ?_

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ ∃ g, LeftInverse g ⇑(↑f).weightMap ∧ RightInverse g ⇑(↑f).weightMap
Module: Mathlib.LinearAlgebra.RootSystem.Hom

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ Bijective ⇑(↑f).coweightMap

Tactic:
refine bijective_iff_has_inverse.mpr ?_

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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P✝ : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ ∃ g, LeftInverse g ⇑(↑f).coweightMap ∧ RightInverse g ⇑(↑f).coweightMap
Module: Mathlib.LinearAlgebra.RootSystem.Base

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
b : P.Base
x✝ : ↥(P.rootSpan ℤ)
x : M
hx : x ∈ P.rootSpan ℤ
⊢ ⟨x, hx⟩ ∈ ↑(span ℤ (P.rootSpanMem ℤ '' ↑b.support))

Tactic:
← (injective_subtype (P.rootSpan ℤ)).mem_set_image,

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
b : P.Base
x✝ : ↥(P.rootSpan ℤ)
x : M
hx : x ∈ P.rootSpan ℤ
⊢ (P.rootSpan ℤ).subtype ⟨x, hx⟩ ∈ ⇑(P.rootSpan ℤ).subtype '' ↑(span ℤ (P.rootSpanMem ℤ '' ↑b.support))
Module: Mathlib.LinearAlgebra.RootSystem.Base

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
b : P.Base
x✝ : ↥(P.rootSpan ℤ)
x : M
hx : x ∈ P.rootSpan ℤ
⊢ (P.rootSpan ℤ).subtype ⟨x, hx⟩ ∈ ⇑(P.rootSpan ℤ).subtype '' ↑(span ℤ (P.rootSpanMem ℤ '' ↑b.support))

Tactic:
← Submodule.map_coe

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
b : P.Base
x✝ : ↥(P.rootSpan ℤ)
x : M
hx : x ∈ P.rootSpan ℤ
⊢ (P.rootSpan ℤ).subtype ⟨x, hx⟩ ∈ ↑(map (P.rootSpan ℤ).subtype (span ℤ (P.rootSpanMem ℤ '' ↑b.support)))
Module: Mathlib.LinearAlgebra.RootSystem.Chain

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✝⁷ : 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✝¹ : P.IsCrystallographic
i j : ι
inst✝ : P.IsReduced
h : LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 3

Tactic:
rw [← Int.ofNat_le, Nat.cast_add, Nat.cast_ofNat,
    chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h]

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✝⁷ : 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✝¹ : P.IsCrystallographic
i j : ι
inst✝ : P.IsReduced
h : LinearIndependent R ![P.root i, P.root j]
⊢ P.pairingIn ℤ (chainTopIdx i j) i ≤ 3
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case refine_3
ι : 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
b : P.Base
inst✝³ : CharZero R
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ : P.root l = P.root j + P.root k
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ ↑b.support
h₃ : P.root j = ∑ m, P.root (f m)
h₄ : ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ range ⇑P.root
h₅ : k ∈ b.support
m : Fin (n + 1)
⊢ ∑ m' ≤ m, P.root (Fin.snoc f k m') ∈ range ⇑P.root

Tactic:
· by_cases hm : m < n
    · have : m = (⟨m, hm⟩ : Fin n).castSucc := rfl
      rw [this, Fin.sum_Iic_castSucc]
      simp only [Fin.snoc_castSucc, h₄]
    · replace hm : m = n := by lia
      replace hm : Finset.Iic m = Finset.univ := by ext; simp [hm, Fin.le_def, Fin.is_le]
      simp [hm, Fin.sum_univ_castSucc, ← h₃, ← h₁]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f g : CauSeq α abs
F : α
F0 : F > 0
hF : ∃ i, ∀ j ≥ i, F ≤ ↑f j
H : g.LimZero
i : ℕ
h : ∀ j ≥ i, F ≤ ↑f j ∧ |↑g j| < F / 2
j : ℕ
ij : j ≥ i
⊢ F / 2 ≤ ↑(f + g) j

Tactic:
obtain ⟨h₁, h₂⟩ := h j ij
      have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1)
      rwa [← sub_eq_add_neg, sub_self_div_two] at this

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Field R
inst✝⁵ : CharZero R
inst✝⁴ : Module R M
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsRootSystem
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i✝ : ι
_i✝² : InvolutiveNeg ι := P.indexNeg
_i✝¹ : Fintype ι := Fintype.ofFinite ι
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, f (P.root i) = 1
hf : s = baseOf ⇑P.root ↑f
hf₀ : ∀ (i : ι), f (P.root i) ≠ 0
i : ι
⊢ ↑(2 / ((P.RootFormIn ℚ) (P.rootSpanMem ℚ i)) (P.rootSpanMem ℚ i)) = 2 / (P.RootForm (P.root i)) (P.root i)

Tactic:
simp [← P.algebraMap_rootFormIn ℚ (P.rootSpanMem ℚ i) (P.rootSpanMem ℚ i)]

Goal state after:
Module: Mathlib.Data.Real.Basic

Goal state before:
pp: x : ℝ
f : CauSeq ℚ abs
⊢ (∃ i, ∀ j ≥ i, x ≤ ↑(↑f j)) → x ≤ mk f

Tactic:
by
  intro h
  induction x using Real.ind_mk
  apply le_of_not_gt
  rw [mk_lt]
  rintro ⟨K, K0, hK⟩
  obtain ⟨i, H⟩ := exists_forall_ge_and h (exists_forall_ge_and hK (f.cauchy₃ <| half_pos K0))
  apply not_lt_of_ge (H _ le_rfl).1
  rw [← mk_const, mk_lt]
  refine ⟨_, half_pos K0, i, fun j ij => ?_⟩
  have := add_le_add (H _ ij).2.1 (le_of_lt (abs_lt.1 <| (H _ le_rfl).2.2 _ ij).1)
  rwa [← sub_eq_add_neg, sub_self_div_two, sub_apply, sub_add_sub_cancel] at this

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case refine_2
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ ∃ i ∈ x.support, 0 < x.sum fun j xj ↦ star (x i) * diagonal d i j * xj

Tactic:
refine ⟨i, ?_, Finsupp.sum_pos' ?_ ⟨i, ?_, ?_⟩⟩

Goal state after:
case refine_2.refine_1
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ i ∈ x.support

case refine_2.refine_2
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ ∀ i_1 ∈ x.support, 0 ≤ star (x i) * diagonal d i i_1 * x i_1

case refine_2.refine_3
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ i ∈ x.support

case refine_2.refine_4
n : Type u_2
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : n → R
h : ∀ (i : n), 0 < d i
x : n →₀ R
hx : x ≠ 0
i : n
hxi : ¬x i = 0
⊢ 0 < star (x i) * diagonal d i i * x i
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: case pos
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
this : (M⁻¹ᴴ * M * M⁻¹)ᴴ.PosSemidef
⊢ M⁻¹.PosSemidef

Tactic:
mul_nonsing_inv_cancel_right _ _ h,

Goal state after:
case pos
n : Type u_2
R' : Type u_4
inst✝⁴ : CommRing R'
inst✝³ : PartialOrder R'
inst✝² : StarRing R'
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R'
hM : M.PosSemidef
h : IsUnit M.det
this : M⁻¹ᴴᴴ.PosSemidef
⊢ M⁻¹.PosSemidef
Module: Mathlib.Algebra.Lie.Basis.Base

Goal state before:
pp: ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
e : ι ≃ ↑(range b.baseSupp') := Equiv.ofInjective b.baseSupp' ⋯
⊢ LinearIndepOn K (⇑(rootSystem H).root) (range b.baseSupp')

Tactic:
rw [LinearIndepOn, ← linearIndependent_equiv e]

Goal state after:
ι : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Fintype ι
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
b : Basis ι H
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : IsKilling K L
e : ι ≃ ↑(range b.baseSupp') := Equiv.ofInjective b.baseSupp' ⋯
⊢ LinearIndependent K ((fun x ↦ (rootSystem H).root ↑x) ∘ ⇑e)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝² : Ring R
n : ℕ
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
⊢ (descPochhammer R n).Monic

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn =>
    have h : leadingCoeff (X - 1 : R[X]) = 1 := leadingCoeff_X_sub_C 1
    have : natDegree (X - (1 : R[X])) ≠ 0 := ne_zero_of_eq_one <| natDegree_X_sub_C (1 : R)
    rw [descPochhammer_succ_left, Monic.def, leadingCoeff_mul, leadingCoeff_comp this, hn, monic_X,
        one_mul, one_mul, h, one_pow]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.inr.inl.inr
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
hne : n ≠ 0
⊢ (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)

Tactic:
det_eq_zero_of_column_eq_zero 0 (fun i ↦ by simpa [projVandermonde_apply, h0']),

Goal state after:
case succ.inr.inl.inr
K : Type u_2
inst✝ : Field K
n✝ n : ℕ
ih : ∀ (v w : Fin n → K), (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
v w : Fin (n + 1) → K
aux : ∀ (v w : Fin (n + 1) → K), w 0 ≠ 0 → (projVandermonde v w).det = ∏ i, ∏ j > i, (v j * w i - v i * w j)
h0 : ¬w 0 ≠ 0
h0' : ∀ (a : Fin (n + 1)), w a = 0
hne : n ≠ 0
⊢ 0 = ∏ i, ∏ j > i, (v j * w i - v i * w j)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ Lagrange.basis s v i ≠ 0

Tactic:
by
  simp_rw [Lagrange.basis, prod_ne_zero_iff, Ne, mem_erase]
  rintro j ⟨hij, hj⟩
  rw [basisDivisor_eq_zero_iff, hvs.eq_iff hi hj]
  exact hij.symm

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ (Lagrange.basis s v i).natDegree = ∑ x ∈ s.erase i, 1

Tactic:
convert! natDegree_prod _ _ H using 1

Goal state after:
case e'_3
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
H : ∀ j ∈ s.erase i, basisDivisor (v i) (v j) ≠ 0
⊢ ∑ x ∈ s.erase i, 1 = ∑ i_1 ∈ s.erase i, (basisDivisor (v i) (v i_1)).natDegree
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs✝ : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
⊢ #t = 1 + #t - 1

Tactic:
Nat.succ_add_sub_one,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs✝ : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ s
hs : 1 ≤ #s
hst' : #s ≤ #t
⊢ #t = 0 + #t
Module: Mathlib.Algebra.Lie.EngelSubalgebra

Goal state before:
pp: R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
⊢ ∀ (x_1 : ℕ), ((ad R L) x ^ x_1) y = 0 → ∀ (x_2 : ℕ), ((ad R L) x ^ x_2) z = 0 → ∃ k, ((ad R L) x ^ k) ⁅y, z⁆ = 0

Tactic:
m

Goal state after:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y z : L
m : ℕ
⊢ ((ad R L) x ^ m) y = 0 → ∀ (x_1 : ℕ), ((ad R L) x ^ x_1) z = 0 → ∃ k, ((ad R L) x ^ k) ⁅y, z⁆ = 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst✝¹³ : Semiring A
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst✝¹⁰ : DecidableEq ιA
inst✝⁹ : AddMonoid ιA
inst✝⁸ : SetLike σA A
inst✝⁷ : AddSubmonoidClass σA A
inst✝⁶ : GradedRing 𝒜
inst✝⁵ : DecidableEq ιM
inst✝⁴ : SetLike σM M
inst✝³ : AddSubmonoidClass σM M
inst✝² : Decomposition ℳ
inst✝¹ : VAdd ιA ιM
inst✝ : GradedSMul 𝒜 ℳ
x : HomogeneousSubmodule 𝒜 ℳ
r : A
⊢ ∀ {m : M}, m ∈ x → r • m ∈ x

Tactic:
m

Goal state after:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst✝¹³ : Semiring A
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst✝¹⁰ : DecidableEq ιA
inst✝⁹ : AddMonoid ιA
inst✝⁸ : SetLike σA A
inst✝⁷ : AddSubmonoidClass σA A
inst✝⁶ : GradedRing 𝒜
inst✝⁵ : DecidableEq ιM
inst✝⁴ : SetLike σM M
inst✝³ : AddSubmonoidClass σM M
inst✝² : Decomposition ℳ
inst✝¹ : VAdd ιA ιM
inst✝ : GradedSMul 𝒜 ℳ
x : HomogeneousSubmodule 𝒜 ℳ
r : A
m : M
⊢ m ∈ x → r • m ∈ x
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ insert a s, φ i).IsHomogeneous (∑ i ∈ insert a s, n i)

Tactic:
· intro i s his IH h
    simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
    apply (h i (by grind)).mul (IH _)
    grind

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (φ ^ n).IsHomogeneous (m * n)

Tactic:
rw [show φ ^ n = ∏ _i ∈ Finset.range n, φ by simp]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (m * n)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
⊢ Polynomial.eval 1 (Polynomial.map (eval 0) ((finSuccEquiv R N) F)) ≠ 0

Tactic:
eval_one_map,

Goal state after:
case h
R : Type u_3
inst✝ : CommSemiring R
N : ℕ
F : MvPolynomial (Fin N.succ) R
n : ℕ
hF : F.IsHomogeneous n
hFn : ((finSuccEquiv R N) F).coeff n ≠ 0
hF₀ : F ≠ 0
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
aux : ∀ i ∈ Finset.range n, constantCoeff (((finSuccEquiv R N) F).coeff i) = 0
⊢ (eval 0) (Polynomial.eval 1 ((finSuccEquiv R N) F)) ≠ 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
x : ↥W
hx : G x = 0
this : ↑x ∈ ⊥
⊢ ↑x = ↑0

Tactic:
Submodule.mem_bot

Goal state after:
K : Type u_2
M : Type u_3
inst✝³ : Field K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
inst✝ : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ n, ker (φ ^ n)
W : Submodule K M := ⨅ n, range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, φ x ∈ V
hφW : ∀ x ∈ W, φ x ∈ W
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ : ψ = e.symm.conj φ
x : ↥W
hx : G x = 0
this : ↑x = 0
⊢ ↑x = ↑0
Module: Mathlib.LinearAlgebra.SymplecticGroup

Goal state before:
pp: l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * J l R * aᵀ = J l R

Tactic:
exact ha

Goal state after: