mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case pos
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:
rw [← hij, ← feq]

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

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

Tactic:
let : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm

Goal state after:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
N₁ : Type uN₁
N₂ : Type uN₂
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing A
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : AddCommGroup M₂
inst✝¹³ : AddCommGroup N₁
inst✝¹² : AddCommGroup N₂
inst✝¹¹ : Algebra R A
inst✝¹⁰ : Module R M₁
inst✝⁹ : Module A M₁
inst✝⁸ : Module R N₁
inst✝⁷ : Module A N₁
inst✝⁶ : SMulCommClass R A M₁
inst✝⁵ : IsScalarTower R A M₁
inst✝⁴ : IsScalarTower R A N₁
inst✝³ : Module R M₂
inst✝² : Module R N₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticMap A M₁ N₁
Q₂ : QuadraticMap R M₂ N₂
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ associated (Q₁.tmul Q₂) = (associated Q₁).tmul (associated Q₂)
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
⊢ ∀ (m : A ⊗[R] V),
    (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m *
        (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m =
      (algebraMap A (A ⊗[R] CliffordAlgebra Q)) ((QuadraticForm.baseChange A Q) m)

Tactic:
let : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm

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
this : Invertible 2 := (Invertible.map (algebraMap R A) 2).copy 2 ⋯
⊢ ∀ (m : A ⊗[R] V),
    (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m *
        (TensorProduct.AlgebraTensorModule.map LinearMap.id (ι Q)) m =
      (algebraMap A (A ⊗[R] CliffordAlgebra Q)) ((QuadraticForm.baseChange A Q) m)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
r✝ : R
⊢ (foldr' Q (contractLeftAux Q (d₁ + d₂)) ⋯ 0) ((algebraMap R (CliffordAlgebra Q)) r✝) =
    (foldr' Q (contractLeftAux Q d₁) ⋯ 0) ((algebraMap R (CliffordAlgebra Q)) r✝) +
      (foldr' Q (contractLeftAux Q d₂) ⋯ 0) ((algebraMap R (CliffordAlgebra Q)) r✝)

Tactic:
foldr'_algebraMap,

Goal state after:
case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' d₁ d₂ : Module.Dual R M
r✝ : R
⊢ r✝ • 0 = r✝ • 0 + r✝ • 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
r✝ : R
⊢ (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0) ((algebraMap R (CliffordAlgebra Q)) r✝) =
    c • (foldr' Q (contractLeftAux Q d) ⋯ 0) ((algebraMap R (CliffordAlgebra Q)) r✝)

Tactic:
foldr'_algebraMap,

Goal state after:
case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d✝ d' : Module.Dual R M
c : R
d : Module.Dual R M
r✝ : R
⊢ r✝ • 0 = c • r✝ • 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
⊢ (ι Q') m = ((changeFormAux Q' B) m) 1

Tactic:
rw [changeFormAux_apply_apply, mul_one, contractLeft_one, sub_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : (ι Q).compr₂ f = (ι Q).compr₂ g
⊢ f = g

Tactic:
rw [EvenHom.ext_iff] at h

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f g : ↥(even Q) →ₐ[R] A
h : ((ι Q).compr₂ f).bilin = ((ι Q).compr₂ g).bilin
⊢ f = g
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ (Finsupp.single y 1) x + f v * (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0

Tactic:
Finsupp.single_eq_of_ne hxy,

Goal state after:
case neg
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
hfv : ¬f v = 0
ι : Set V
b : Basis (↑ι) K V
i : ↑ι
hv : v = b i
hf : f = f v • b.coord i
this : Fintype ↑ι
x y : ↑ι
hxy : ¬x = y
⊢ 0 + f v * (Finsupp.single y 1) i * (Finsupp.single i 1) x = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ (-1) ^ (i✝ * 0) • ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] ((lof R ι ℬ i✝) x✝ * 1) =
    r • (lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝

Tactic:
rw [mul_zero, uzpow_zero, one_smul, smul_tmul',
      mul_one, _root_.Algebra.smul_def, Algebra.commutes]

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] (lof R ι ℬ i✝) x✝ =
    ((lof R ι 𝒜 i✝¹) x✝¹ * (algebraMap R (⨁ (i : ι), 𝒜 i)) r) ⊗ₜ[R] (lof R ι ℬ i✝) x✝
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
y : (CliffordAlgebra Q)ˣ
hy₂ : ↑y = x
_hx₂ : star x * x = 1
hx₃ : x * star x = 1
hy₁ : y ∈ lipschitzGroup Q
⊢ ↑(star y) = star x

Tactic:
simp only [hy₂, Units.coe_star]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ((ofDirectSum.comp toDirectSum).toLinearMap ∘ₗ ι R) x✝ = ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ ι R) x✝

Tactic:
simp [tprod_apply]

Goal state after:
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
⊢ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd) = ⊤

Tactic:
rw [Submodule.eq_top_iff']

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (x : ExteriorAlgebra R M), x ∈ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd)
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: case id
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✝ maps : {i : I} → A i →ₐ[R] B
i✝ : I
⊢ (RingCon.ker ((TensorAlgebra.lift R) (toModule R I B fun x ↦ maps.toLinearMap)).toRingHom)
    ((TensorAlgebra.ι R) ((DirectSum.lof R I A i✝) 1)) 1

Tactic:
| id =>

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
⊢ (LinearIndependent S fun i ↦ ⇑(algebraMap R S) ∘ v i) ↔ LinearIndependent R v

Tactic:
change LinearIndependent S (Pi.algebraMap ι' R S ∘ v) ↔ LinearIndependent R v
  refine ⟨fun h ↦ (h.restrict_scalars' R).of_comp, fun h ↦ ?_⟩
  have : IsDomain R := .of_faithfulSMul R S
  set K := FractionRing R
  set L := FractionRing S
  replace h : LinearIndependent K (Pi.algebraMap ι' R K ∘ v) := by
    rw [← LinearIndependent.iff_fractionRing (R := R)]
    have : Function.Injective (Pi.algebraMap ι' R K) := by
      rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]
      intro v hv; ext i; simpa [Pi.algebraMap] using congr($hv i)
    rwa [LinearMap.linearIndependent_iff_of_injOn _ this.injOn]
  let : Algebra K L := FractionRing.liftAlgebra R L
  suffices LinearIndependent L (Pi.algebraMap ι' R L ∘ v) by
    rw [← LinearIndependent.iff_fractionRing (R := S)] at this
    have aux : Pi.algebraMap ι' R L ∘ v = Pi.algebraMap ι' S L ∘ Pi.algebraMap ι' R S ∘ v := by
      ext; simp [Pi.algebraMap, ← IsScalarTower.algebraMap_apply]
    rw [aux] at this
    exact this.of_comp
  have aux : Pi.algebraMap ι' R L ∘ v = Pi.algebraMap ι' K L ∘ Pi.algebraMap ι' R K ∘ v := by
    ext; simp [Pi.algebraMap, ← IsScalarTower.algebraMap_apply]
  rw [aux]
  replace h := h.linearIndependent_algebraMap_comp_aux L
  exact h

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
⊢ circulant v k 0 = w k

Tactic:
← circulant_col_zero_eq w,

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
⊢ circulant v k 0 = circulant w k 0
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case pos
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
h : ↑A 1 0 = 0
⊢ C A

Tactic:
exact base _ h

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 k : ℤ
H : Finset ℤ := Finset.Icc (-|k|) |k|
H4 : Type := Fin 2 → Fin 2 → ↥H
M N : ↑(reps k)
h : (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) M = (fun M i j ↦ ⟨↑↑M i j, ⋯⟩) N
i j : Fin 2
⊢ ↑↑M i j = ↑↑N i j

Tactic:
simpa only [Subtype.mk.injEq] using congrFun₂ h i j

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

Goal state before:
pp: case pred
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✝
m : ℕ
hm : C (T ^ (-↑m) • B) ↔ C B
⊢ C (T ^ (-↑m - 1) • B) ↔ C B

Tactic:
sub_eq_neg_add,

Goal state after:
case pred
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✝
m : ℕ
hm : C (T ^ (-↑m) • B) ↔ C B
⊢ C (T ^ (-1 + -↑m) • B) ↔ C B
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case succ.mpr.cons
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 b : n
q : Path i b
e : b ⟶ j
hp_len : q.length = m
h_Am_pos : 0 < (A ^ m) i b
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j

Tactic:
let h_A_pos := e

Goal state after:
case succ.mpr.cons
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 b : n
q : Path i b
e : b ⟶ j
hp_len : q.length = m
h_Am_pos : 0 < (A ^ m) i b
h_A_pos : b ⟶ j := e
⊢ 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : m
g : Matrix m n R
⊢ (g * swap R i j) a i = g a j

Tactic:
by
  simp [swap, PEquiv.mul_toMatrix_toPEquiv]

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

Goal state before:
pp: case succ
R : Type u_2
M₂ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : Module.Finite R M₂
inst✝⁴ : Module.Free R M₂
n : ℕ
ih :
  ∀ (N : Fin n → Type u_5) [inst : (i : Fin n) → AddCommGroup (N i)] [inst_1 : (i : Fin n) → Module R (N i)]
    [∀ (i : Fin n), Module.Finite R (N i)] [∀ (i : Fin n), Module.Free R (N i)],
    Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
N : Fin (n + 1) → Type u_5
inst✝³ : (i : Fin (n + 1)) → AddCommGroup (N i)
inst✝² : (i : Fin (n + 1)) → Module R (N i)
inst✝¹ : ∀ (i : Fin (n + 1)), Module.Finite R (N i)
inst✝ : ∀ (i : Fin (n + 1)), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
| succ n ih =>

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst✝ : CommMagma α
⊢ ∀ (a b : WithConv (Matrix m n α)), a * b = b * a

Tactic:
by simp [hadamard_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: case succ
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
hι : Nat.card ι = n + 1
this : Nonempty ι
⊢ φ = φ'

Tactic:
have i₀ : ι := Classical.arbitrary _

Goal state after:
case succ
R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
⊢ φ = φ'
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬((Projectivization.rep ∘ ![u, v]) 1 ≠ 0 ∧
        ∀ (a : K), a • (Projectivization.rep ∘ ![u, v]) 1 ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔
    u = v

Tactic:
dsimp only [Function.comp_def, Matrix.cons_val]

Goal state after:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬(v.rep ≠ 0 ∧ ∀ (a : K), a • v.rep ≠ u.rep) ↔ u = v
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case add
ι : 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
i : ↥b.support
j : ↥b.support ⊕ ι
x u v : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx✝ : u ∈ span R (range h)
hy✝ : v ∈ span R (range h)
hu : u j (Sum.inl i) = 0
hv : v j (Sum.inl i) = 0
⊢ (u + v) j (Sum.inl i) = 0

Tactic:
| add u v _ _ hu hv =>

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

Goal state before:
pp: case add
ι : 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✝ : DecidableEq ι
j : ι
x u v : ↥b.support ⊕ ι → R
hx✝ : u ∈ span R (range GeckConstruction.u)
hy✝ : v ∈ span R (range GeckConstruction.u)
hu : u (Sum.inr j) = 0
hv : v (Sum.inr j) = 0
⊢ (u + v) (Sum.inr j) = 0

Tactic:
| add u v _ _ hu hv =>

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

Goal state before:
pp: case add
ι : 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✝¹ : DecidableEq ι
inst✝ : Fintype ι
x u v : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx✝ : u ∈ LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f)
hy✝ : v ∈ LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f)
hu : (ωConj b) u ∈ lieAlgebra b
hv : (ωConj b) v ∈ lieAlgebra b
⊢ (ωConj b) (u + v) ∈ lieAlgebra b

Tactic:
| add u v _ _ hu hv =>

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

Goal state before:
pp: case succ
ι : 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 : ℕ
ih :
  (e i ^ n).col (Sum.inr j) = 0 ∨
    ∃ k x, P.root k = P.root j + n • P.root ↑i ∧ (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
⊢ (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
    ∃ k x, P.root k = P.root j + (n + 1) • P.root ↑i ∧ (e i ^ (n + 1)).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
ι : 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
n : ℕ
ih : ω b * f i ^ n = e i ^ n * ω b
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b

Tactic:
| succ n ih =>

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

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✝⁵ : 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
_i : InvolutiveNeg ι := P.indexNeg
this : ∑ j, P.pairingIn ℤ (-j) ↑i = ∑ j, P.pairingIn ℤ j ↑i
⊢ -∑ j, P.pairingIn ℤ j ↑i = ∑ j, P.pairingIn ℤ j ↑i

Tactic:
by simpa using this

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
d : ↥b.support ⊕ ι → K
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K
hx : x ∈ lieAlgebra b
hx' : ⟨x, hx⟩ ∈ H
μ : K := χ ⟨⟨x, hx⟩, hx'⟩
hdx : x = diagonal d
this : ∀ (d : ↥b.support ⊕ ι → K) (μ : K), toLin' (diagonal d) - μ • 1 = toLin' (diagonal (d - μ • 1))
⊢ w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) μ ⟨⟨x, hx⟩, hx'⟩ ↔ ∃ k, diagonal ((d - μ • 1) ^ k) *ᵥ w = 0

Tactic:
simp [mem_genWeightSpaceOf, hdx, this, ← toLin'_pow, diagonal_pow]

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, f i⁆ = -(2 • f i)

Tactic:
by rw [lie_h_f]; simp

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.EmbeddedG2
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsIrreducible
this : P.pairing (long P) (short P) = -3
h : P.root (short P) = -P.root (long P)
⊢ False

Tactic:
· simp only [root_eq_neg_iff] at h
      norm_num [h] at this

Goal state after: