mathlib-initiative/mathlib-tactics huggingface dataset:
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
B : P.InvariantForm
inst✝¹ : P.IsIrreducible
inst✝ : Nonempty ι
i j : ι
hji_ne : (B.form (P.root j)) (P.root j) ≠ (B.form (P.root i)) (P.root i)
k : ι
hki_ne : (B.form (P.root k)) (P.root k) ≠ (B.form (P.root i)) (P.root i)
hkj_ne : (B.form (P.root k)) (P.root k) ≠ (B.form (P.root j)) (P.root j)
hij :
  (B.form (P.root i)) (P.root i) = 2 * (B.form (P.root j)) (P.root j) ∨
    (B.form (P.root i)) (P.root i) = 3 * (B.form (P.root j)) (P.root j) ∨
      (B.form (P.root j)) (P.root j) = 2 * (B.form (P.root i)) (P.root i) ∨
        (B.form (P.root j)) (P.root j) = 3 * (B.form (P.root i)) (P.root i)
hik :
  (B.form (P.root i)) (P.root i) = 2 * (B.form (P.root k)) (P.root k) ∨
    (B.form (P.root i)) (P.root i) = 3 * (B.form (P.root k)) (P.root k) ∨
      (B.form (P.root k)) (P.root k) = 2 * (B.form (P.root i)) (P.root i) ∨
        (B.form (P.root k)) (P.root k) = 3 * (B.form (P.root i)) (P.root i)
hjk :
  (B.form (P.root j)) (P.root j) = 2 * (B.form (P.root k)) (P.root k) ∨
    (B.form (P.root j)) (P.root j) = 3 * (B.form (P.root k)) (P.root k) ∨
      (B.form (P.root k)) (P.root k) = 2 * (B.form (P.root j)) (P.root j) ∨
        (B.form (P.root k)) (P.root k) = 3 * (B.form (P.root j)) (P.root j)
⊢ False

Tactic:
grind

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✝ : ι
h✝ : LinearIndependent R ![P.root i✝, P.root j✝]
i j : ι
h : LinearIndependent R ![P.root i, P.root j]
h₁ : (P.reflection i) (P.root (chainBotIdx i j)) = P.root j + (↑(chainBotCoeff i j) - P.pairingIn ℤ j i) • P.root i
h₂ :
  -↑(chainBotCoeff i j) ≤ ↑(chainBotCoeff i j) - P.pairingIn ℤ j i ∧
    ↑(chainBotCoeff i j) - P.pairingIn ℤ j i ≤ ↑(chainTopCoeff i j)
⊢ ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) ≤ P.pairingIn ℤ j i

Tactic:
grind

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 : ι
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}
hS₁₂ : S₂ = (fun z ↦ -↑(chainTopCoeff i j) + z) '' Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
hS₂ : S₂ = Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j))
⊢ chainBotCoeff i (chainTopIdx i j) = chainBotCoeff i j + chainTopCoeff i j ∧ chainTopCoeff i (chainTopIdx i j) = 0

Tactic:
hS₂,

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 : ι
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}
hS₁₂ :
  Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j)) =
    (fun z ↦ -↑(chainTopCoeff i j) + z) '' Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
hS₁ : S₁ = Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)
hS₂ : S₂ = Icc (-↑(chainBotCoeff i (chainTopIdx i j))) ↑(chainTopCoeff i (chainTopIdx i j))
⊢ chainBotCoeff i (chainTopIdx i j) = chainBotCoeff i j + chainTopCoeff i j ∧ chainTopCoeff i (chainTopIdx i j) = 0
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 : ι
h : LinearIndependent R ![P.root i, P.root j]
⊢ LinearIndependent R ![P.root i, P.root (chainTopIdx i j)]

Tactic:
rwa [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul,
      LinearIndependent.pair_add_smul_right_iff]

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 ι
this : DecidableEq ι
⊢ ((BilinForm.toMatrix b) B).SeparatingLeft

Tactic:
separatingLeft_toMatrix_iff

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 ι
⊢ SeparatingLeft B
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
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, ⋯⟩
x : ↑(⇑P.root '' s)
hx : x ≠ ri
huv : u * ↑(a x) + v * ↑(b x) = 0
this✝ : 0 ≤ u * ↑(a x)
this : 0 ≤ v * ↑(b x)
⊢ u * ↑(a x) = 0

Tactic:
grind

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
n✝ : ℕ
x✝ : CauSeq β abv
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝

Tactic:
rfl

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
n✝ : ℤ
x✝ : CauSeq β abv
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝

Tactic:
rfl

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
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝

Tactic:
rfl

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
n✝ : ℤ
⊢ ↑↑n✝ = ↑n✝

Tactic:
rfl

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

Goal state before:
pp: case succ.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
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
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
⊢ p i

Tactic:
obtain ⟨k, hk⟩ := P.root_sub_root_mem_of_pairingIn_pos hj' hij

Goal state after:
case succ.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
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
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk : P.root k = P.root i - P.root j
⊢ p i
Module: Mathlib.LinearAlgebra.RootSystem.BaseExists

Goal state before:
pp: case inr
ι : 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
q : ℚ
hq : q > 0
hq' : P.root j = q • P.root i
hij✝ : ¬LinearIndependent R ![P.root i, P.root j]
hij : P.root i = -P.root j
⊢ i = j

Tactic:
grind

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.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s) ∨ -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s)

Tactic:
let _i := P.indexNeg

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
s : Set ι
hli : LinearIndepOn R (⇑P.root) s
hsp : ∀ (i : ι), P.root i ∈ AddSubmonoid.closure (⇑P.root '' s) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' s)
i : ι
_i : InvolutiveNeg ι := P.indexNeg
⊢ P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s) ∨ -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' s)
Module: Mathlib.Algebra.Order.CauSeq.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
hx : x ≠ 0
⊢ ¬(const abv x).LimZero

Tactic:
by rwa [const_limZero]

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

Goal state before:
pp: a b : Cauchy abs
⊢ { cauchy := a } + -{ cauchy := b } = { cauchy := a } - { cauchy := b }

Tactic:
rfl

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

Goal state before:
pp: a b : Cauchy abs
⊢ ({ cauchy := a } - { cauchy := b }).cauchy = ({ cauchy := a } + -{ cauchy := b }).cauchy

Tactic:
rfl

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

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ (match { cauchy := ⟦f⟧ }, { cauchy := ⟦g⟧ } with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x1 x2 ↦ x1 < x2) definition._proof_1✝) ↔
    f < g

Tactic:
rfl

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

Goal state before:
pp: ⊢ mk 0 = { cauchy := 0 }

Tactic:
rfl

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

Goal state before:
pp: ⊢ mk 1 = { cauchy := 1 }

Tactic:
rfl

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

Goal state before:
pp: f g : CauSeq ℚ abs
⊢ f < g ∨ f ≈ g ↔ f ≤ g

Tactic:
rfl

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

Goal state before:
pp: case h.h
x : ℝ
y✝¹ y✝ : CauSeq ℚ abs
⊢ mk y✝¹ < mk y✝ ↔ mk y✝¹ ≤ mk y✝ ∧ ¬mk y✝ ≤ mk y✝¹

Tactic:
simpa using lt_iff_le_not_ge

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
⊢ 0 = const abv 0

Tactic:
rfl

Goal state after:
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 : β
h : ¬(const abv x).LimZero
⊢ const abv x⁻¹ = (const abv x).inv h

Tactic:
rfl

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

Goal state before:
pp: a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊔ b⟧ } =
    match { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x1 x2 ↦ x1 ⊔ x2) ⋯ x y }

Tactic:
rfl

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

Goal state before:
pp: a b : CauSeq ℚ abs
⊢ { cauchy := ⟦a ⊓ b⟧ } =
    match { cauchy := ⟦a⟧ }, { cauchy := ⟦b⟧ } with
    | { cauchy := x }, { cauchy := y } => { cauchy := Quotient.map₂ (fun x1 x2 ↦ x1 ⊓ x2) ⋯ x y }

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix m m (Matrix n n α)
⊢ (∀ (a : m) (b : n) (a_1 : m) (b_1 : n), star (A a_1 a b_1 b) = A a a_1 b b_1) ↔
    ∀ (i j : m) (i' j' : n), star (A j i j' i') = A i j i' j'

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝² : AddMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : DecidableEq n
d : n → α
⊢ (diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)

Tactic:
by
  simp [isSelfAdjoint_iff, IsHermitian, conjTranspose, diagonal_transpose, diagonal_map]

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
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ n = 0

Tactic:
zero_pow

Goal state after:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : ↑n ≠ 0
⊢ 0 = 0

n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
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
b : Basis n R M
⊢ ⨆ μ, eigenspace ((toLin b b) (diagonal d)) μ = ⊤

Tactic:
refine (Submodule.eq_top_iff_forall_basis_mem b).mpr fun j ↦ ?_
  exact Submodule.mem_iSup_of_mem (d j) <| by simp [diagonal_apply]

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 ≤ ρ - μ
⊢ μ ≤ ρ - μ

Tactic:
grind

Goal state after:
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 μ
q : R[X]
hq : minpoly R f = (X - C μ) * q
h_contra : ∀ (v : M), ((aeval f) q) v = 0
this : 1 + q.natDegree ≤ q.natDegree
⊢ False

Tactic:
grind

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

Goal state before:
pp: S : Type u
inst✝² : Semiring S
n : ℕ
inst✝¹ : Nontrivial S
inst✝ : NoZeroDivisors S
⊢ (ascPochhammer S n).Monic

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn =>
    have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1
    rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n.succ → R
⊢ (Fin.cons (fun j ↦ v 0 ^ ↑j) fun i ↦ Fin.cons 1 fun j ↦ tail v i * vandermonde (tail v) i j) =
    of Fin.cons (fun j ↦ v 0 ^ ↑j) fun i ↦ Fin.cons 1 fun j ↦ v i.succ * vandermonde (tail v) i j

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Vandermonde

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
i j : Fin n
⊢ (vandermonde v * (vandermonde w)ᵀ) i j = ∑ k, (v i * w j) ^ ↑k

Tactic:
by
  simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, mul_pow]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : ↑rn = -r
⊢ eval r (ascPochhammer R n) = 0

Tactic:
convert! ascPochhammer_eval_neg_coe_nat_of_lt hrn

Goal state after:
case e'_2
R : Type u
inst✝¹ : Ring R
inst✝ : IsDomain R
n : ℕ
r : R
rn : ℕ
hrn : rn < n
rnn : ↑rn = -r
⊢ r = -↑rn
Module: Mathlib.LinearAlgebra.Vandermonde

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

Tactic:
rfl

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
this :
  ∀ (ij kl : ι × ι),
    a ij.1 - a ij.2 = a kl.1 - a kl.2 →
      (algebraMap R K) (f ⟨a ij.1, ⋯⟩) - (algebraMap R K) (f ⟨a ij.2, ⋯⟩) =
        (algebraMap R K) (f ⟨a kl.1, ⋯⟩) - (algebraMap R K) (f ⟨a kl.2, ⋯⟩)
⊢ ∃ r, ∀ (i j : ι), Polynomial.eval (a i - a j) r = (algebraMap R K) (f ⟨a i, ⋯⟩) - (algebraMap R K) (f ⟨a j, ⋯⟩)

Tactic:
obtain ⟨r, hr⟩ := (Polynomial.exists_eval_eq_iff _ _).mpr this

Goal state after:
ι : 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
this :
  ∀ (ij kl : ι × ι),
    a ij.1 - a ij.2 = a kl.1 - a kl.2 →
      (algebraMap R K) (f ⟨a ij.1, ⋯⟩) - (algebraMap R K) (f ⟨a ij.2, ⋯⟩) =
        (algebraMap R K) (f ⟨a kl.1, ⋯⟩) - (algebraMap R K) (f ⟨a kl.2, ⋯⟩)
r : K[X]
hr :
  ∀ (i : ι × ι), Polynomial.eval (a i.1 - a i.2) r = (algebraMap R K) (f ⟨a i.1, ⋯⟩) - (algebraMap R K) (f ⟨a i.2, ⋯⟩)
⊢ ∃ r, ∀ (i j : ι), Polynomial.eval (a i - a j) r = (algebraMap R K) (f ⟨a i, ⋯⟩) - (algebraMap R K) (f ⟨a j, ⋯⟩)
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₂
y : ↥(prod eι b₁ b₂)
x : ↥H₂
hy :
  (prodSymmEquiv eι b₁ b₂).symm y ∈
    lieSpan R (↥(prod eι.symm b₂ b₁))
      (⇑(prodSymmEquiv eι b₁ b₂).symm.toLieHom '' {x | ∃ i, ⟨(b₁.h i, b₂.h (eι i)), ⋯⟩ = x})
x✝ : ↥(prod eι.symm b₂ b₁)
⊢ (∃ i, ⟨(b₂.h i, b₁.h (eι.symm i)), ⋯⟩ = x✝) ↔ ∃ a, ⟨(b₂.h (eι a), b₁.h a), ⋯⟩ = x✝

Tactic:
grind

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
⊢ ∏ j > 0, (↑↑j - ↑↑0) = ↑n.succ.factorial

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:
· simp only [Fin.val_zero, Nat.cast_zero, sub_zero]
      norm_cast
      simp [Fin.prod_univ_eq_prod_range (fun i ↦ (↑i + 1)) (n + 1)]

Goal state after:
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
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
⊢ eval (v i) (∑ i ∈ s, Lagrange.basis s v i) = 1

Tactic:
sum_basis (hvt.mono hst) hs,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s t : Finset ι
v r : ι → F
hvt : Set.InjOn v ↑t
hs : s.Nonempty
hst : s ⊆ t
i : ι
hi : i ∈ t
hi' : i ∉ s
⊢ eval (v i) 1 = 1
Module: Mathlib.LinearAlgebra.Lagrange

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
k : ℕ
hk : k < #s
i : ι
hi : i ∈ s
hvs' : Set.InjOn v ↑(s.erase i)
⊢ ↑(powersetCard (#s - (k + 1)) (s.erase i)) ⊆ ↑(s.erase i).powerset

Tactic:
grind

Goal state after: