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

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
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂) =
    e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)

Tactic:
by
                rw [mul_sub, add_mul, add_mul, ← Algebra.commutes, ← Algebra.smul_def, ← map_mul, ←
                  Algebra.smul_def, sub_add_eq_sub_sub, smul_mul_assoc, smul_mul_assoc]

Goal state after:
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
⊢ LinearIndependent R fun (x : ↑s) ↦ M'.mkQ ↑x

Tactic:
linearIndependent_iff',

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
⊢ ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • M'.mkQ ↑i = 0 → ∀ i ∈ s_1, 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
⊢ ringCon R A = (ringConGen (rel' R A)).comap (powerAlgebraEquivFreeTensorAlgebra R A).symm

Tactic:
ringCon,

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
⊢ ringConGen (rel R A) = (ringConGen (rel' R A)).comap (powerAlgebraEquivFreeTensorAlgebra R A).symm
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✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
nG : Submodule ℤ G := ((LinearMap.lsmul ℤ G) ↑n).range
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (Int.castAddHom (ZMod n)).toIntLinearMap
f : G →ₗ[ℤ] ι →₀ ℤ := ↑b.repr
hker : nG ≤ (mod ∘ₗ f).ker
g : H →ₗ[ℤ] ι →₀ ZMod n := nG.liftQ (mod ∘ₗ f) hker
this : ⇑mod ∘ ⇑b.repr = ⇑g ∘ ⇑nG.mkQ
⊢ Surjective ⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom)

Tactic:
exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp
        b.repr.surjective).of_comp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
i : ι
⊢ (basis b) i = (mkQ n) (b i)

Tactic:
Basis.apply_eq_iff

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : NeZero n
ι : Type u_4
b : Basis ι ℤ G
i : ι
⊢ (basis b).repr ((mkQ n) (b i)) = single i 1
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_5
n : Type u_6
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
i j : n
⊢ circulant (Pi.single 0 1) i j = 1 i j

Tactic:
simp [one_apply, Pi.single_apply, sub_eq_zero]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
i : { i // l i ≠ ⊤ }
⊢ ∀ ⦃j : { i // l i ≠ ⊤ }⦄, id j < id i → A.submatrix Subtype.val g i j = 0

Tactic:
j

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : LinearOrder m
inst✝² : LinearOrder n
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
l : m → WithTop n
hA : A.IsPivotedBy l
g : { i // l i ≠ ⊤ } → n := fun i ↦ (l ↑i).untop ⋯
hlead : ∀ (i : { i // l i ≠ ⊤ }), A.IsLeadingEntry (↑i) (g i)
i j : { i // l i ≠ ⊤ }
⊢ id j < id i → A.submatrix Subtype.val g i j = 0
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case 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
h_irr : A.IsIrreducible
i : n
⊢ ∀ (j : n), ∃ k > 0, 0 < (A ^ k) i j

Tactic:
j

Goal state after:
case 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
h_irr : A.IsIrreducible
i j : n
⊢ ∃ k > 0, 0 < (A ^ k) i j
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case mpr.connected
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
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
i : n
⊢ ∀ (j : n), ∃ p, 0 < p.length

Tactic:
j

Goal state after:
case mpr.connected
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
h_exists : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
i j : n
⊢ ∃ p, 0 < p.length
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : StarRing R
A : Matrix n n R
inst✝ : IsReduced R
hA : A.IsHadamard
hcard : ↑(Fintype.card n) ≠ 0
h : A.det = 0
⊢ ↑(Fintype.card n) ^ ?m.29 h = 0

Tactic:
by rw [← hA.det_mul_star_det, h, star_zero, zero_mul]

Goal state after:
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
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ A.map f i j = 0) i j

Tactic:
j

Goal state after:
α : 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
i j : n
⊢ i ≠ j → (fun i j ↦ A.map f i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A : Matrix n n α
ha : A.IsDiag
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ (-A) i j = 0) i j

Tactic:
j

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A : Matrix n n α
ha : A.IsDiag
i j : n
⊢ i ≠ j → (fun i j ↦ (-A) i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ (A + B) i j = 0) i j

Tactic:
j

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
⊢ i ≠ j → (fun i j ↦ (A + B) i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ (A - B) i j = 0) i j

Tactic:
j

Goal state after:
α : Type u_1
n : Type u_4
inst✝ : SubtractionMonoid α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
⊢ i ≠ j → (fun i j ↦ (A - B) i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: α : Type u_1
R : Type u_3
n : Type u_4
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
k : R
A : Matrix n n α
ha : A.IsDiag
i : n
⊢ ∀ ⦃j : n⦄, i ≠ j → (fun i j ↦ (k • A) i j = 0) i j

Tactic:
j

Goal state after:
α : Type u_1
R : Type u_3
n : Type u_4
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
k : R
A : Matrix n n α
ha : A.IsDiag
i j : n
⊢ i ≠ j → (fun i j ↦ (k • A) i j = 0) i j
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case cons
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
i j : n
this : Quiver n := A.toQuiver
b c : n
q : Path i b
e : b ⟶ c
ih : Path b i
eT : 0 < Aᵀ c b
⊢ Path c i

Tactic:
exact (@Quiver.Path.comp n (toQuiver Aᵀ) c b i (@Quiver.Hom.toPath n (toQuiver Aᵀ) c b
      (PLift.up eT)) ih)

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i : n
⊢ ∀ (j : n), ∃ p, 0 < p.length

Tactic:
j

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
⊢ ∃ p, 0 < p.length
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
σ : Perm n
M : Matrix n n R
⊢ Mᵀ.permanent = M.permanent

Tactic:
permanent_transpose

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
σ : Perm n
M : Matrix n n R
⊢ M.permanent = M.permanent
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
M : Matrix n n R
j : n
c : R
u : n → R
⊢ c * (M.updateRow j u)ᵀ.permanent = c * (M.updateRow j u).permanent

Tactic:
permanent_transpose

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ c * (M.updateRow j u).permanent = c * (M.updateRow j u).permanent
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: case a
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
p : (a : ι) → κ a
a✝ : p ∈ Fintype.piFinset fun i ↦ Finset.univ
h :
  ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) x =
      (g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) x
⊢ (f fun i ↦ Pi.single (p i) (x i (p i))) = g fun i ↦ Pi.single (p i) (x i (p i))

Tactic:
exact h _ _

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

Goal state before:
pp: R : Type u_1
m✝ : Type u_2
n✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype m✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m✝
inst✝¹ : DecidableEq n✝
A : Matrix n✝ n✝ R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Function.Injective ⇑f
g : (Fin m → R) →ₗ[R] Fin n → R := LinearMap.pi fun i ↦ if h : ↑i < m then LinearMap.proj ⟨↑i, h⟩ else 0
hnm : m < n
x y : Fin m → R
eq : g x = g y
i : Fin m
⊢ x i = y i

Tactic:
simpa [g] using congr($eq ⟨i, i.prop.trans hnm⟩)

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

Goal state before:
pp: case succ.e_f
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) := ⋯
ψ ψ' : 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))))
⊢ (lift.equiv (RingHom.id R) (M i₀) (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) N).symm ψ =
    (lift.equiv (RingHom.id R) (M i₀) (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) N).symm ψ'

Tactic:
rw [Submodule.linearMap_eq_iff_of_span_eq_top _ _ (hg i₀)]

Goal state after:
case succ.e_f
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))))
⊢ ∀ (s : ↑(Set.range g)),
    ((lift.equiv (RingHom.id R) (M i₀) (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) N).symm ψ) ↑s =
      ((lift.equiv (RingHom.id R) (M i₀) (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) N).symm ψ') ↑s
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
⊢ (fun s ↦
        { carrier := {x | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯, zero_mem' := ⋯,
          smul_mem' := ⋯ })
      ((fun s ↦ { carrier := Set.ofPred (Projectivization.lift (fun x ↦ ↑x ∈ s) ⋯), mem_add' := ⋯ }) s) =
    s

Tactic:
by
    ext x
    suffices x = 0 → x ∈ s by
      simpa [imp_iff_not_or]
    rintro rfl
    exact s.zero_mem

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
u v : V
hu : u ≠ 0
hv : v ≠ 0
huv : LinearIndependent K ![u, v]
p : Submodule K V
hp1 : Module.finrank K ↥p = 2
x : V
hx : x ∈ {u, v}
hp2 : u ∈ p
hp3 : v ∈ p
⊢ x ∈ ↑p

Tactic:
refine hx.casesOn ?_ ?_ <;> simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this✝ : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R :=
  (Matrix.SpecialLinearGroup.toLin_equiv b).symm
r : R
hr : r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1
this : ↑((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) = Matrix.of fun i j ↦ (b.repr ((fun x ↦ ↑g x) (b j))) i
i : Module.Free.ChooseBasisIndex R V
⊢ ∀ (b_1 : Module.Free.ChooseBasisIndex R V),
    Matrix.diagonal (fun x ↦ r) i b_1 = (b.repr (↑g (b b_1))) i ↔
      (LinearMap.toMatrix b b) (↑↑g) i b_1 = (LinearMap.toMatrix b b) (r • LinearMap.id) i b_1

Tactic:
j

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this✝ : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R :=
  (Matrix.SpecialLinearGroup.toLin_equiv b).symm
r : R
hr : r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1
this : ↑((Matrix.SpecialLinearGroup.toLin_equiv b).symm g) = Matrix.of fun i j ↦ (b.repr ((fun x ↦ ↑g x) (b j))) i
i j : Module.Free.ChooseBasisIndex R V
⊢ Matrix.diagonal (fun x ↦ r) i j = (b.repr (↑g (b j))) i ↔
    (LinearMap.toMatrix b b) (↑↑g) i j = (LinearMap.toMatrix b b) (r • LinearMap.id) i j
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ IsUnit (LinearMap.det (↑↑r • LinearMap.id))

Tactic:
by
    simp [LinearMap.det_smul, IsUnit.pow]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inl
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = Module.finrank R V
h' : 1 ≤ Module.finrank R V
⊢ ↑↑r ^ Module.finrank R V = 1

pp: case inr
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1

Tactic:
· simp_rw [h] at this
      exact this

Goal state after:
case inr
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
this : ↑↑r ^ max (Module.finrank R V) 1 = 1
h : max (Module.finrank R V) 1 = 1
h' : Module.finrank R V < 1
⊢ ↑↑r ^ Module.finrank R V = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ (bm.repr x).support.offDiag,
        if x_1.1 < x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • polar (⇑Q) (bm x_1.1) (bm x_1.2) else 0) =
    Q (∑ a ∈ (bm.repr x).support, (bm.repr x) a • bm a)

pp: case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2

Tactic:
QuadraticMap.map_sum,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ (∑ x_1 ∈ (bm.repr x).support, (bm.repr x) x_1 • (bm.repr x) x_1 • Q (bm x_1) +
      ∑ x_1 ∈ (bm.repr x).support.offDiag,
        if x_1.1 < x_1.2 then (bm.repr x) x_1.1 • (bm.repr x) x_1.2 • polar (⇑Q) (bm x_1.1) (bm x_1.2) else 0) =
    ∑ i ∈ (bm.repr x).support, Q ((bm.repr x) i • bm i) +
      ∑ ij ∈ (bm.repr x).support.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map (fun a ↦ (bm.repr x) a • bm a) ij)

case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ ∀ x_1 ∈ (bm.repr x).support.offDiag, ¬x_1.1 = x_1.2
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
r : ↥(rootsOfUnity (max (Module.finrank R V) 1) R)
⊢ ↑↑↑(centerEquivRootsOfUnity.symm r) = r • LinearMap.id

Tactic:
by
  simp only [centerEquivRootsOfUnity, MulEquiv.symm_mk, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk,
    centerEquivRootsOfUnity_invFun, LinearMap.coe_equivOfIsUnitDet]
  congr

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

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

Tactic:
QuadraticMap.map_add Q m' (m - m'),

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup P
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
⊢ Q m' + Q (m - m') + polar (⇑Q) m' (m - m') = Q m'
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 ι
⊢ span R (range h) ≤ (Matrix.diagonalLinearMap (↥b.support ⊕ ι) R R).range

Tactic:
by
  rw [span_le]
  rintro - ⟨i, rfl⟩
  rw [h_eq_diagonal]
  exact LinearMap.mem_range_self _ _

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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : x ∈ span R (range h)
⊢ x j (Sum.inl i) = 0

Tactic:
induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]

Goal state after: