mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
p : P
hp : p ∉ affineSpan k (Set.range s.points)
⊢ p ∈ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) ↔
    p ∈ ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior

Tactic:
apply iff_of_false (hp <| s.closedInterior_subset_affineSpan ·.1)
    rintro ⟨q, hq, rfl⟩
    exact hp <| homothety_mem (mem_affineSpan _ (by simp)) _ <|
      affineSpan_mono _ (by simp) ((s.faceOpposite i).closedInterior_subset_affineSpan hq)

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : f v = 0
x : V
⊢ (LinearMap.transvection f v) ((LinearMap.transvection f (-v)) x) = x

Tactic:
by
    have h' : f (-v) = 0 := by simp [h]
    simp [comp_of_left_eq_apply h']

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : ¬i = j
⊢ f (b j) = (b.coord i) (f (b i)) • b j

Tactic:
have := h' i j hij 1

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
f : V →ₗ[R] V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
h : ∀ (v : V), ¬LinearIndependent R ![v, f v]
feq : ∀ (i : ι), f (b i) = (b.coord i) (f (b i)) • b i
h' : ∀ (i j : ι), i ≠ j → ∀ (r : R), (b.coord i) (f (b i)) * r = r * (b.coord j) (f (b j))
i j : ι
hij : ¬i = j
this : (b.coord i) (f (b i)) * 1 = 1 * (b.coord j) (f (b j))
⊢ f (b j) = (b.coord i) (f (b i)) • b j
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ 2 • (associatedHom A) (Q₁.tmul Q₂) = ⅟2 • BilinForm.tmul (2 • (associatedHom A) Q₁) (polarBilin Q₂)

Tactic:
← two_nsmul_associated R,

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ 2 • (associatedHom A) (Q₁.tmul Q₂) = ⅟2 • BilinForm.tmul (2 • (associatedHom A) Q₁) (2 • (associatedHom R) Q₂)
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Goal state before:
pp: R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ (BilinForm.tensorDistrib R A) ((⅟2 • QuadraticMap.sq.polarBilin) ⊗ₜ[R] polarBilin Q) =
    BilinForm.tmul (LinearMap.mul A A) (polarBilin Q)

Tactic:
← two_nsmul_associated R,

Goal state after:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ (BilinForm.tensorDistrib R A) ((⅟2 • 2 • (associatedHom R) QuadraticMap.sq) ⊗ₜ[R] polarBilin Q) =
    BilinForm.tmul (LinearMap.mul A A) (polarBilin Q)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case ι
R : Type u_1
inst✝ : CommRing R
x : Unit
⊢ reverse ((ι 0) x) = (ι 0) x

Tactic:
rw [ι_eq_zero, LinearMap.zero_apply, reverse.map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case re
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 }.re =
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))).re

pp: case imI
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 }.imI =
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))).imI

pp: case imJ
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 }.imJ =
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))).imJ

pp: case imK
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
v : R × R
⊢ { re := 0 * 0 + c₁ * v.1 * v.1 + c₂ * v.2 * v.2 + 0 * c₂ * v.2 * 0 - c₁ * c₂ * 0 * 0,
        imI := 0 * v.1 + v.1 * 0 + 0 * v.1 * v.1 - c₂ * v.2 * 0 + c₂ * 0 * v.2,
        imJ := 0 * v.2 + c₁ * v.1 * 0 + v.2 * 0 + 0 * v.2 * v.1 - c₁ * 0 * v.1,
        imK := 0 * 0 + v.1 * v.2 + 0 * v.1 * 0 - v.2 * v.1 + 0 * 0 }.imK =
    (↑(c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2))).imK

Tactic:
all_goals dsimp; ring

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
c : CliffordAlgebra (Q c₁ c₂)
⊢ toQuaternion (involute (reverse c)) = star (toQuaternion c)

Tactic:
induction c using CliffordAlgebra.induction with
  | algebraMap r => simp
  | ι x => simp
  | mul x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
  | add x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
⊢ N.toAddSubgroup.index =
    Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index

Tactic:
rcases snf with ⟨bM, bN, f, a, snf⟩

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ N.toAddSubgroup.index =
    Nat.card R ^ (Fintype.card ι - n) *
      ∏ i, (Submodule.toAddSubgroup (Ideal.span {{ bM := bM, bN := bN, f := f, a := a, snf := snf }.a i})).index
Module: Mathlib.LinearAlgebra.FreeModule.ModN

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
f : ModN G n →+ M
g : G
Gn : AddSubgroup G := ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup
⊢ n • (f.comp (QuotientAddGroup.mk' ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup)) g = 0

Tactic:
suffices n • g ∈ (QuotientAddGroup.mk' Gn).ker by
      simp only [AddMonoidHom.coe_comp, comp_apply, ← map_nsmul]
      change f (QuotientAddGroup.mk' Gn (n • g)) = 0 -- Can we avoid `change`?
      rw [this, map_zero]

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
f : ModN G n →+ M
g : G
Gn : AddSubgroup G := ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup
⊢ n • g ∈ (QuotientAddGroup.mk' Gn).ker
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case succ
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
⊢ (M.submatrix i.succ.succAbove id).det = (↑↑i.succ).negOnePow • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
rw [Fin.val_succ, Nat.cast_add, Nat.cast_one, Int.negOnePow_succ, Units.neg_smul,
        ← neg_eq_iff_eq_neg, ← neg_one_smul R,
        ← det_updateRow_sum (M.submatrix i.succ.succAbove id) i (fun _ ↦ -1),
        ← Fin.val_castSucc i, ← h_ind]
      congr
      ext a b
      simp_rw [neg_one_smul, updateRow_apply, Finset.sum_neg_distrib, Pi.neg_apply,
        Finset.sum_apply, submatrix_apply, id_eq]
      split_ifs with h
      · 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]
      · obtain h | h := ne_iff_lt_or_gt.mp h
        · rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]
        · rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
snf : SmithNormalForm N ι n
⊢ (if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0) ≠ 0 ↔
    n = Fintype.card ι

Tactic:
rcases snf with ⟨bM, bN, f, a, snf⟩

Goal state after:
ι : Type u_1
M : Type u_3
n : ℕ
inst✝¹ : AddCommGroup M
inst✝ : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
⊢ (if n = Fintype.card ι then
        ∏ i, (Submodule.toAddSubgroup (Ideal.span {{ bM := bM, bN := bN, f := f, a := a, snf := snf }.a i})).index
      else 0) ≠
      0 ↔
    n = Fintype.card ι
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromRows (replicateRow m' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
refine fromRows_isTotallyUnimodular_iff_rows <| fun _ _ => ?_
  inhabit n
  refine ⟨default, 0, ?_⟩
  ext x
  simp [Pi.single_apply]

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

Goal state before:
pp: case pos
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
hs_det : (Matrix.of fun i j ↦ s (i, j)).det = 0
⊢ ((eval s) p - (eval s) q) * (Matrix.of fun i j ↦ s (i, j)).det = 0

Tactic:
hs_det,

Goal state after:
case pos
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
hs_det : (Matrix.of fun i j ↦ s (i, j)).det = 0
⊢ ((eval s) p - (eval s) q) * 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: case refine_2
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
d : n → R
⊢ ∏ i, diagonal d (1 i) i = ∏ i, d i

Tactic:
simp only [Perm.one_apply, diagonal_apply_eq]

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A i)
inst✝⁴ : Algebra R' R
inst✝³ : (i : ι) → Algebra R (A i)
inst✝² : (i : ι) → Algebra R' (A i)
inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
i : ι
inst✝ : DecidableEq ι
⊢ (algebraMap R' (⨂[R] (i : ι), A i)) r = (tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))

Tactic:
change r • tprod R 1 = _

Goal state after:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A i)
inst✝⁴ : Algebra R' R
inst✝³ : (i : ι) → Algebra R (A i)
inst✝² : (i : ι) → Algebra R' (A i)
inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
i : ι
inst✝ : DecidableEq ι
⊢ r • (tprod R) 1 = (tprod R) (Pi.mulSingle i ((algebraMap R' (A i)) r))
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A i)
inst✝⁴ : Algebra R' R
inst✝³ : (i : ι) → Algebra R (A i)
inst✝² : (i : ι) → Algebra R' (A i)
inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)
inst✝ : DecidableEq ι
i : ι
a a' : A i
⊢ (tprod R) ((MonoidHom.mulSingle A i) (a * a')) =
    (tprod R) ((MonoidHom.mulSingle A i) a) * (tprod R) ((MonoidHom.mulSingle A i) a')

Tactic:
simp [map_mul]

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (A i)
inst✝⁴ : Algebra R' R
inst✝³ : (i : ι) → Algebra R (A i)
inst✝² : (i : ι) → Algebra R' (A i)
inst✝¹ : ∀ (i : ι), IsScalarTower R' R (A i)
inst✝ : DecidableEq ι
i : ι
a a' : A i
⊢ (tprod R) ((MonoidHom.mulSingle A i) (a * a')) =
    (tprod R) ((MonoidHom.mulSingle A i) a) * (tprod R) ((MonoidHom.mulSingle A i) a')

Tactic:
by simp [map_mul]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
h : Module.finrank k V = 2
⊢ Nat.card (ℙ k V) = Nat.card k + 1

Tactic:
simp [card_of_finrank k V h]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
⊢ IsCollinear S ↔ ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M

Tactic:
IsCollinear_iff

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (Projectivization K V)
⊢ (∃ M, Module.Finite K ↥(Subspace.submodule M) ∧ Module.finrank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M) ↔
    ∃ M, Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
t : TransvectionStruct (Fin 2) F
⊢ t.toSpecialLinearGroup ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
obtain ⟨i, j, hij, c⟩ := t

Goal state after:
F : Type u_2
inst✝ : Field F
i j : Fin 2
hij : i ≠ j
c : F
⊢ { i := i, j := j, hij := hij, c := c }.toSpecialLinearGroup ∈
    lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 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
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
this : c = 1
⊢ ↑↑u x = LinearMap.id x

Tactic:
simp [← hc, LinearEquiv.smul_id_of_finrank_eq_one, this]

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

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
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
g : Matrix ι ι R →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ : Injective (⇑g ∘ ⇑(diagonalLinearMap ι R R))
⊢ Matrix.diagonal (0 ⊕ᵥ d) ∈ span R (range h) ↔ d ∈ span R (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))

Tactic:
have h₁ {d : ι → R} : diagonal (Sum.elim 0 d) = g (diagonalLinearMap ι R R d) := by
    ext (i | i) (j | j) <;> simp [g]

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
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
d : ι → R
g : Matrix ι ι R →ₗ[R] Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ : Injective (⇑g ∘ ⇑(diagonalLinearMap ι R R))
h₁ : ∀ {d : ι → R}, Matrix.diagonal (0 ⊕ᵥ d) = g ((diagonalLinearMap ι R R) d)
⊢ Matrix.diagonal (0 ⊕ᵥ d) ∈ span R (range h) ↔ d ∈ span R (range fun i j ↦ ↑(P.pairingIn ℤ j ↑i))
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
⊢ (algebraMap ℤ R) (P.pairingIn ℤ l i) = (algebraMap ℤ R) (1 - P.pairingIn ℤ j i)

Tactic:
simp only [algebraMap_pairingIn, map_sub, map_one, algebraMap_pairingIn]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : k ≠ j
hk' : P.root k + P.root i ∈ range ⇑P.root
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hl : P.root l = P.root k + P.root i - P.root j
hli : l ≠ i
hkl : P.pairingIn ℤ l k ≤ 0
hki : P.pairing k i = -1
⊢ P.pairing l i = 1 - P.pairing j i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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
inst✝⁴ : P.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
⊢ ω b * e i = f i * ω b

Tactic:
classical
  ext (k | k) (l | l)
  · simp [ω, e, f]
  · simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
      Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]
    simp [← ite_and, and_comm, -indexNeg_neg, neg_eq_iff_eq_neg]
  · simp [ω, e, f]
  · simp only [ω, e, f, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Matrix.of_apply, mul_ite, ← neg_eq_iff_eq_neg (a := k)]
    rw [Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)]
    simp [neg_eq_iff_eq_neg, sub_eq_add_neg]

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

Goal state before:
pp: case pos
ι : 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 ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := ⋯
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
⊢ ∃ k_1 x_1,
    P.root k_1 = P.root j + (n + 1) • P.root ↑i ∧ x • e i *ᵥ Pi.single (Sum.inr k) 1 = x_1 • Pi.single (Sum.inr k_1) 1

Tactic:
refine ⟨l, x * (P.chainBotCoeff i k + 1), hl, ?_⟩

Goal state after:
case pos
ι : 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 ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
l : ι
hl : P.root l = P.root j + (n + 1) • P.root ↑i
⊢ x • e i *ᵥ Pi.single (Sum.inr k) 1 = (x * (chainBotCoeff (↑i) k + 1)) • Pi.single (Sum.inr l) 1
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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
inst✝⁶ : P.IsCrystallographic
inst✝⁵ : P.IsReduced
inst✝⁴ : P.IsIrreducible
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsG2
i j : ι
h : P.root i ≠ P.root j
h' : P.root i ≠ -P.root j
⊢ P.pairingIn ℤ i j ∈ {-3, -1, 0, 1, 3}

Tactic:
suffices ¬ (∀ i j, P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
                     P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨
                     P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j) by
    have aux₁ := P.forall_pairingIn_eq_swap_or.resolve_left this i j
    have aux₂ := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i j h h'
    simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero,
      Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at aux₂ ⊢
    lia
  obtain ⟨k, l, hkl⟩ := exists_pairingIn_neg_three (P := P)
  push Not
  refine ⟨k, l, ?_⟩
  have aux := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed k l
  simp only [mem_insert_iff, mem_singleton_iff, Prod.mk_zero_zero, Prod.mk_eq_zero,
      Prod.mk_one_one, Prod.mk_eq_one, Prod.mk.injEq] at aux
  omega

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

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
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
⊢ P.pairingIn ℤ (short P) (long P) = -1

Tactic:
by
  have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed (long P) (short P)
  aesop

Goal state after: