mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
ι : Type u_3 := Free.ChooseBasisIndex R M
b : Basis ι R M
this✝ : Fintype (Free.ChooseBasisIndex R M)
e : (M →ₗ[R] N) ≃ₗ[R] ι → N := LinearEquiv.congrLeft N R b.repr ≪≫ₗ (Finsupp.llift N R R ι).symm
f : (M →ₗ[R] P) ≃ₗ[S] ι → P := LinearEquiv.congrLeft P S b.repr ≪≫ₗ (Finsupp.llift P R S ι).symm
h : S ⊗[R] (M →ₗ[R] N) →ₗ[S] M →ₗ[R] P := linearMapRightBaseChangeHom S M ε
e' : S ⊗[R] (M →ₗ[R] N) ≃ₗ[S] S ⊗[R] (ι → N) := LinearEquiv.baseChange R S (M →ₗ[R] N) (ι → N) e
h' : S ⊗[R] (ι → N) →ₗ[S] ι → P := (↑f ∘ₗ linearMapRightBaseChangeHom S M ε) ∘ₗ ↑e'.symm
this : ↑f ∘ₗ linearMapRightBaseChangeHom S M ε = ↑⋯.equiv ∘ₗ ↑e'
⊢ h' = ↑⋯.equiv

Tactic:
simp [h', this, ← LinearEquiv.trans_assoc e'.symm e']

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_2
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
M : Type u_3
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_4
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type u_5
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
Q : Type u_6
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Module S Q
inst✝ : IsScalarTower R S Q
α : M →ₗ[R] P
j : IsBaseChange S α
β : N →ₗ[R] Q
f : M →ₗ[R] N
⊢ ↑R ((j.linearMapLeftRightHom β) f) ∘ₗ α = β ∘ₗ f

Tactic:
ext; simp [linearMapLeftRightHom_comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case mpr
R : Type u_4
V : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e : V ≃ₗ[R] V
a : R
⊢ (∀ (v : V), e.fixedReduce ((↑e).fixedSubmodule.mkQ v) = (↑e).fixedSubmodule.mkQ (a • v)) →
    ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x

Tactic:
· intro H x
    have ⟨y, hy⟩ := e.fixedSubmodule.mkQ_surjective x
    rw [← hy]
    apply H

Goal state after:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : V →ₗ[R] V
a : R
hf : ∀ (x : V), f x = a • x
⊢ f ∈ center (End R V)

Tactic:
by
  simp [mem_center_iff, isMulCentral_iff, commute_iff_eq, mul_assoc, LinearMap.ext_iff, hf]

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

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 1
h1 : 1 ≤ 1
b : Basis (Fin (finrank R V)) R V := finBasis R V
x : V
⊢ 0 < finrank R V

Tactic:
by simp [h]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ (↑(AlgEquiv.toOpposite A A)).toLinearMap)
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)

Tactic:
AlgEquiv.toAlgHom_toLinearMap,

Goal state after:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ ↑↑(AlgEquiv.toOpposite A A))
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
i : Fin n
⊢ γ (MvPolynomial.X (Sum.inl i)) = f (ε (Pi.single i 1))

Tactic:
hε

Goal state after:
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε : ∀ (i : Fin n), ε (Pi.single i 1) = b i
fM : Dual S M := Fintype.linearCombination S fun i ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun i ↦ MvPolynomial.X (Sum.inr i)
i : Fin n
⊢ γ (MvPolynomial.X (Sum.inl i)) = f (b i)
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ↑s
g : ↑s → R
hg : ∑ x ∈ t, g x • ↑x ∈ M'
i : ↑s
hi : i ∈ t
⊢ g i = 0

Tactic:
obtain ⟨r, hg⟩ := hN hg

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ↑s
g : ↑s → R
hg✝ : ∑ x ∈ t, g x • ↑x ∈ M'
i : ↑s
hi : i ∈ t
r : ↥(nonZeroDivisors R)
hg : r • ∑ x ∈ t, g x • ↑x = 0
⊢ g i = 0
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ((lift R A) fun {i} ↦ maps) ∘ₐ ι R A i = maps

Tactic:
ext a

Goal state after:
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
a : A i
⊢ (((lift R A) fun {i} ↦ maps) ∘ₐ ι R A i) a = maps a
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝² : Zero R
inst✝¹ : LT n
inst✝ : WellFoundedLT n
i : m
⊢ A i ≠ 0 ↔ ∃ c, A.IsLeadingEntry i c

Tactic:
by
  refine ⟨fun h => ?_, fun ⟨c, hc⟩ => hc.row_ne_zero⟩
  obtain ⟨c, hc, hmin⟩ := wellFounded_lt.has_min {j | A i j ≠ 0} <| Function.ne_iff.mp h
  refine ⟨c, ?_, hc⟩
  by_contra
  aesop

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
⊢ N.toAddSubgroup.index ≠ 0 ↔ n = Fintype.card ι

Tactic:
rw [snf.toAddSubgroup_index_eq_ite]
  rcases snf with ⟨bM, bN, f, a, snf⟩
  simp only [ne_eq, ite_eq_right_iff, Classical.not_imp, and_iff_left_iff_imp]
  have ha : ∀ i, a i ≠ 0 := by
    intro i hi
    apply Basis.ne_zero bN i
    specialize snf i
    simpa [hi] using snf
  intro h
  simpa [Ideal.span_singleton_toAddSubgroup_eq_zmultiples, Int.index_zmultiples,
    Finset.prod_eq_zero_iff] using ha

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

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3
base : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A
step : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (reduceStep A) → C A
A : FixedDetMatrix (Fin 2) ℤ m
⊢ C A

Tactic:
by_cases h : (A.1 1 0) = 0
  · exact base _ h
  · exact step A h (reduce_rec base step (reduceStep A))

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

Goal state before:
pp: case succ.mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
⊢ Nonempty { p // p.length = m + 1 }

Tactic:
have h_A : 0 < A l j := by by_contra! h; simp [le_antisymm h hA_nonneg'] at hl_pos

Goal state after:
case succ.mp
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
h_A : 0 < A l j
⊢ Nonempty { p // p.length = m + 1 }
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ ∀ (n : ℤ), C (T ^ n • B) ↔ C B

Tactic:
n

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
n : ℤ
⊢ C (T ^ n • B) ↔ C B
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)

Tactic:
refine eigenvalue_mem_ball ?_

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ Module.End.HasEigenvalue (Matrix.toLin' A) 0
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case inl
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
hac : ¬a = c
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B (a, b) (c, d) = 0

pp: case inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
hbd : ¬b = d
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B (a, b) (c, d) = 0

Tactic:
· simp [hA hac]

Goal state after:
case inr
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
hbd : ¬b = d
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) A B (a, b) (c, d) = 0
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ (diagonal fun x ↦ 1).permanent = 1

Tactic:
simp [-diagonal_one]

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
a₁ a₂ a₃ : (i : ι) → A i
ha : SemiconjBy a₁ a₂ a₃
⊢ SemiconjBy ((PiTensorProduct.tprod R) a₁) ((PiTensorProduct.tprod R) a₂) ((PiTensorProduct.tprod R) a₃)

Tactic:
SemiconjBy,

Goal state after:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
a₁ a₂ a₃ : (i : ι) → A i
ha : SemiconjBy a₁ a₂ a₃
⊢ (PiTensorProduct.tprod R) a₁ * (PiTensorProduct.tprod R) a₂ =
    (PiTensorProduct.tprod R) a₃ * (PiTensorProduct.tprod R) a₁
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
⊢ Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)

Tactic:
have : 1 < Nat.card k := Finite.one_lt_card

Goal state after:
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)
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✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i

Tactic:
have : 1 < Nat.card k := Finite.one_lt_card

Goal state after:
k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
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
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
⊢ LinearEquiv.det (LinearEquiv.baseChange R S V V ↑g) = 1

Tactic:
by
      rw [LinearEquiv.det_baseChange, g.prop, map_one]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
x y : M
hx : x ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
hy : y ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
this : Q (x + y) = Q x + Q y
⊢ Q x + Q y = 0

Tactic:
hx.1,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
x y : M
hx : x ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
hy : y ∈ {x | Q x = 0 ∧ Q.polarBilin x = 0}
this : Q (x + y) = Q x + Q y
⊢ 0 + Q y = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
⊢ comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃

Tactic:
have h₁ : Q₁ = Q₂.comp f.toLinearMap := QuadraticMap.ext fun x => (f.map_app x).symm
  have h₃ : Q₃ = Q₄.comp g.toLinearMap := QuadraticMap.ext fun x => (g.map_app x).symm
  refine (QuadraticMap.associated_rightInverse R).injective ?_
  ext m₁ m₃ m₁' m₃'
  simp [h₁, h₃, associated_tmul]

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 ι
i : ↥b.support
⊢ h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i))

Tactic:
by
  ext (j | j) (k | k) <;> simp [h, Matrix.diagonal_apply]

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 ι
i : ↥b.support
⊢ h i = Matrix.diagonal (0 ⊕ᵥ fun x ↦ ↑(P.pairingIn ℤ x ↑i))

Tactic:
by
  ext (j | j) (k | k) <;> simp [h, Matrix.diagonal_apply]

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✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h) ≤ cartanSubalgebra b

Tactic:
LieSubalgebra.lieSpan_le,

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✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ range h ⊆ ↑(cartanSubalgebra b)
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
i k : ι
inst✝ : P.IsNotG2
hik_mem : P.root k + P.root i ∈ range ⇑P.root
this : Module.IsReflexive R M
⊢ P.pairingIn ℤ k i = 0 ∨ P.pairingIn ℤ k i < 0 ∧ chainBotCoeff i k = 0

Tactic:
have := pairingIn_le_zero_of_root_add_mem hik_mem

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
i k : ι
inst✝ : P.IsNotG2
hik_mem : P.root k + P.root i ∈ range ⇑P.root
this✝ : Module.IsReflexive R M
this : P.pairingIn ℤ k i ≤ 0
⊢ P.pairingIn ℤ k i = 0 ∨ P.pairingIn ℤ k i < 0 ∧ chainBotCoeff i k = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inr.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
inst✝⁴ : P.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ (ω b * e i) (Sum.inr k) (Sum.inr l) = (f i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
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.Finite.G2

Goal state before:
pp: case refine_2
ι : 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
h :
  ∀ (i j : ι),
    P.pairingIn ℤ i j = -2 ∨
      P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 0 ∨ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ i j = 2
i j : ι
⊢ ¬P.pairingIn ℤ i j = -3

Tactic:
specialize h i j
    lia

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

Goal state before:
pp: case pos.inr.inl
ι : 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
m : ι
hl : P.root m = P.root ↑i + P.root k
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr m) =
    ((x * (chainBotCoeff (↑i) k + 1)) • Pi.single (Sum.inr m) 1) (Sum.inr m)

Tactic:
simp [e, -indexNeg_neg, hl, mul_add]

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✝² : CharZero R
inst✝¹ : P.IsCrystallographic
inst✝ : P.IsReduced
long short : ι
h : P.pairingIn ℤ long short = 3
⊢ P.pairingIn ℤ ((P.reflectionPerm long) long) short = -3

Tactic:
by simp [h]

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
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
y : ι
hy : P.root k = P.root y - P.root ↑i
⊢ LinearIndependent R ![P.root ↑i, P.root x]

Tactic:
simpa [hx] using h_lin_ind

Goal state after: