mathlib-initiative/mathlib-tactics huggingface dataset:
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
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : ↑s.card + 1 < ENat.card K
hj' : ↑(p j) ∪ ⋃ i ∈ s, ↑(p i) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 | ∃ t, ∃ (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, ↑(p i)
k : ι
hk : k ∈ s
t₁ t₂ : K
ht : t₁ ≠ t₂
ht₁ : x + t₁ • y ∈ p k
ht₂ : x + t₂ • y ∈ p k
this : (t₁ - t₂) • y ∈ p k
⊢ t₁ - t₂ ≠ 0

Tactic:
rwa [sub_ne_zero]

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg.a
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
e : (chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
⊢ genWeightSpace L (↑(chainLength α β - chainTopCoeff (⇑α) β).succ • ⇑(-α) + ⇑β) = ⊥

Tactic:
Nat.cast_succ,

Goal state after:
case neg.a
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
e : (chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
⊢ genWeightSpace L ((↑(chainLength α β - chainTopCoeff (⇑α) β) + 1) • ⇑(-α) + ⇑β) = ⊥
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: case neg.a
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
e : (chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
⊢ genWeightSpace L ((-1 + -↑(chainLength α β) + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) = ⊥

Tactic:
← neg_add_rev,

Goal state after:
case neg.a
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
e : (chainLength α β - chainTopCoeff (⇑α) β).succ ≤ chainTopCoeff (⇑(-α)) β
⊢ genWeightSpace L ((-(↑(chainLength α β) + 1) + ↑(chainTopCoeff (⇑α) β)) • ⇑α + ⇑β) = ⊥
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case indexEquiv
ι : 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
f g : P.End
hfg : (weightHom P) f = (weightHom P) g
x : ι
⊢ f.indexEquiv x = g.indexEquiv x

Tactic:
refine Embedding.injective P.root ?_

Goal state after:
case indexEquiv
ι : 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
f g : P.End
hfg : (weightHom P) f = (weightHom P) g
x : ι
⊢ P.root (f.indexEquiv x) = P.root (g.indexEquiv x)
Module: Mathlib.Algebra.Lie.Weights.RootSystem

Goal state before:
pp: 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
x✝ : ↥LieSubalgebra.root
α : Weight K (↥H) L
hα : α ∈ LieSubalgebra.root
⊢ (LinearMap.id ({ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } ⟨α, hα⟩))
      ({ toFun := coroot ∘ Subtype.val, inj' := ⋯ } ⟨α, hα⟩) =
    2

Tactic:
by simpa using root_apply_coroot <| by simpa using hα

Goal state after:
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: k : Type u_1
inst✝² : Semiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x y : G
x✝ a✝ : H
⊢ (((↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x_1 ↦ (x * y) • x_1) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ
            lsingle x✝)
          1).coeff
      a✝ =
    (((↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x_1 ↦ x • x_1) ∘ₗ ↑(coeffLinearEquiv k) *
              ↑(coeffLinearEquiv k).symm ∘ₗ (Finsupp.lmapDomain k k fun x ↦ y • x) ∘ₗ ↑(coeffLinearEquiv k)) ∘ₗ
            lsingle x✝)
          1).coeff
      a✝

Tactic:
simp [mul_smul]

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

Goal state before:
pp: case refine_1
ι : 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✝ : Nontrivial M
h : IsSimpleOrder ↥P.weylGroupRootRep.invtSubmodule
q : Submodule R M
hq₁ : ∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)
hq₂ : q ≠ ⊥
⊢ q = ⊤

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
inst✝ : Nontrivial M
h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
⊢ q = ⊥ ∨ q = ⊤

Tactic:
· suffices ∀ g : P.weylGroup, q ∈ invtSubmodule (P.weylGroupRootRep g) by
      let q' : P.weylGroupRootRep.invtSubmodule :=
        ⟨q, (Representation.mem_invtSubmodule P.weylGroupRootRep).mpr this⟩
      suffices q' = ⊤ by simpa [q']
      apply (IsSimpleOrder.eq_bot_or_eq_top _).resolve_left
      simpa [q']
    rintro ⟨g, hg⟩
    induction hg using weylGroup.induction with
    | mem i => exact hq₁ i
    | one => simp [← Submonoid.one_def]
    | mul x y hx hy hx' hy' => apply invtSubmodule.comp <;> assumption

Goal state after:
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
inst✝ : Nontrivial M
h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
⊢ q = ⊥ ∨ q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Irreducible

Goal state before:
pp: case refine_2.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
inst✝ : Nontrivial M
h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
hq : q ≠ ⊥
⊢ q = ⊥ ∨ q = ⊤

Tactic:
suffices (q : Submodule R M) = ⊤ by right; simpa using this

Goal state after:
case refine_2.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
inst✝ : Nontrivial M
h : ∀ (q : Submodule R M), (∀ (i : ι), q ∈ invtSubmodule ↑(P.reflection i)) → q ≠ ⊥ → q = ⊤
q : ↥P.weylGroupRootRep.invtSubmodule
hq : q ≠ ⊥
⊢ ↑q = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.Hom

Goal state before:
pp: case hr
ι : 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₂
inst✝⁵ : IsDomain R
inst✝⁴ : CharZero R
inst✝³ : Module.IsTorsionFree R M₂
inst✝² : Finite ι₂
P : RootPairing ι R M N
inst✝¹ : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst✝ : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf : ∀ (i : ι), f (P.root i) = Q.root (e i)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
x✝ : ι₂
⊢ Q.root x✝ = (RootPairing.map e f g).root x✝

Tactic:
simp [hf, RootPairing.map, RootPairing.map]

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
i j : ↥b.support
hij : i ≠ j
this : {↑j, ↑i} ⊆ ↑b.support
⊢ LinearIndepOn R id (range ![P.root ↑i, P.root ↑j])

Tactic:
simpa [image_pair] using LinearIndepOn.id_image <| b.linearIndepOn_root.mono this

Goal state after:
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 : ι
h : LinearIndependent R ![P.root i, P.root j]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
n : ℕ
h'' : P.root j - n • P.root i ∈ range ⇑P.root
h' : 1 ∉ {k | P.root j - k • P.root i ∈ range ⇑P.root}
⊢ n = 0

Tactic:
rw [← Iic_chainBotCoeff_eq h, mem_Iic, not_le, Nat.lt_one_iff] at 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 : ι
h : LinearIndependent R ![P.root i, P.root j]
this : chainBotCoeff i j = 0 ↔ Iic (chainBotCoeff i j) = {0}
n : ℕ
h'' : P.root j - n • P.root i ∈ range ⇑P.root
h' : chainBotCoeff i j = 0
⊢ n = 0
Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg
ι : 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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
hij : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
⊢ (∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 2 * P.pairing j i ∨ P.pairing j i = 2 * P.pairing i j) ∨
    ∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 3 * P.pairing j i ∨ P.pairing j i = 3 * P.pairing i j

Tactic:
have key := B.apply_eq_or_of_apply_ne hij

Goal state after:
case neg
ι : 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
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
hij : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
key :
  ∀ (k : ι),
    (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
      (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)
⊢ (∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 2 * P.pairing j i ∨ P.pairing j i = 2 * P.pairing i j) ∨
    ∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 3 * P.pairing j i ∨ P.pairing j i = 3 * P.pairing i j
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 k : ι
z : ℤ
hk : P.root k = P.root i + z • P.root j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
⊢ P.root k = ∑ x ∈ b.support, (f x • P.root x + (z • g x) • P.root x)

Tactic:
smul_assoc,

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
i j k : ι
z : ℤ
hk : P.root k = P.root i + z • P.root j
f : ι → ℤ
hf : P.root i = ∑ j ∈ b.support, f j • P.root j
g : ι → ℤ
hg : P.root j = ∑ j ∈ b.support, g j • P.root j
⊢ P.root k = ∑ x ∈ b.support, (f x • P.root x + z • g x • P.root x)
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: ι : 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
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
huv : P.root i = u • P.root j + v • P.root k
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
⊢ i = j

Tactic:
replace huv : u • (Nat.cast ∘ a) + v • (Nat.cast (R := ℚ) ∘ b) = Pi.single ri 1 := by
    simp_rw [← ha, ← hb, Finset.smul_sum, ← Finset.sum_add_distrib, ← Nat.cast_smul_eq_nsmul ℚ,
      smul_smul, ← add_smul] at huv
    have aux : P.root i = ∑ x, Pi.single (M := fun x : P.root '' s ↦ ℚ) ri 1 x • (x : M) := by
      simp [ri]
    rw [eq_comm, aux] at huv
    have hli : LinearIndepOn ℚ id (P.root '' s) := by
      rw [← linearIndepOn_iff_image P.root.injective.injOn]
      exact (linearIndepOn_root_baseOf P f hf).restrict_scalars' ℚ
    rw [← linearIndependent_subtype_iff] at hli
    exact linearIndependent_iff_injective_fintypeLinearCombination.mp hli huv

Goal state after:
ι : 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
f : M →+ ℚ
g : N →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
hfg : ∀ (i : ι), 0 < f (P.root i) ↔ 0 < g (P.coroot i)
_i✝ : Fintype ι
_i : Module ℚ M := compHom M (algebraMap ℚ R)
s : Set ι := baseOf (⇑P.root) f
i : ι
hi : i ∈ baseOf (⇑P.root) f
j : ι
hj : j ∈ {i | 0 < g (P.coroot i)}
k : ι
hk : k ∈ {i | 0 < g (P.coroot i)}
contra : P.coroot i = P.coroot j + P.coroot k
u : ℚ
hu : u > 0
v : ℚ
hv : v > 0
hjk : ∀ {l : ι}, 0 < g (P.coroot l) → ∃ c, ∑ x, c x • ↑x = P.root l
a : ↑(⇑P.root '' s) → ℕ
ha : ∑ x, a x • ↑x = P.root j
b : ↑(⇑P.root '' s) → ℕ
hb : ∑ x, b x • ↑x = P.root k
ri : ↑(⇑P.root '' s) := ⟨P.root i, ⋯⟩
huv : u • Nat.cast ∘ a + v • Nat.cast ∘ b = Pi.single ri 1
⊢ i = j
Module: Mathlib.Data.Int.Star

Goal state before:
pp: n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
⊢ x ∈ closure (range fun x ↦ x ^ n)

Tactic:
have : x = x.natAbs • 1 ^ n := by simpa [eq_comm (a := x)] using hx

Goal state after:
n : ℕ
hn : Even n
x : ℤ
hx : x ∈ nonneg ℤ
this : x = x.natAbs • 1 ^ n
⊢ x ∈ closure (range fun x ↦ x ^ n)
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
f1 f2 g1 g2 : CauSeq β abv
hf : f1 ≈ f2
hg : g1 ≈ g2
⊢ f1 + g1 ≈ f2 + g2

Tactic:
by simpa only [← add_sub_add_comm] using! add_limZero hf hg

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

Goal state before:
pp: x : ℝ
⊢ { cauchy := ↑0 } = 0

Tactic:
by apply ext_cauchy; simp [cauchy_zero]

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

Goal state before:
pp: ⊢ mk 0 = 0

Tactic:
rw [← ofCauchy_zero]; rfl

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

Goal state before:
pp: ι : 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 : ι
⊢ P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑⋯.toFinset) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑⋯.toFinset)

Tactic:
simpa using hsp i

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

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ y✝¹ ≤ y✝¹ ⊔ y✝

Tactic:
exact CauSeq.le_sup_left

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

Goal state before:
pp: R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
d : n → R
μ : R
b : Basis n R M
inst✝ : IsDomain R
x : M
hx : x ∈ maxGenEigenspace ((toLin b b) (diagonal d)) μ
k : ℕ
hk : (((toLin b b) (diagonal d) - μ • 1) ^ k) x = 0
j : n
⊢ (toLin b b) (diagonal d) - μ • 1 = (toLin b b) (diagonal d - diagonal (μ • 1))

Tactic:
simp [one_eq_id]

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

Goal state before:
pp: n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit X.det
hy : IsUnit Y.det
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])

Tactic:
have hx' : IsUnit (X ^ n.succ).det := by
      rw [det_pow]
      exact hx.pow n.succ
    have hy' : IsUnit (Y ^ n.succ).det := by
      rw [det_pow]
      exact hy.pow n.succ
    rw [zpow_negSucc, zpow_negSucc, nonsing_inv_apply _ hx', nonsing_inv_apply _ hy', SemiconjBy]
    refine (isRegular_of_isLeftRegular_det hy'.isRegular.left).left ?_
    dsimp only
    rw [← mul_assoc, ← (h.pow_right n.succ).eq, mul_assoc, Matrix.mul_smul,
      mul_adjugate, ← Matrix.mul_assoc, Matrix.mul_smul (Y ^ _) (↑hy'.unit⁻¹ : R),
      mul_adjugate, smul_smul, smul_smul, hx'.val_inv_mul,
      hy'.val_inv_mul, one_smul, Matrix.mul_one, Matrix.one_mul]

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

Goal state before:
pp: n : Type u_2
inst✝⁴ : Fintype n
K : Type u_5
inst✝³ : Field K
inst✝² : PartialOrder K
inst✝¹ : StarRing K
inst✝ : DecidableEq n
M : Matrix n n K
hM : M.PosDef
h : ¬IsUnit M
⊢ ∃ a, a ≠ 0 ∧ M *ᵥ a = 0

Tactic:
obtain ⟨a, b, ha⟩ := Function.not_injective_iff.mp <| mulVec_injective_iff_isUnit.not.mpr h
    exact ⟨a - b, by simp [sub_eq_zero, ha, mulVec_sub]⟩

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
A : Matrix ι ι R
d : ι → R
hA : (diagonal d * A).PosDef
hD : ∀ (i : ι), 0 < d i
μ ρ : R
hμ : ∀ (i j : ι), A i j ≤ if i = j then μ else 0
hρ : HasEigenvalue (toLin' A) ρ
contra : 2 * μ ≤ ρ
N : Matrix ι ι R := μ • 1 - A
N_def : N = μ • 1 - A
hN : ∀ (i j : ι), 0 ≤ N i j
v : ι → R
hv : N *ᵥ v = (μ - ρ) • v
hv₀ : v ≠ 0
q : R := |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
q_def : q = |v| ⬝ᵥ (diagonal d * N) *ᵥ |v|
Q : R := μ * ∑ i, d i * |v i| ^ 2
Q_def : Q = μ * ∑ i, d i * |v i| ^ 2
hq₀ : q < Q
i : ι
x✝ : i ∈ Finset.univ
h₀ : 0 ≤ ρ - μ
h₁ : μ ≤ ρ - μ
h₂ : 0 ≤ d i
⊢ (ρ - μ) * |v i| ≤ (N *ᵥ |v|) i

Tactic:
calc (ρ - μ) * |v i|
          = |μ - ρ| * |v i| := by rw [← abs_eq_self.mpr h₀, abs_sub_comm]
        _ = |(N *ᵥ v) i| := by simp [hv]
        _ = |∑ j, N i j * v j| := by simp [mulVec_eq_sum, mul_comm]
        _ ≤ ∑ j, |N i j * v j| := Finset.abs_sum_le_sum_abs _ _
        _ = ∑ j, N i j * |v j| := by simp [abs_eq_self.mpr (hN i _)]
        _ = (N *ᵥ |v|) i := by simp [mulVec_eq_sum, mul_comm]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S n * (X + ↑n)) = eval k (ascPochhammer S n) * (k + ↑n)

Tactic:
mul_add,

Goal state after:
S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (ascPochhammer S n * X + ascPochhammer S n * ↑n) = eval k (ascPochhammer S n) * (k + ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n * (X + ↑n))

Tactic:
mul_add,

Goal state after:
case succ
S : Type u_1
inst✝² : Semiring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (ascPochhammer S n)
⊢ 0 < eval s (ascPochhammer S n * X + ascPochhammer S n * ↑n)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ (n + 1) = (ascPochhammer ℤ (n + 1)).comp (X - ↑(n + 1) + 1)

Tactic:
Nat.cast_succ,

Goal state after:
case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ (n + 1) = (ascPochhammer ℤ (n + 1)).comp (X - (↑n + 1) + 1)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval r (descPochhammer R (n + 1)) = eval (r - ↑(n + 1) + 1) (ascPochhammer R (n + 1))

Tactic:
Nat.cast_succ,

Goal state after:
case succ
R : Type u
inst✝ : Ring R
r : R
n : ℕ
ih : eval r (descPochhammer R n) = eval (r - ↑n + 1) (ascPochhammer R n)
⊢ eval r (descPochhammer R (n + 1)) = eval (r - (↑n + 1) + 1) (ascPochhammer R (n + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R k * (X + ↑k)) = (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))

Tactic:
mul_add,

Goal state after:
R : Type u
inst✝ : Ring R
r : R
k : ℕ
⊢ eval (-r) (ascPochhammer R k * X + ascPochhammer R k * ↑k) = (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ (↑n - ↑k) * 0 = ↑((n - k) * 0)

Tactic:
mul_zero,

Goal state after:
case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ 0 = ↑((n - k) * 0)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ 0 = ↑((n - k) * 0)

Tactic:
mul_zero,

Goal state after:
case pos
R : Type u
inst✝ : Ring R
n k : ℕ
ih : eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k)
h : n < k
⊢ 0 = ↑0
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(b ! * a.choose b) = eval (↑(a - (b - 1))) (ascPochhammer K b)

Tactic:
← descFactorial_eq_factorial_mul_choose,

Goal state after:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.descFactorial b) = eval (↑(a - (b - 1))) (ascPochhammer K b)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(b ! * a.choose b) = eval (↑a) (descPochhammer K b)

Tactic:
← descFactorial_eq_factorial_mul_choose,

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(a.descFactorial b) = eval (↑a) (descPochhammer K b)
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝ : Field F
x : F
⊢ degree 0 = ⊥

Tactic:
degree_zero

Goal state after:
F : Type u_1
inst✝ : Field F
x : F
⊢ ⊥ = ⊥