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

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
⊢ ((Equiv.coweightHom P).domRestrict P.weylGroup).range = Subgroup.closure (range (MulOpposite.op ∘ P.coreflection))

Tactic:
refine (Subgroup.closure_eq_of_le _ ?_ ?_).symm
  · rintro - ⟨i, rfl⟩
    simp only [MonoidHom.domRestrict_range, Subgroup.coe_map, mem_image,
      SetLike.mem_coe]
    use Equiv.reflection P i
    refine ⟨reflection_mem_weylGroup P i, by simp⟩
  · rintro fg ⟨⟨w, hw⟩, rfl⟩
    induction hw using Subgroup.closure_induction'' with
    | one =>
      change ((Equiv.coweightHom P).domRestrict P.weylGroup) 1 ∈ _
      simp only [map_one, one_mem]
    | mem w' hw' =>
      obtain ⟨i, rfl⟩ := hw'
      simp only [MonoidHom.domRestrict_apply, Equiv.coweightHom_apply,
        Equiv.reflection_coweightEquiv]
      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.coweightHom_apply,
        Equiv.reflection_coweightEquiv]
      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.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
⊢ Nontrivial ↥ρ.invtSubmodule ↔ Nontrivial V

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
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
h : Nontrivial ↥ρ.invtSubmodule
⊢ Nontrivial V

case refine_2
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
h : Nontrivial V
⊢ Nontrivial ↥ρ.invtSubmodule
Module: Mathlib.RepresentationTheory.Basic

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (x y : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom y) m =
          (RestrictScalars.addEquiv k k[G] M).symm (y • (RestrictScalars.addEquiv k k[G] M) m) →
        ((ofModule M).asAlgebraHom (x + y)) m =
          (RestrictScalars.addEquiv k k[G] M).symm ((x + y) • (RestrictScalars.addEquiv k k[G] M) m)

pp: case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (r : k) (x : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom (r • x)) m =
        (RestrictScalars.addEquiv k k[G] M).symm ((r • x) • (RestrictScalars.addEquiv k k[G] M) m)

Tactic:
· intro f g fw gw
    simp only [fw, gw, map_add, add_smul, LinearMap.add_apply]

Goal state after:
case smul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module k[G] M
r : k[G]
m : RestrictScalars k k[G] M
⊢ ∀ (r : k) (x : k[G]),
    ((ofModule M).asAlgebraHom x) m =
        (RestrictScalars.addEquiv k k[G] M).symm (x • (RestrictScalars.addEquiv k k[G] M) m) →
      ((ofModule M).asAlgebraHom (r • x)) m =
        (RestrictScalars.addEquiv k k[G] M).symm ((r • x) • (RestrictScalars.addEquiv k k[G] M) m)
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
α β : ↥LieSubalgebra.root
⊢ ↑(↑(chainBotCoeff ⇑↑β ↑α) - ↑(chainTopCoeff ⇑↑β ↑α)) =
    (LinearMap.id ({ toFun := fun x ↦ Weight.toLinear K (↥H) L ↑x, inj' := ⋯ } α))
      ({ toFun := coroot ∘ Subtype.val, inj' := ⋯ } β)

Tactic:
by simp [apply_coroot_eq_cast β.1 α.1]

Goal state after:
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
α β : ↥LieSubalgebra.root
⊢ (algebraMap ℤ K) (↑(chainBotCoeff ⇑↑β ↑α) - ↑(chainTopCoeff ⇑↑β ↑α)) = (rootSystem H).pairing α β

Tactic:
by simp [apply_coroot_eq_cast β.1 α.1]

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

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
i : ι
f : N
x : M
⊢ (((↑(P.reflection i)).dualMap ∘ₗ ↑P.flip.toPerfPair) f) x = ((↑P.flip.toPerfPair ∘ₗ ↑(P.coreflection i)) f) 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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_card : Nat.card ↑(baseOf (⇑P.root) f) = finrank R M
h_span : span R (range (⇑(P.rootSpan ℚ).subtype ∘ v)) = ⊤
⊢ Fintype.card ↑(baseOf (⇑P.root) f) = Set.finrank R (range (⇑(P.rootSpan ℚ).subtype ∘ v))

Tactic:
Set.finrank,

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
f : M →+ ℚ
hf : ∀ (i : ι), f (P.root i) ≠ 0
_i✝ : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
this✝ : InvolutiveNeg ι := P.indexNeg
this : Fintype ↑(baseOf (⇑P.root) f)
v : ↑(baseOf (⇑P.root) f) → ↥(P.rootSpan ℚ) := fun i ↦ P.rootSpanMem ℚ ↑i
h_card : Nat.card ↑(baseOf (⇑P.root) f) = finrank R M
h_span : span R (range (⇑(P.rootSpan ℚ).subtype ∘ v)) = ⊤
⊢ Fintype.card ↑(baseOf (⇑P.root) f) = finrank R ↥(span R (range (⇑(P.rootSpan ℚ).subtype ∘ v)))
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 : ι
⊢ ∃ f,
    Function.support f ⊆ ↑b.support ∧
      (P.root i = ∑ j ∈ b.support, f j • P.root j ∨ -P.root i = ∑ j ∈ b.support, f j • P.root j)

Tactic:
suffices ∀ m ∈ AddSubmonoid.closure (P.root '' b.support),
    ∃ f : ι → ℕ, f.support ⊆ b.support ∧ m = ∑ j ∈ b.support, f j • P.root j by
    rcases b.root_mem_or_neg_mem i with hi | hi
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inl hf'⟩
    · obtain ⟨f, hf, hf'⟩ := this _ hi
      exact ⟨f, hf, Or.inr hf'⟩

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
i : ι
⊢ ∀ m ∈ AddSubmonoid.closure (⇑P.root '' ↑b.support),
    ∃ f, Function.support f ⊆ ↑b.support ∧ m = ∑ j ∈ b.support, f j • P.root j
Module: Mathlib.LinearAlgebra.RootSystem.Base

Goal state before:
pp: case pred
ι : 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
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k
n : ℕ
ih : ∀ {i : ι}, b.IsPos i → b.height i = -↑n → p i
i : ι
h₀ : b.IsPos i
hN : b.height i = -↑n - 1
⊢ p i

Tactic:
| pred n ih =>

Goal state after:
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
h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - ↑g j) < ε
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, abv (f j - ↑g j) < ε / 2 / 2 ∧ ∀ k ≥ j, abv (↑g k - ↑g j) < ε / 2
j : ℕ
ij : j ≥ i
h₁ : abv (↑g i - f i) < ε / 2 / 2
h₂ : ∀ k ≥ i, abv (↑g k - ↑g i) < ε / 2
this✝ : abv (f j - ↑g j + (↑g i - f i)) < ε / 2 / 2 + ε / 2 / 2
this : abv (f j - ↑g j + (↑g i - f i) + (↑g j - ↑g i)) < ε / 2 / 2 + ε / 2 / 2 + ε / 2
⊢ abv (f j - f i) < ε

Tactic:
rwa [add_halves, add_halves, add_right_comm, sub_add_sub_cancel, sub_add_sub_cancel] at this

Goal state after:
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)
⊢ False

Tactic:
have hN1' := hN2 i (le_trans (le_max_right _ _) (le_max_right _ _))

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)
⊢ False
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : mk (f.inv hf) * mk g = mk (g.inv hg) * mk g
Ig : mk (g.inv hg) * mk g = 1
Ig' : mk g * mk (g.inv hg) = 1
⊢ mk (g.inv hg) * (mk g * mk (g.inv hg)) = mk (g.inv ⋯)

Tactic:
Ig',

Goal state after:
case neg
α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : Cauchy abv
f g : CauSeq β abv
fg : f ≈ g
this : f.LimZero ↔ g.LimZero
hf : ¬f.LimZero
hg : ¬g.LimZero
If : mk (f.inv hf) * mk g = mk (g.inv hg) * mk g
Ig : mk (g.inv hg) * mk g = 1
Ig' : mk g * mk (g.inv hg) = 1
⊢ mk (g.inv hg) * 1 = mk (g.inv ⋯)
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
R : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Star R
inst✝³ : Star α
inst✝² : MulAction R α
inst✝¹ : StarModule R α
A : Matrix n n α
k : R
inst✝ : Invertible k
h : (k • A).IsHermitian
hk : IsSelfAdjoint ⅟k
⊢ (⅟k • k • A).IsHermitian

Tactic:
exact h.smul hk

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

Goal state before:
pp: 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
⊢ (A * B).vec = (1 * A * B).vec

pp: case hA
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), Commute (1 i j) x

Tactic:
Matrix.one_mul

Goal state after:
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
⊢ (A * B).vec = (A * B).vec

case hA
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), Commute (1 i j) x
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
n : ℕ
⊢ 1 ^ -[n+1] = 1

Tactic:
rw [zpow_negSucc, one_pow, inv_one]

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

Goal state before:
pp: case inl
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : m ≤ 0
hn : n ≤ 0
h : A⁻¹ * A = 1
right✝ : A * A⁻¹ = 1
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
exact zpow_add (isUnit_det_of_left_inverse h) m n

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 : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ A = 1 * A

Tactic:
Matrix.one_mul

Goal state after:
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 : ℕ
hx' : IsUnit (X ^ n.succ).det
hy' : IsUnit (Y ^ n.succ).det
⊢ A = A
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 : M
ha : IsUnit A.det
z1 z2 : ℤ
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2

Tactic:
by
  rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
hA : Function.Injective fun v ↦ v ᵥ* A
⊢ (A * Aᴴ).PosDef

Tactic:
by
  classical
  simpa using mul_mul_conjTranspose_same .one hA

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

Goal state before:
pp: case refine_2
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ ∀ (p q : R[X]),
    ((aeval f) p) x = eval μ p • x → ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x

Tactic:
intro p

Goal state after:
case refine_2
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
p✝ : R[X]
h : f.HasEigenvector μ x
p : R[X]
⊢ ∀ (q : R[X]),
    ((aeval f) p) x = eval μ p • x → ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| ascPochhammer ℕ (n + 1) * (X + (↑n + 1))

Tactic:
← Nat.cast_succ

Goal state after:
S : Type u
inst✝ : Semiring S
n : ℕ
ih : ascPochhammer ℕ (n + 1) = ascPochhammer ℕ n * (X + ↑n)
| ascPochhammer ℕ (n + 1) * (X + ↑n.succ)
Module: Mathlib.RingTheory.Polynomial.Pochhammer

Goal state before:
pp: case inr
S : Type u_1
inst✝² : Ring S
inst✝¹ : PartialOrder S
inst✝ : IsStrictOrderedRing S
n : ℕ
s : S
h✝ : ↑n - 1 ≤ s
h : ↑n - 1 < s
⊢ 0 ≤ eval s (descPochhammer S n)

Tactic:
· exact (descPochhammer_pos h).le

Goal state after:
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝⁶ : Finite ι₁
inst✝⁵ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁴ : LieRing L₁
inst✝³ : LieRing L₂
R : Type u_5
inst✝² : CommRing R
inst✝¹ : LieAlgebra R L₁
H₁ : LieSubalgebra R L₁
b₁ : Basis ι₁ H₁
inst✝ : LieAlgebra R L₂
H₂ : LieSubalgebra R L₂
b₂ : Basis ι₂ H₂
⊢ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) = ⊤

Tactic:
by
  suffices lieSpan R (prod eι b₁ b₂) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) =
      lieSpan R (prod eι b₁ b₂)
        (range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)) by
    have hr : range (prodH eι b₁ b₂) ∪ range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂) =
        Subtype.val ⁻¹' ( {(b₁.h i, b₂.h (eι i)) | i : ι₁} ∪
                          {(b₁.e i, b₂.e (eι i)) | i : ι₁} ∪
                          {(b₁.f i, b₂.f (eι i)) | i : ι₁} ) := by
      ext; simp [Subtype.ext_iff]
    rw [this, hr]
    exact lieSpan_lieSpan_coe_preimage
  simp only [union_assoc]
  refine le_antisymm (lieSpan_mono <| by simp) (lieSpan_le.mpr <| union_subset ?_ subset_lieSpan)
  rintro - ⟨i, rfl⟩
  have hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆ := by
    simp [Subtype.ext_iff, (b₁.sl2 i).lie_e_f, (b₂.sl2 (eι i)).lie_e_f]
  rw [hef]
  apply lie_mem
  · exact subset_lieSpan <| mem_union_left _ <| mem_range_self i
  · exact subset_lieSpan <| mem_union_right _ <| mem_range_self i

Goal state after:
Module: Mathlib.Algebra.Lie.CartanCriterion

Goal state before:
pp: ι : Type u_4
R : Type u_5
K : Type u_6
inst✝³ : Finite ι
inst✝² : CommRing R
inst✝¹ : Field K
inst✝ : Algebra R K
E : Submodule R K
a : ι → K
ha : ∀ (i : ι), a i ∈ E
f : ↥E →+ R
⊢ ∃ r, ∀ (i j : ι), Polynomial.eval (a i - a j) r = (algebraMap R K) (f ⟨a i, ⋯⟩) - (algebraMap R K) (f ⟨a j, ⋯⟩)

Tactic:
suffices ∀ (ij kl : ι × ι) (hij : a ij.1 - a ij.2 = a kl.1 - a kl.2),
      algebraMap R K (f ⟨a ij.1, ha ij.1⟩) - algebraMap R K (f ⟨a ij.2, ha ij.2⟩) =
      algebraMap R K (f ⟨a kl.1, ha kl.1⟩) - algebraMap R K (f ⟨a kl.2, ha kl.2⟩) by
    obtain ⟨r, hr⟩ := (Polynomial.exists_eval_eq_iff _ _).mpr this
    exact ⟨r, fun i j ↦ hr (i, j)⟩
  rintro ⟨i, j⟩ ⟨k, l⟩ hij
  have heq : (⟨a i, ha i⟩ - ⟨a j, ha j⟩ : E) = ⟨a k, ha k⟩ - ⟨a l, ha l⟩ := Subtype.ext hij
  rw [← (algebraMap R K).map_sub, ← (algebraMap R K).map_sub, ← map_sub, ← map_sub, heq]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: case succ.e_a
R : Type u_1
inst✝ : CommRing R
n : ℕ
hn : (vandermonde fun i ↦ ↑↑i).det = ↑n.superFactorial
⊢ ∏ i, ∏ j > succAbove 0 i, (↑↑j - ↑↑(succAbove 0 i)) = ↑n.superFactorial

Tactic:
rw [det_vandermonde] at hn
      simp [hn]

Goal state after:
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: case refine_2
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 ∈ t
⊢ ∑ i_1 ∈ s, eval (v i) ((interpolate (insert i_1 (t \ s)) v) r * Lagrange.basis s v i_1) = r i

Tactic:
eval_mul

Goal state after:
case refine_2
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 ∈ t
⊢ ∑ x ∈ s, eval (v i) ((interpolate (insert x (t \ s)) v) r) * eval (v i) (Lagrange.basis s v x) = r i
Module: Mathlib.Algebra.Lie.Basis.Prod

Goal state before:
pp: ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹⁰ : Finite ι₁
inst✝⁹ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁸ : LieRing L₁
inst✝⁷ : LieRing L₂
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieAlgebra K L₁
inst✝³ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝² : LieAlgebra K L₂
inst✝¹ : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
f : ↥H₁ × ↥H₂ →ₗ[K] ↥(prodCartan eι b₁ b₂) := { toFun := fun x ↦ ⟨⟨(↑x.1, ↑x.2), ⋯⟩, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
f_inj : Injective ⇑f
g : ↥H₁ × ↥H₂ →ₗ[K] ↥H₁ := ↑(prodCartanEquiv eι b₁ b₂) ∘ₗ f
hg₁ : Injective ⇑g
⊢ False

Tactic:
obtain ⟨x₂ : H₂, hx₂ : x₂ ≠ 0⟩ := exists_ne (0 : H₂)

Goal state after:
ι₁ : Type u_1
ι₂ : Type u_2
L₁ : Type u_3
L₂ : Type u_4
inst✝¹⁰ : Finite ι₁
inst✝⁹ : Finite ι₂
eι : ι₁ ≃ ι₂
inst✝⁸ : LieRing L₁
inst✝⁷ : LieRing L₂
K : Type u_5
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : LieAlgebra K L₁
inst✝³ : FiniteDimensional K L₁
H₁ : LieSubalgebra K L₁
b₁ : Basis ι₁ H₁
inst✝² : LieAlgebra K L₂
inst✝¹ : FiniteDimensional K L₂
H₂ : LieSubalgebra K L₂
b₂ : Basis ι₂ H₂
hA : (Matrix.reindex eι eι) b₁.A = b₂.A
inst✝ : Nontrivial L₂
this✝⁴ : Fintype ι₁
this✝³ : Fintype ι₂
this✝² : H₁.IsCartanSubalgebra
this✝¹ : H₂.IsCartanSubalgebra
this✝ : (prodCartan eι b₁ b₂).IsCartanSubalgebra
contra : prod eι b₁ b₂ = ⊤
this : ∀ (x : ↥H₁ × ↥H₂) (hx : (↑x.1, ↑x.2) ∈ prod eι b₁ b₂), ⟨(↑x.1, ↑x.2), hx⟩ ∈ prodCartan eι b₁ b₂
f : ↥H₁ × ↥H₂ →ₗ[K] ↥(prodCartan eι b₁ b₂) := { toFun := fun x ↦ ⟨⟨(↑x.1, ↑x.2), ⋯⟩, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
f_inj : Injective ⇑f
g : ↥H₁ × ↥H₂ →ₗ[K] ↥H₁ := ↑(prodCartanEquiv eι b₁ b₂) ∘ₗ f
hg₁ : Injective ⇑g
x₂ : ↥H₂
hx₂ : x₂ ≠ 0
⊢ False