mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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✝ : Fintype ι
i j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
⊢ (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i)

Tactic:
apply (rootForm_symmetric P).eq

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear

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✝ : Fintype ι
i j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ 4 • ((P.RootForm (P.root i)) (P.root j) * (P.RootForm (P.root i)) (P.root j)) =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))

Tactic:
nsmul_eq_mul,

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✝ : Fintype ι
i j : ι
hij : 4 • (P.RootForm (P.root i)) (P.root j) = 2 • (P.toLinearMap (P.root j)) (2 • P.Polarization (P.root i))
hji : 2 • (P.RootForm (P.root i)) (P.root j) = (P.toLinearMap (P.root i)) (2 • P.Polarization (P.root j))
⊢ ↑4 * ((P.RootForm (P.root i)) (P.root j) * (P.RootForm (P.root i)) (P.root j)) =
    P.coxeterWeight i j • ((P.RootForm (P.root i)) (P.root i) * (P.RootForm (P.root j)) (P.root j))
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg
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α : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : ↑(chainLength α β) = (chainTopCoeff (⇑α) β • ⇑α + ⇑β) (coroot α)
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))

Tactic:
nsmul_eq_mul,

Goal state after:
case neg
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α : ¬α.IsZero
x : L
hx : x ∈ genWeightSpace L ⇑(chainTop (⇑α) β)
x_ne0 : x ≠ 0
this : ↑(chainLength α β) = (↑(chainTopCoeff (⇑α) β) * ⇑α + ⇑β) (coroot α)
⊢ β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
Module: Mathlib.Algebra.Module.Submodule.Union

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
inst✝⁴ : Field K
inst✝³ : AddCommGroup M
inst✝² : Module K M
inst✝¹ : Finite ι
inst✝ : Infinite K
f : ι → Dual K M
p : ι → Submodule K M := fun i ↦ LinearMap.ker (f i)
h : ∀ (i : ι), p i ≠ ⊤
x : M
hx : ∀ (i : ι), x ∉ p i
⊢ ∃ x, ∀ (i : ι), (f i) x ≠ 0

Tactic:
exact ⟨x, by simpa [p] using hx⟩

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Prod

Goal state before:
pp: ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
⊢ ∑ i_1, (Q i_1) (Pi.single i m i_1) = (Q i) m

Tactic:
Fintype.sum_eq_single i fun j hj => ?_,

Goal state after:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
⊢ (Q i) (Pi.single i m i) = (Q i) m

ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
⊢ (Q j) (Pi.single i m j) = 0
Module: Mathlib.LinearAlgebra.RootSystem.WeylGroup

Goal state before:
pp: case refine_2
ι : 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
⊢ ((Equiv.weightHom P).domRestrict P.weylGroup).range ≤ Subgroup.closure (range P.reflection)

Tactic:
rintro fg ⟨⟨w, hw⟩, rfl⟩
    induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.weightHom P).domRestrict P.weylGroup) 1 ∈ _
      simp only [map_one, one_mem]
    | mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.domRestrict_apply, Equiv.weightHom_apply, Equiv.reflection_weightEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | inv_mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [Equiv.reflection_inv, MonoidHom.domRestrict_apply, Equiv.weightHom_apply,
        Equiv.reflection_weightEquiv]
      simpa only [reflection_mem_weylGroup] using! Subgroup.subset_closure (mem_range_self i)
    | mul w₁ w₂ hw₁ hw₂ h₁ h₂ =>
      simpa only [← Submonoid.mk_mul_mk _ w₁ w₂ hw₁ hw₂, map_mul] using! Subgroup.mul_mem _ h₁ h₂

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : Semiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : IsTrivial (MonoidHom.comp ρ S.subtype)
⊢ QuotientGroup.con S ≤ Con.ker ρ

Tactic:
by
    rintro x y ⟨⟨z, hz⟩, rfl⟩
    ext w
    change ρ (_ * z.unop) _ = _
    exact congr($(apply_eq_of_coe_eq ρ S _ _ (by simp_all)) w)

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case single.add
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
g : G
a : k
f✝ g✝ : α →₀ k[G]
a✝¹ : MonoidAlgebra.single g a • f✝ = ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) f✝
a✝ : MonoidAlgebra.single g a • g✝ = ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) g✝
⊢ MonoidAlgebra.single g a • (f✝ + g✝) = ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) (f✝ + g✝)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case single.single.add
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
α✝ : Type u_3
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
τ : Representation k G B
α : Type u_6
g : G
a : k
h : α
x✝ y✝ : k[G]
a✝¹ :
  MonoidAlgebra.single g a • Finsupp.single h x✝ =
    ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) (Finsupp.single h x✝)
a✝ :
  MonoidAlgebra.single g a • Finsupp.single h y✝ =
    ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) (Finsupp.single h y✝)
⊢ MonoidAlgebra.single g a • Finsupp.single h (x✝ + y✝) =
    ((free k G α).asAlgebraHom (MonoidAlgebra.single g a)) (Finsupp.single h (x✝ + y✝))

Tactic:
simp [*]

Goal state after:
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
i : ι
⊢ (↑(P.reflection i)).dualMap ∘ₗ ↑P.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ ↑(P.coreflection i)

Tactic:
ext f x; simpa [reflection_apply, coreflection_apply] using mul_comm ..

Goal state after:
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
inst✝ : CharZero R
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
this :
  ∀ (f : ι → ℤ),
    ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      Function.support f ⊆ ↑b.support → f ≠ 0 → 0 < f
k : ι
hk : P.root k = ∑ j ∈ b.support, f j • P.root j
hf' : f ≠ 0
hk' : -∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ ∑ j ∈ b.support, (-f) j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)

Tactic:
convert! hk'

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
inst✝ : CharZero R
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
this :
  ∀ (f : ι → ℤ),
    ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support) →
      Function.support f ⊆ ↑b.support → f ≠ 0 → 0 < f
k : ι
hk : P.root k = ∑ j ∈ b.support, f j • P.root j
hf' : f ≠ 0
hk' : -∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support)
⊢ ∑ j ∈ b.support, (-f) j • P.root j = -∑ j ∈ b.support, f j • P.root j
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

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✝¹ : P.IsCrystallographic
inst✝ : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : P.root i ≠ P.root j
hne' : P.root i ≠ -P.root j
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
⊢ B.rootLength j < B.rootLength i

Tactic:
by
  have hij' : P.pairingIn ℤ i j = -3 ∨ P.pairingIn ℤ i j = -2 ∨ P.pairingIn ℤ i j = 2 ∨
      P.pairingIn ℤ i j = 3 ∨ P.pairingIn ℤ i j = -4 ∨ P.pairingIn ℤ i j = 4 := by
    have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
    aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
  have aux₁ : P.pairingIn ℤ j i = -1 ∨ P.pairingIn ℤ j i = 1 := by
    have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
    have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
    aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster)
  have aux₂ := B.pairingIn_mul_eq_pairingIn_mul_swap i j
  have hi := B.rootLength_pos i
  rcases aux₁ with hji | hji <;> rcases hij' with hij' | hij' | hij' | hij' | hij' | hij' <;>
  rw [hji, hij'] at aux₂ <;> lia

Goal state after:
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
inst✝ : CharZero R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
⊢ P.root i - P.root j ∉ range ⇑P.root

Tactic:
by
  rcases eq_or_ne j i with rfl | hij
  · simpa only [sub_self, mem_range, not_exists] using fun k ↦ P.ne_zero k
  classical
  let f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
  have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j := by
    have : {i, j} ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
    rw [← Finset.sum_subset (s₁ := {i, j}) (s₂ := b.support) (by lia) (by aesop),
      Finset.sum_insert (by grind), Finset.sum_singleton]
    simp [f, hij, sub_eq_add_neg]
  intro contra
  rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg
  · simpa [hij, f] using le_of_lt pos j
  · simpa [hij, f] using le_of_lt neg i

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Finite ι
inst✝⁷ : CommRing R
inst✝⁶ : 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 : ι
h : ¬LinearIndependent R ![P.root i, P.root j]
⊢ P.root (chainTopIdx i j) = P.root j + chainTopCoeff i j • P.root i

Tactic:
simp only [chainTopIdx, chainTopCoeff, h, reduceDIte, zero_smul, add_zero]

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

Goal state before:
pp: case inl
ι : 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
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
pos : 0 < f
contra : ∀ (j : ι), f j = 0
⊢ False

Tactic:
exact P.ne_zero i <| by simp [hf₂, contra]

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

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✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
b : P.Base
inst✝ : CharZero R
i : ι
f : ι → ℤ
hf₀ : Function.support f ⊆ ↑b.support
hf₂ : P.root i = ∑ j ∈ b.support, f j • P.root j
neg : f < 0
contra : ∀ (j : ι), f j = 0
⊢ False

Tactic:
exact P.ne_zero i <| by simp [hf₂, contra]

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

Goal state before:
pp: ι : 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 : ι
aux : LinearIndependent R ![P.root i, P.root j] ↔ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
h : LinearIndependent R ![P.root i, P.root j]
h' : LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]
S₁ : Set ℤ := {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₁_def : S₁ = {z | P.root j + z • P.root i ∈ range ⇑P.root}
S₂ : Set ℤ := {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
S₂_def : S₂ = {z | P.root (chainTopIdx i j) + z • P.root i ∈ range ⇑P.root}
x✝ : ℤ
⊢ x✝ ∈ S₂ ↔ x✝ ∈ (fun z ↦ -↑(chainTopCoeff i j) + z) '' S₁

Tactic:
simp [S₁_def, S₂_def, root_chainTopIdx, add_smul, add_assoc, natCast_zsmul]

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

Goal state before:
pp: R₂ : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
inst✝² : IsDomain R₂
inst✝¹ : Free R₂ M₂
inst✝ : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
this✝ : Finite ι
this : Fintype ι
⊢ B.Nondegenerate

Tactic:
have : DecidableEq ι := Classical.decEq ι

Goal state after:
R₂ : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
inst✝² : IsDomain R₂
inst✝¹ : Free R₂ M₂
inst✝ : Module.Finite R₂ M₂
B : BilinForm R₂ M₂
hB : SeparatingLeft B
ι : Type u_4
b : Basis ι R₂ M₂
this✝¹ : Finite ι
this✝ : Fintype ι
this : DecidableEq ι
⊢ B.Nondegenerate
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
⊢ False

Tactic:
have hN' := hN i (le_max_left _ _)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
⊢ False
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑f i * ↑g i)

Tactic:
abv_mul abv

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hf : ¬f ≈ 0
hg : ¬g ≈ 0
this✝ : (f * g - 0).LimZero
hlz : (f * g).LimZero
hf' : ¬f.LimZero
hg' : ¬g.LimZero
a1 : α
ha1 : a1 > 0
N1 : ℕ
hN1 : ∀ j ≥ N1, a1 ≤ abv (↑f j)
a2 : α
ha2 : a2 > 0
N2 : ℕ
hN2 : ∀ j ≥ N2, a2 ≤ abv (↑g j)
this : 0 < a1 * a2
N : ℕ
hN : ∀ j ≥ N, abv (↑(f * g) j) < a1 * a2
i : ℕ := max N (max N1 N2)
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑f i) * abv (↑g i)
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
f : CauSeq α abs
h : f.LimZero
⊢ f.Pos ∨ f.LimZero ∨ (-f).Pos

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : CauSeq α abs
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
by
  obtain ha | ha := ha
  · obtain hb | hb := hb
    · exact Or.inl (CauSeq.sup_lt ha hb)
    · replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)
      refine le_of_le_of_eq (Or.inr ?_) hb
      exact CauSeq.sup_eq_right ha
  · replace hb := le_of_le_of_eq hb (Setoid.symm ha)
    refine le_of_le_of_eq (Or.inr ?_) ha
    exact CauSeq.sup_eq_left hb

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

Goal state before:
pp: l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst✝² : NonUnitalSemiring R
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l✝
⊢ ∑ x, ∑ x_1, B k x * A l x_1 * X x_1 x = ∑ x, ∑ x_1, A l x_1 * B k x * X x_1 x

Tactic:
(hB ..).eq

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

Goal state before:
pp: case hB.inl
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
x : R
i : n
⊢ Commute x (1 i i)

Tactic:
simp [*]

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

Goal state before:
pp: case hB.inr
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix l m R
B : Matrix m n R
x : R
i j : n
hij : i ≠ j
⊢ Commute x (1 i j)

Tactic:
simp [*]

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

Goal state before:
pp: case hA.inl
m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
A : Matrix m n R
B : Matrix n p R
x : R
i : m
⊢ Commute (1 i i) x

Tactic:
simp [*]

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

Goal state before:
pp: case hA.inr
m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst✝³ : Semiring R
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq m
A : Matrix m n R
B : Matrix n p R
x : R
i j : m
hij : i ≠ j
⊢ Commute (1 i j) x

Tactic:
simp [*]

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

Goal state before:
pp: case inl
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n →₀ R
i : n
x✝¹ x✝ : i ∈ x.support
⊢ 0 ≤ star (x i) * 1 i i * x i

Tactic:
simp [*]

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

Goal state before:
pp: case inr
n : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
x : n →₀ R
i : n
x✝¹ : i ∈ x.support
j : n
x✝ : j ∈ x.support
hij : i ≠ j
⊢ 0 ≤ star (x i) * 1 i j * x j

Tactic:
simp [*]

Goal state after:
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
χ : ↥root
this : H.IsCartanSubalgebra := isCartanSubalgebra b
n : ι → ℕ
⊢ ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')

Tactic:
← Submodule.span_nat_eq_addSubmonoidClosure,

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
χ : ↥root
this : H.IsCartanSubalgebra := isCartanSubalgebra b
n : ι → ℕ
⊢ ∑ i, n i • b.baseSupp i ∈ (Submodule.span ℕ (⇑(rootSystem H).root '' range b.baseSupp')).toAddSubmonoid
Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
f : End R M
μ : R
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
h : (minpoly R f).IsRoot μ
⊢ f.HasEigenvalue μ

Tactic:
obtain ⟨q, hq⟩ := dvd_iff_isRoot.mpr h
  obtain ⟨v, hv⟩ : ∃ v : M, q.aeval f v ≠ 0 := by
    by_contra! h_contra
    have := minpoly.min R f
      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
      (LinearMap.ext h_contra)
    rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this
    · norm_cast at this; grind
    · rintro rfl
      exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)
  refine Module.End.hasEigenvalue_of_hasEigenvector (hasEigenvector_iff.mpr ⟨?_, hv⟩)
  simpa [sub_eq_zero, hq] using congr($(minpoly.aeval R f) v)

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

Goal state before:
pp: case add
ι : 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✝⁵ : P.IsCrystallographic
inst✝⁴ : CharZero R
inst✝³ : IsDomain R
inst✝² : Finite ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
p : ↥b.support → Prop
i j : ↥b.support
hi : p i
hp : ∀ (i j : ↥b.support), p i → b.cartanMatrix j i ≠ 0 → p j
q : Submodule R M := span R (⇑P.root ∘ Subtype.val '' {i | p i})
hq₀ : q ≠ ⊥
hq_mem : ∀ (k : ↥b.support), P.root ↑k ∈ q ↔ p k
k : ↥b.support
x✝ x y : M
hx : x ∈ span R (⇑P.root ∘ Subtype.val '' {i | p i})
hy : y ∈ span R (⇑P.root ∘ Subtype.val '' {i | p i})
hx' : (P.coroot' ↑k) x ≠ 0 → p k
hy' : (P.coroot' ↑k) y ≠ 0 → p k
hk : (P.coroot' ↑k) (x + y) ≠ 0
⊢ p k

Tactic:
replace hk : P.coroot' k x ≠ 0 ∨ P.coroot' k y ≠ 0 := by by_contra! contra; simp_all
      tauto

Goal state after: