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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ Fin.cons x₀ x a))
        (0 :: List.map Fin.succ (List.finRange n))).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Tactic:
List.map_cons,

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ Fin.cons x₀ x 0) ::
        List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ Fin.cons x₀ x a))
          (List.map Fin.succ (List.finRange n))).prod =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))
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
m : M
⊢ ↑⟨(ι R) m, ⋯⟩ = (CliffordAlgebra.ι 0) m

Tactic:
Subtype.coe_mk

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (ι R) m = (CliffordAlgebra.ι 0) m
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
m : M
⊢ (DirectSum.coeAlgHom fun i ↦ ⋀[R]^i M) (((lift R) ⟨GradedAlgebra.ι R M, ⋯⟩) ((CliffordAlgebra.ι 0) m)) =
    (CliffordAlgebra.ι 0) m

Tactic:
rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]

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

Goal state before:
pp: I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A ∘ₗ DirectSum.lof R I A i) 1 = 1

Tactic:
dsimp [mkAlgHom]

Goal state after:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A) ((DirectSum.lof R I A i) 1) = 1
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
⊢ ∃ M' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)

Tactic:
have hL₁' : Surjective (Prod.fst ∘ L'.subtype) := by
    simp only [← coe_fst (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
    simpa only [L', ← LinearMap.range_comp, fst_prod, range_eq_top] using
      (LinearMap.fst ..).submoduleMap_surjective L

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
⊢ ∃ M' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Basic

Goal state before:
pp: case inl
m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝³ : Zero R
inst✝² : LinearOrder m
inst✝¹ : LT n
inst✝ : One R
i₁ i₂ : m
c : n
hA : A.IsReducedRowEchelon
hne : i₁ ≠ i₂
hlead : A.IsLeadingEntry i₂ c
hlt : i₁ < i₂
⊢ A i₁ c = 0

pp: case inr
m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝³ : Zero R
inst✝² : LinearOrder m
inst✝¹ : LT n
inst✝ : One R
i₁ i₂ : m
c : n
hA : A.IsReducedRowEchelon
hne : i₁ ≠ i₂
hlead : A.IsLeadingEntry i₂ c
hlt : i₂ < i₁
⊢ A i₁ c = 0

Tactic:
· exact hA.eq_zero hlt hlead

Goal state after:
case inr
m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝³ : Zero R
inst✝² : LinearOrder m
inst✝¹ : LT n
inst✝ : One R
i₁ i₂ : m
c : n
hA : A.IsReducedRowEchelon
hne : i₁ ≠ i₂
hlead : A.IsLeadingEntry i₂ c
hlt : i₂ < i₁
⊢ A i₁ c = 0
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
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
⊢ (∃ i, (f i).isRight = true) ∨ ∃ f', f = Sum.inl ∘ f'

Tactic:
or_iff_not_imp_left,

Goal state after:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
⊢ (¬∃ i, (f i).isRight = true) → ∃ f', f = Sum.inl ∘ f'
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
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
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ ∑ x, M (i.succ.succAbove x) b + M i.succ b = 0

Tactic:
add_comm

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
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
hv : M i.succ b + ∑ c, M (i.succ.succAbove c) b = 0 b
⊢ M i.succ b + ∑ x, M (i.succ.succAbove x) b = 0
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
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)
⊢ ∀ (i : Fin n), a i ≠ 0

Tactic:
intro i hi

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)
i : Fin n
hi : a i = 0
⊢ False
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 : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0
⊢ ((-1) ^ (↑j₀ + ↑i₀) * ∑ i, Mᵀ i i₀) * (M.submatrix i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det

Tactic:
add_comm

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 : ∀ (i : Fin (n + 1)), i ≠ i₀ → ∑ j, M i j = 0
⊢ ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, Mᵀ i i₀) * (M.submatrix i₀.succAbove j₀.succAbove).det =
    ((-1) ^ (↑i₀ + ↑j₀) * ∑ j, M i₀ j) * (M.submatrix i₀.succAbove j₀.succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_4
inst✝¹ : Zero α
inst✝ : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
⊢ (A.map f).IsDiag

Tactic:
intro i j h
  simp [ha h, hf]

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

Goal state before:
pp: case mp.refine_3
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : (fromBlocks A B C D).IsDiag
i : n
j : m
⊢ C i j = 0 i j

Tactic:
exact h Sum.inr_ne_inl

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

Goal state before:
pp: 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)
this :
  Module.Free R (N 0 →ₗ[R] MultilinearMap R (fun i ↦ N i.succ) M₂) ∧
    Module.Finite R (N 0 →ₗ[R] MultilinearMap R (fun i ↦ N i.succ) M₂)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
cases this
      exact
        ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂).symm,
          Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂).symm⟩

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

Goal state before:
pp: n : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_4
inst✝ : CommRing R
A : Matrix n n R
h : ∀ (a b : R), (a - b) * A.det = 0 → a = b
x : R
eq : x * A.det = 0
⊢ (x - 0) * A.det = 0

Tactic:
simpa

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

Goal state before:
pp: n : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_4
inst✝ : CommRing R
A : Matrix n n R
h : ∀ (x : R), x * A.det = 0 → x = 0
a b : R
eq : (a - b) * A.det = 0
⊢ (a - b) * A.det = 0

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ Ai none none * detp s (Ai.submatrix some some) +
      ∑ k, Ai none (some k) * detp (-s) (Ai.submatrix some (Function.update some k none)) =
    ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D

Tactic:
add_comm

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ ∑ k, Ai none (some k) * detp (-s) (Ai.submatrix some (Function.update some k none)) +
      Ai none none * detp s (Ai.submatrix some some) =
    ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
⊢ (reindex R M (Equiv.subtypeNeSumPUnit i₀).symm) (⨂ₜ[R] (i : ι), m i) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)

Tactic:
reindex_tprod (R := R) (s := M),

Goal state after:
R : Type u_1
ι : Type u_2
inst✝³ : DecidableEq ι
M : ι → Type u_3
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i₀ : ι
m : (i : ι) → M i
⊢ ((tprod R) fun i ↦ m ((Equiv.subtypeNeSumPUnit i₀).symm.symm i)) =
    (tprod R) fun j ↦ m ((Equiv.subtypeNeSumPUnit i₀) j)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: 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) = ⊤
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) :=
  equivPiTensorComplSingletonTensor R M i₀ ≪≫ₗ TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀)
ψ ψ' : M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) →ₗ[R] N
h :
  ∀ (j : (i : ι) → γ i),
    ψ
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i)))) =
      ψ'
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i))))
g₀ : γ i₀
⊢ Nat.card ι = n + {i₀}.ncard

Tactic:
simpa

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✝
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
⊢ Module.finrank k V = Module.finrank k (Fin n → k)

Tactic:
simpa

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

Goal state before:
pp: case 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
⊢ Independent f → iSupIndep fun i ↦ (f i).submodule

Tactic:
rintro ⟨f, hf, hi⟩
    simp only [submodule_mk]
    exact (iSupIndep_iff_linearIndependent_of_ne_zero (R := K) hf).mpr hi

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
⊢ IsCollinear ∅

Tactic:
IsCollinear_iff_rank

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ β • v + α • v = α • v + β • v

Tactic:
add_comm

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
w : ι → F
α : F
hα : α • v = A • w - w
β : F
hβ : β • v = B • w - w
⊢ α • v + β • v = α • v + β • v
Module: Mathlib.LinearAlgebra.Quotient.Bilinear

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ n ∈ (M'.liftQ f hM').flip.ker

Tactic:
simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
hwu : ∀ (i : ι), w i / |↑(u i)| = ↑(sign (w i))
v : ι → ℝ
⊢ (weightedSumSquares ℝ fun i ↦ ↑(sign (w i))) v =
    ((weightedSumSquares ℝ w).basisRepr ((Pi.basisFun ℝ ι).unitsSMul fun i ↦ Units.mk0 (1 / √|↑(u i)|) ⋯)) v

Tactic:
classical
  suffices ∑ i, (w i / |(u i : ℝ)|) * v i ^ 2 = ∑ i, w i * (v i ^ 2 * |(u i : ℝ)|⁻¹) by
    simpa [basisRepr_apply, Basis.unitsSMul_apply, ← _root_.sq, mul_pow, ← hwu, Pi.single_apply]
  exact sum_congr rfl fun j _ ↦ by ring

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

Goal state before:
pp: case e'_4
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : CommRing R
inst✝² : LinearOrder R
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Module R M'
Q' : QuadraticForm R M'
e : IsometryEquiv Q Q'
⊢ Module.finrank R M = Module.finrank R M'

Tactic:
· exact e.toLinearEquiv.finrank_eq

Goal state after:
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.pairingIn ℤ i k ≤ -2
⊢ P.root i + P.root k ≠ 0

Tactic:
add_comm

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.pairingIn ℤ i k ≤ -2
⊢ P.root k + P.root i ≠ 0
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 ι
⊢ cartanSubalgebra b = LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)

Tactic:
by
  refine le_antisymm LieSubalgebra.submodule_span_le_lieSpan ?_
  rw [LieSubalgebra.lieSpan_le, cartanSubalgebra]
  exact Submodule.subset_span

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✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
hi : h i ∈ lieAlgebra b
⊢ ⟨h i, hi⟩ ∈ cartanSubalgebra' b

Tactic:
simp [cartanSubalgebra']

Goal state after:
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
this : P.pairingIn ℤ k i ≤ 0
⊢ P.pairingIn ℤ k i = 0 ∨ P.pairingIn ℤ k i < 0 ∧ chainBotCoeff i k = 0

Tactic:
add_comm

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 i + P.root k ∈ 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.Semisimple

Goal state before:
pp: case neg.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 ι
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 : ι
hij : P.root l ≠ P.root ↑i + P.root k
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr l) = 0 (Sum.inr l)

Tactic:
simp [e, -indexNeg_neg, hij]

Goal state after: