mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ := ⋯
hN' : abv (↑(f * g) i) < a1 * a2
hN1'✝ : a1 ≤ abv (↑f i)
hN1' : a2 ≤ abv (↑g i)
⊢ a1 * a2 ≤ abv (↑(f * g) i)

Tactic:
change _ ≤ 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 * ↑g i)
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε

Tactic:
obtain ⟨bi, hbi⟩ := hb ε ε0

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊔ b₁ - a₂ ⊔ b₂) j| < ε
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε

Tactic:
obtain ⟨bi, hbi⟩ := hb ε ε0

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a₁ b₁ a₂ b₂ : CauSeq α abs
ha : a₁ ≈ a₂
hb : b₁ ≈ b₂
ε : α
ε0 : ε > 0
ai : ℕ
hai : ∀ j ≥ ai, |↑(a₁ - a₂) j| < ε
bi : ℕ
hbi : ∀ j ≥ bi, |↑(b₁ - b₂) j| < ε
⊢ ∃ i, ∀ j ≥ i, |↑(a₁ ⊓ b₁ - a₂ ⊓ b₂) j| < ε
Module: Mathlib.Algebra.Order.CauSeq.Completion

Goal state before:
pp: α : Type u_1
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
β : Type u_2
inst✝² : Field β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f✝ : CauSeq β abv
hf✝ : ¬f✝.LimZero
hl : f✝.lim ≠ 0
g f : CauSeq β abv
hf : ¬f.LimZero
⊢ (g - f * f.inv hf * g).LimZero

Tactic:
have h₂ : g - f * inv f hf * g = 1 * g - f * inv f hf * g := by rw [one_mul g]
          have h₃ : f * inv f hf * g = (f * inv f hf) * g := by simp [mul_assoc]
          have h₄ : g - f * inv f hf * g = (1 - f * inv f hf) * g := by rw [h₂, h₃, ← sub_mul]
          have h₅ : g - f * inv f hf * g = g * (1 - f * inv f hf) := by rw [h₄, mul_comm]
          have h₆ : g - f * inv f hf * g = g * (1 - inv f hf * f) := by rw [h₅, mul_comm f]
          rw [h₆]; exact mul_limZero_right _ (Setoid.symm (CauSeq.inv_mul_cancel _))

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
⊢ A.vec = B.vec ↔ ∀ (i : m) (j : n), A i j = B i j

Tactic:
funext_iff,

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
⊢ (∀ (x : n × m), A.vec x = B.vec x) ↔ ∀ (i : m) (j : n), A i j = B i j
Module: Mathlib.LinearAlgebra.Matrix.Hermitian

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ A.IsHermitian

Tactic:
rw [← transpose_transpose A]

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ Aᵀᵀ.IsHermitian
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R' : Type u_4
inst✝² : CommRing R'
inst✝¹ : PartialOrder R'
inst✝ : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * Mᵀ i j * xj

Tactic:
Finsupp.sum_comm

Goal state after:
n : Type u_2
R' : Type u_4
inst✝² : CommRing R'
inst✝¹ : PartialOrder R'
inst✝ : StarRing R'
M : Matrix n n R'
hM : M.PosSemidef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ 0 ≤ x.sum fun x' v' ↦ x.sum fun x v ↦ star v * Mᵀ x x' * v'
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_2
R' : Type u_4
inst✝² : CommRing R'
inst✝¹ : PartialOrder R'
inst✝ : StarRing R'
M : Matrix n n R'
hM : M.PosDef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ x ≠ 0 → 0 < x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * Mᵀ i j * xj

Tactic:
Finsupp.sum_comm

Goal state after:
n : Type u_2
R' : Type u_4
inst✝² : CommRing R'
inst✝¹ : PartialOrder R'
inst✝ : StarRing R'
M : Matrix n n R'
hM : M.PosDef
this : ∀ (a b c : R'), a * b * c = c * b * a
x : n →₀ R'
⊢ x ≠ 0 → 0 < x.sum fun x' v' ↦ x.sum fun x v ↦ star v * Mᵀ x x' * v'
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: 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
⊢ M⁻¹.PosSemidef

Tactic:
by_cases h : IsUnit M.det

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
⊢ M⁻¹.PosSemidef

case neg
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
⊢ M⁻¹.PosSemidef
Module: Mathlib.LinearAlgebra.Matrix.PosDef

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Q.toMatrix'.PosDef
⊢ (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((QuadraticMap.associatedHom ℝ) Q)))).PosDef

Tactic:
exact hQ.toQuadraticForm'

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

Goal state before:
pp: case refine_1
ι : 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
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ genWeightSpace L ⇑(b.baseSupp i) ≠ ⊥

Tactic:
simp only [LieSubmodule.eq_bot_iff, ne_eq, not_forall]

Goal state after:
case refine_1
ι : 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
i : ι
this : H.IsCartanSubalgebra := isCartanSubalgebra b
⊢ ∃ x, ∃ (_ : x ∈ genWeightSpace L ⇑(b.baseSupp i)), ¬x = 0
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
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs : ⇑χ ∈ s
⊢ (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i

Tactic:
have hχ' : ¬ χ.IsZero := by simpa using hχ

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
this✝ : H.IsCartanSubalgebra := isCartanSubalgebra b
this : ∀ (n : ι → ℕ), ∑ i, n i • b.baseSupp i ∈ closure (⇑(rootSystem H).root '' range b.baseSupp')
s : Set (↥H → K) :=
  {0} ∪ {f | ∃ n, n ≠ 0 ∧ f = -⇑(∑ i, n i • b.baseSupp i)} ∪ {f | ∃ n, n ≠ 0 ∧ f = ⇑(∑ i, n i • b.baseSupp i)}
χ : Weight K (↥H) L
hχ : χ ∈ root
hs : ⇑χ ∈ s
hχ' : ¬χ.IsZero
⊢ (∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = -∑ i, n i • b.baseSupp i) ∨
    ∃ n, n ≠ 0 ∧ Weight.toLinear K (↥H) L χ = ∑ i, n i • b.baseSupp i
Module: Mathlib.LinearAlgebra.RootSystem.CartanMatrix

Goal state before:
pp: case h₀
ι : 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
inst✝¹⁰ : CharZero R
inst✝⁹ : IsDomain R
inst✝⁸ : Finite ι
ι₂ : Type u_6
M₂ : Type u_7
N₂ : Type u_8
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
P : RootPairing ι R M N
inst✝³ : P.IsRootSystem
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsReduced
b : P.Base
P₂ : RootPairing ι₂ R M₂ N₂
inst✝ : P₂.IsCrystallographic
b₂ : P₂.Base
e : ↥b.support ≃ ↥b₂.support
f : M ≃ₗ[R] M₂
hf : ∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)
he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j
this : ∀ (k : ↥b.support), P.reflection ↑k ≪≫ₗ f = f ≪≫ₗ P₂.reflection ↑(e k)
i : ι
⊢ ∀ (i : ι), f (P.root i) ∈ range ⇑P₂.root → f (P.root ((P.reflectionPerm i) i)) ∈ range ⇑P₂.root

Tactic:
exact fun j ⟨k, hk⟩ ↦ ⟨P₂.reflectionPerm k k, by simpa⟩

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

Goal state before:
pp: case succ.inl
R : Type u
inst✝ : Ring R
k n : ℕ
ih : k < n → eval (-↑k) (ascPochhammer R n) = 0
h : k < n + 1
hkn : k < n
⊢ eval (-↑k) (ascPochhammer R n) * (-↑k + ↑n) = 0

Tactic:
simp [ih hkn]

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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆ ∈
    ↑(lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂)))

Tactic:
apply lie_mem

Goal state after:
case hx
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodE eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))

case hy
ι₁ : 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₂
i : ι₁
hef : prodH eι b₁ b₂ i = ⁅prodE eι b₁ b₂ i, prodF eι b₁ b₂ i⁆
⊢ prodF eι b₁ b₂ i ∈ lieSpan R (↥(prod eι b₁ b₂)) (range (prodE eι b₁ b₂) ∪ range (prodF eι b₁ b₂))
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ nodal (↑G).toFinset Units.val = X ^ Fintype.card ↥G - 1

Tactic:
apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset

Goal state after:
case hvs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ Set.InjOn Units.val ↑(↑G).toFinset

case h_deg_le
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree ≤ ↑(#(↑G).toFinset)

case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree = (X ^ Fintype.card ↥G - 1).degree

case hlc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).leadingCoeff = (X ^ Fintype.card ↥G - 1).leadingCoeff

case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight w) d = n

Tactic:
← hn hd

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight w) d = (weight w) d
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
⊢ IsWeightedHomogeneous w (φ ^ (n + 1)) ((n + 1) • m)

Tactic:
rw [pow_succ, succ_nsmul]

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ : MvPolynomial σ R
m : M
w : σ → M
hφ : IsWeightedHomogeneous w φ m
n : ℕ
ih : IsWeightedHomogeneous w (φ ^ n) (n • m)
⊢ IsWeightedHomogeneous w (φ ^ n * φ) (n • m + m)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d = n

Tactic:
← hn hd

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d = (weight 1) d
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (monomial d) (coeff d φ) = 0

Tactic:
exfalso

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (monomial d) (coeff d φ) = 0

Tactic:
exfalso

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ False
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
r : R
⊢ (C r * φ).IsHomogeneous m

Tactic:
by
  simpa only [zero_add] using (isHomogeneous_C _ _).mul hφ

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
m : M
⊢ ↑((decompose' R w φ) m) = ↑0 ↔ (weightedHomogeneousComponent w m) φ = 0

Tactic:
rw [decompose'_apply, Submodule.coe_zero]

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

Goal state before:
pp: R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsDomain R
N : ℕ
IH : ∀ {F : MvPolynomial (Fin N) R} {n : ℕ}, F.IsHomogeneous n → F ≠ 0 → ↑n ≤ #R → ∃ r, (eval r) F ≠ 0
F : MvPolynomial (Fin (N + 1)) R
n : ℕ
hF : F.IsHomogeneous n
hF₀ : F ≠ 0
hnR : ↑n ≤ #R
hdeg : ((finSuccEquiv R N) F).natDegree < n + 1
⊢ ∃ i, ((finSuccEquiv R N) F).coeff i ≠ 0

Tactic:
by
      contrapose! hF₀
      exact (finSuccEquiv _ _).injective <| Polynomial.ext <| by simpa using! hF₀

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

Goal state before:
pp: case h
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
⊢ φ ↑x = 0

Tactic:
Subtype.ext_iff

Goal state after:
case h
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
⊢ φ ↑x = 0
Module: Mathlib.LinearAlgebra.Dimension.LinearMap

Goal state before:
pp: K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set V
hsc : lift.{v', v} #↑s = lift.{v, v'} c
si : LinearIndepOn K (⇑f) s
this : LinearIndepOn K (⇑f.rangeRestrict) s
⊢ lift.{?u.137, v'} c = lift.{?u.137, v'} #↑(⇑f.rangeRestrict '' s)

Tactic:
← hsc,

Goal state after:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
c : Cardinal.{v'}
f : V →ₗ[K] V'
g : ↥f.range →ₗ[K] V
hg : f.rangeRestrict ∘ₗ g = id
fg : LeftInverse ⇑f.rangeRestrict ⇑g
s : Set V
hsc : lift.{v', v} #↑s = lift.{v, v'} c
si : LinearIndepOn K (⇑f) s
this : LinearIndepOn K (⇑f.rangeRestrict) s
⊢ lift.{v', v} #↑s = lift.{v, v'} #↑(⇑f.rangeRestrict '' s)
Module: Mathlib.Algebra.Lie.CartanExists

Goal state before:
pp: R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))
⊢ Polynomial.map (↑(MvPolynomial.aeval ⇑(b.repr (r • y + x)))) ((↑φ).polyCharpoly b) = charpoly (φ (r • y) + φ x)

Tactic:
MvPolynomial.coe_aeval_eq_eval,

Goal state after:
R : Type u_2
L : Type u_3
M : Type u_4
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
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Module.Finite R M
inst✝ : Free R M
x y : L
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = ⇑(b.repr (r • y + x))
⊢ Polynomial.map (MvPolynomial.eval ⇑(b.repr (r • y + x))) ((↑φ).polyCharpoly b) = charpoly (φ (r • y) + φ x)
Module: Mathlib.Algebra.Lie.Classical

Goal state before:
pp: case pos
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
simp [Pso, h, hi, one_apply]

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

Goal state before:
pp: case neg
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
x y : q
h : ¬x = y
⊢ (Pso p q R i * Pso p q R (-i)) (Sum.inr x) (Sum.inr y) = 1 (Sum.inr x) (Sum.inr y)

Tactic:
simp [Pso, h, hi, one_apply]

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

Goal state before:
pp: n : Type un
n₀ : Type un₀
R : Type uR
inst✝ : Semiring R
m m₀ : Type um
A : Matrix m n R
r : m₀ → m
c : n₀ → n
⊢ (A.submatrix r c).cRank ≤ A.cRank

Tactic:
simpa using lift_cRank_submatrix_le A r c

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

Goal state before:
pp: m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
h : LinearIndependent R (col 1)
⊢ #↑(range (col 1)) = lift.{max um uR, um} #m

Tactic:
← Cardinal.mk_range_eq_of_injective h.injective,

Goal state after:
m : Type um
R : Type uR
inst✝³ : Semiring R
inst✝² : Nontrivial R
inst✝¹ : DecidableEq m
inst✝ : StrongRankCondition R
h : LinearIndependent R (col 1)
⊢ #↑(range (col 1)) = lift.{um, max uR um} #↑(range (col 1))