mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e_f
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
a₁ a₂ : A
i : ι
⊢ (of R 𝒜 ℬ) ((a₁ * ↑(((decompose 𝒜) a₂) i)) ⊗ₜ[R] ↑GradedMonoid.GOne.one) =
    (-1) ^ 0 • (a₁ * ↑(((decompose 𝒜) a₂) i)) ᵍ⊗ₜ[R] (↑GradedMonoid.GOne.one * ↑GradedMonoid.GOne.one)

Tactic:
uzpow_zero,

Goal state after:
case e_f
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
a₁ a₂ : A
i : ι
⊢ (of R 𝒜 ℬ) ((a₁ * ↑(((decompose 𝒜) a₂) i)) ⊗ₜ[R] ↑GradedMonoid.GOne.one) =
    1 • (a₁ * ↑(((decompose 𝒜) a₂) i)) ᵍ⊗ₜ[R] (↑GradedMonoid.GOne.one * ↑GradedMonoid.GOne.one)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (i : ℕ) (x : ↥(⋀[R]^i M)), (GradedAlgebra.liftι R M) ↑x = (DirectSum.of (fun i ↦ ↥(⋀[R]^i M)) i) x

Tactic:
apply GradedAlgebra.liftι_eq R M

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
⊢ (M ^ Fintype.card K).trace = M.trace ^ Fintype.card K

Tactic:
by
  cases isEmpty_or_nonempty n
  · simp [Matrix.trace]
  rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff,
    FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case succ
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
n✝ : ℕ
f : Fin (n✝ + 1) → m
g✝ : Fin (n✝ + 1) → n
a✝¹ : Function.Injective f
a✝ : Function.Injective g✝
⊢ (A.submatrix f g✝).det ∈ Set.range SignType.cast

Tactic:
exact (IsEmpty.false (f 0)).elim

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
⊢ -∑ x, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b

pp: case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : ¬a = i
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Tactic:
· replace hv := congr_fun hv b
        rw [Fin.sum_univ_succAbove _ i.succ, Pi.add_apply, Finset.sum_apply] at hv
        rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : ¬a = i
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
← one_smul R M.det,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
⊢ 1 • M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
let em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) :=
    MulEquiv.funMultiplicative _ _

Goal state after:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
have h : H'.index = H.index := Subgroup.index_comap_of_surjective _ em.surjective

Goal state after:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
⊢ A.rank = #{i | l i ≠ ⊤}

Tactic:
by
  refine le_antisymm (A.rank_le_card_of_support_subset _
    (Function.support_subset_iff'.mpr fun i hi => hA.eq_top_iff.mp (by aesop))) ?_
  let g : {i // l i ≠ ⊤} → n := fun i => (l i.1).untop i.2
  have hlead : ∀ i : {i // l i ≠ ⊤}, A.IsLeadingEntry i.1 (g i) := fun i =>
    hA.isLeadingEntry (WithTop.coe_untop (l i.1) i.2).symm
  have htri : (A.submatrix Subtype.val g).IsUpperTriangular := by
    intro i j hij
    exact (hlead i).1 _ ((WithTop.untop_lt_untop_iff _ _).mpr (hA.strictMonoOn j.2 i.2 hij))
  have hdet : (A.submatrix Subtype.val g).det ≠ 0 := by
    rw [det_of_isUpperTriangular htri]
    exact prod_ne_zero_iff.mpr fun i _ => (hlead i).2
  calc #{i | l i ≠ ⊤}
      = (A.submatrix Subtype.val g).rank := by
        rw [rank_of_det_ne_zero hdet, Fintype.card_subtype]
    _ ≤ A.rank := rank_submatrix_le A Subtype.val g

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial

Goal state before:
pp: m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
s : m × m → k
⊢ ((eval s) p - (eval s) q) * (eval s) (Matrix.mvPolynomialX m m k).det = 0

Tactic:
Matrix.eval_det_mvPolynomialX

Goal state after:
m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
s : m × m → k
⊢ ((eval s) p - (eval s) q) * (Matrix.of fun i j ↦ s (i, j)).det = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : { s // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
this : Invertible ((Pi.basisFun 𝔽 (Fin n)).toMatrix ⇑b)
⊢ IsUnit (↑M)ᵀ.det

Tactic:
rw [← Basis.coePiBasisFun.toMatrix_eq_transpose,
      ← coe_basisOfPiSpaceOfLinearIndependent M.2]

Goal state after:
𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : { s // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
this : Invertible ((Pi.basisFun 𝔽 (Fin n)).toMatrix ⇑b)
⊢ IsUnit ((Pi.basisFun 𝔽 (Fin n)).toMatrix ⇑(basisOfPiSpaceOfLinearIndependent ⋯)).det
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h : A ∈ reps m
i j : Fin 2
⊢ |↑A i j| ≤ |m|

Tactic:
obtain ⟨h10, h00, h01, h11⟩ := h

Goal state after:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
i j : Fin 2
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
⊢ |↑A i j| ≤ |m|
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℤ
⊢ (A.map Int.cast).num = A

Tactic:
simp [Matrix.num, Function.comp_def]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℕ
⊢ (A.map Nat.cast).num = A.map Nat.cast

Tactic:
simp [Matrix.num, Function.comp_def]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ mapMatrixModule ι id = id

Tactic:
by
  ext; simp

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ mapMatrixModule ι (g ∘ₗ f) = mapMatrixModule ι g ∘ₗ mapMatrixModule ι f

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
⊢ piFamily 0 = 0

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
⊢ piFamily (f + g) = piFamily f + piFamily g

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
⊢ piFamily (s • f) = s • piFamily f

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
nontriviality V
  cases finite_or_infinite k with
  | inr h =>
    have : Infinite V := Module.Free.infinite k V
    simp
  | inl h =>
  cases finite_or_infinite V with
  | inr h =>
    have := not_iff_not.mpr (finite_iff_of_finite k V)
    push Not at this
    have : Infinite (ℙ k V) := by rwa [this]
    simp
  | inl h =>
  classical
  have : Fintype V := Fintype.ofFinite V
  have : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
  have : Fintype k := Fintype.ofFinite k
  have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
  simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
  rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_2.refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : iSupIndep fun i ↦ (f i).submodule
i : ι
⊢ (Projectivization.rep ∘ f) i ∈ (Projectivization.submodule ∘ f) i

Tactic:
simpa only [Function.comp_apply, submodule_eq] using Submodule.mem_span_singleton_self _

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : SpecialLinearGroup R V
⊢ LinearMap.det ↑↑u = 1

Tactic:
by
  simp [← LinearEquiv.coe_det, u.prop]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Free R V
d1 : Module.finrank R V = 1
u✝ v : SpecialLinearGroup R V
a✝ : Nontrivial R
x✝ : V
hx : ¬x✝ = 0
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1) c = ↑↑u
⊢ ↑↑u x = LinearMap.id x

Tactic:
suffices c = 1 by
      simp [← hc, LinearEquiv.smul_id_of_finrank_eq_one, this]

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Free R V
d1 : Module.finrank R V = 1
u✝ v : SpecialLinearGroup R V
a✝ : Nontrivial R
x✝ : V
hx : ¬x✝ = 0
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1) c = ↑↑u
⊢ c = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : Nontrivial V
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)

Tactic:
rw [← Module.finrank_pos_iff_of_free (R := R)] at hV

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Nontrivial R
hV : 0 < Module.finrank R V
⊢ ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
⊢ Q m' + 0 + polar (⇑Q) m' (m - m') = Q m'

Tactic:
add_zero,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
⊢ Q m' + polar (⇑Q) m' (m - m') = Q m'
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
⊢ Q.radical ≤ LinearMap.ker Q.polarBilin

Tactic:
intro m

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
m : M
⊢ m ∈ Q.radical → m ∈ LinearMap.ker Q.polarBilin
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
⊢ Q.radical = LinearMap.ker Q.polarBilin

Tactic:
by
  ext m
  simp only [mem_radical_iff', LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.zero_apply,
    QuadraticMap.polarBilin_apply_apply, QuadraticMap.polar]
  refine ⟨by simp +contextual, fun h ↦ ?_⟩
  suffices Q m = 0 by grind
  specialize h m
  rwa [← two_smul R, QuadraticMap.map_smul, sub_sub, ← two_smul R, mul_smul, ← smul_sub,
    (isUnit_of_invertible 2).smul_eq_zero, two_smul, add_sub_cancel_right] at h

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

Goal state before:
pp: M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
⊢ sigPos Q + Module.finrank 𝕜 ↥V ≤ Module.finrank 𝕜 M

Tactic:
← hr

Goal state after:
M : Type u_2
inst✝⁴ : AddCommGroup M
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : Module 𝕜 M
Q : QuadraticForm 𝕜 M
inst✝ : FiniteDimensional 𝕜 M
V : Subspace 𝕜 M
hV : ∀ x ∈ V, Q x ≤ 0
Vp : Submodule 𝕜 M
hr : Module.finrank 𝕜 ↥Vp = sigPos Q
hVp : (QuadraticMap.restrict Q Vp).PosDef
⊢ Module.finrank 𝕜 ↥Vp + Module.finrank 𝕜 ↥V ≤ Module.finrank 𝕜 M
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

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✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -⁅h j, e i⁆ * ω b = -(b.cartanMatrix i j • e i) * ω b

Tactic:
lie_h_e

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -(b.cartanMatrix i j • e i) * ω b = -(b.cartanMatrix i j • e i) * ω b
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_4
ι : 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✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P) =
    (P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortAddLongRoot P)) (shortAddLongRoot P)

Tactic:
rw [long_eq_three_mul_short, shortAddLongRoot_shortRoot]; ring

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ lieAlgebra b
i : ↥b.support
⊢ (trace R (↥b.support ⊕ ι → R)) ((toEnd R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R)) (f i)) = 0

Tactic:
simpa using Matrix.isNilpotent_trace_of_isNilpotent (isNilpotent_f i)

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

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✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i : ↥b.support
inst✝¹ : P.IsReduced
inst✝ : DecidableEq ι
⊢ ⁅h i, e i⁆ = 2 • e i

Tactic:
lie_h_e

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i : ↥b.support
inst✝¹ : P.IsReduced
inst✝ : DecidableEq ι
⊢ b.cartanMatrix i i • e i = 2 • e i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ι
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr ↑j) = 0 (Sum.inr k) (Sum.inr ↑j)

Tactic:
rw [← ⁅e i, f j⁆.transpose_apply, lie_e_f_ne_aux₁ hij, Pi.zero_apply, Matrix.zero_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
⊢ (↑s₁).pi t₁ ∩ (↑s₂).pi t₂ ∈ squareCylinders C

Tactic:
have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i :=
    fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm

Goal state after:
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
⊢ (↑s₁).pi t₁ ∩ (↑s₂).pi t₂ ∈ squareCylinders C
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
j : ↥J
⊢ ⋃₀ ↑⋯.choose.parts ⊆ ↑j

Tactic:
← Finset.sup_id_set_eq_sUnion,

Goal state after:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
j : ↥J
⊢ ⋯.choose.parts.sup id ⊆ ↑j
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ ⨆ x, ⋃₀ ↑⋯.choose.parts = ⋃₀ ↑J

Tactic:
← Finset.sup_id_set_eq_sUnion,

Goal state after:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ ⨆ x, ⋯.choose.parts.sup id = J.sup id