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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hcomm : ∀ (i j : ι) (r : R), i ≠ j → Commute f ((b.coord i).transvection (r • b j))
⊢ ∃ a, f = a • 1

Tactic:
simp only [SetLike.exists, Subring.mem_center_iff]
  rcases subsingleton_or_nontrivial V with hV | hV
  · refine ⟨1, by simp, ?_⟩
    ext x
    simp [Subring.smul_def, hV.allEq (f x) x]
  simp only [commute_iff_eq] at hcomm
  replace hcomm (i j : ι) (hij : i ≠ j) (r : R) :
      r • f (b j) = b.coord i (f (b i)) • r • b j := by
    have := hcomm i j r hij
    rw [LinearMap.ext_iff] at this
    simpa [LinearMap.transvection.apply] using this (b i)
  have h_allEq (i j : ι) : b.coord i (f (b i)) = b.coord j (f (b j)) := by
    by_cases hij : j = i
    · simp [hij]
    simpa using congr_arg (b.coord i) (hcomm j i hij 1)
  replace hcomm (i : ι) (r : R) : r • f (b i) = b.coord i (f (b i)) • r • b i := by
    obtain ⟨j, hji⟩ := exists_ne i
    simpa [h_allEq j i] using hcomm j i hji r
  let i : ι := Classical.ofNonempty
  refine ⟨b.coord i (f (b i)), fun r ↦ by simpa using congr(b.coord i $(hcomm i r)), ?_⟩
  ext x
  rw [← b.linearCombination_repr x, linearCombination_apply, map_finsuppSum]
  simp only [smul_apply, End.one_apply, smul_sum]
  apply sum_congr
  intro j _
  simp [Subring.smul_def, h_allEq i j, hcomm j]

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

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ y * x₁ + x₂ * y = y * x₁ + y * x₂

Tactic:
hx₂

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
y x₁ x₂ : CliffordAlgebra 0
hx₁ : x₁ * y = y * x₁
hx₂ : x₂ * y = y * x₂
⊢ y * x₁ + y * x₂ = y * x₁ + y * x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case mul
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ * reverse x₂ = x₁ * x₂

Tactic:
hx₂

Goal state after:
case mul
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ * x₂ = x₁ * x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ + reverse x₂ = x₁ + x₂

Tactic:
hx₂

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
x₁ x₂ : CliffordAlgebra 0
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ + x₂ = x₁ + x₂
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
hv : ¬v = 0
hf : ¬f = 0
ι : Set V
b : Basis (↑ι) K V
i j : ↑ι
hi : i ≠ j
hj : v = b i ∧ f = b.coord j
this : Fintype ↑ι
x y : ↑ι
h : ¬x = y
⊢ (Finsupp.single y 1) x = 1 x y

Tactic:
rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]

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

Goal state before:
pp: case mul
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ * reverse x₂ = x₁ * x₂

Tactic:
hx₂

Goal state after:
case mul
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ * x₂ = x₁ * x₂
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: case add
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ + reverse x₂ = x₁ + x₂

Tactic:
hx₂

Goal state after:
case add
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ x₁ + x₂ = x₁ + x₂
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)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ (TensorProduct.directSum R R ℬ 𝒜).symm
      ((gradedCommAux R 𝒜 ℬ) ((TensorProduct.directSum R R 𝒜 ℬ) ((lof R ι 𝒜 i) a ⊗ₜ[R] (lof R ι ℬ j) b))) =
    (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a

Tactic:
TensorProduct.directSum_lof_tmul_lof,

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)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ (TensorProduct.directSum R R ℬ 𝒜).symm
      ((gradedCommAux R 𝒜 ℬ) ((lof R (ι × ι) (fun i ↦ 𝒜 i.1 ⊗[R] ℬ i.2) (i, j)) (a ⊗ₜ[R] b))) =
    (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a
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 ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ ((gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) ((lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b) =
    r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b

Tactic:
erw [tmul_of_gradedMul_of_tmul]

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 ℬ
r : R
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
ia : ι
a : 𝒜 ia
ib : ι
b : ℬ ib
⊢ (-1) ^ (0 * ia) •
      ((algebraMap R (DirectSum ι 𝒜)) r * (lof R ι 𝒜 ia) a) ⊗ₜ[R]
        ((lof R ι ℬ 0) GradedMonoid.GOne.one * (lof R ι ℬ ib) b) =
    r • (lof R ι 𝒜 ia) a ⊗ₜ[R] (lof R ι ℬ ib) b
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✝
⊢ ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝)) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) =
    r • (lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝

Tactic:
erw [tmul_of_gradedMul_of_tmul]

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✝
⊢ (-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✝
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e'_3
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
b₂ : B
⊢ a₁ = a₁ * ↑GradedMonoid.GOne.one

Tactic:
rw [SetLike.coe_gOne, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: case e'_3.e'_16
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
a₁ : A
b₂ : B
⊢ a₁ = a₁ * ↑GradedMonoid.GOne.one

Tactic:
rw [SetLike.coe_gOne, mul_one]

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
inst✝¹ : AddCommGroup G
n : ℕ
inst✝ : AddMonoid M
f : ModN G n →+ M
⊢ (fun φ ↦ QuotientAddGroup.lift ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup ↑φ ⋯)
      ((fun f ↦ ⟨f.comp (QuotientAddGroup.mk' ((LinearMap.lsmul ℤ G) ↑n).range.toAddSubgroup), ⋯⟩) f) =
    f

Tactic:
by
    ext x
    induction x using QuotientAddGroup.induction_on
    rfl

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) ((lof R I A i) 1) = 1

Tactic:
by
  suffices ι' R A (DirectSum.lof R I A i 1) = mkAlgHom R A 1 by simpa [← ι_apply]
  exact Quotient.sound <| RingCon.le_ringConGen _ _ <| rel_id R A (i := i)

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

Goal state before:
pp: case refine_2
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
⊢ Surjective ⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom)

Tactic:
suffices mod ∘ b.repr = g ∘ nG.mkQ by
      exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp
        b.repr.surjective).of_comp

Goal state after:
case refine_2
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
⊢ ⇑mod ∘ ⇑b.repr = ⇑g ∘ ⇑nG.mkQ
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h✝ : ¬a = i
h : i < a
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Tactic:
· rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]

Goal state after:
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) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
⊢ (M.submatrix j₁.succAbove id).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix j₂.succAbove id).det

Tactic:
by
  suffices ∀ j, (M.submatrix (Fin.succAbove j) id).det =
      Int.negOnePow j • (M.submatrix (Fin.succAbove 0) id).det by
    rw [this j₁, this j₂, smul_smul, ← Int.negOnePow_add, sub_add_cancel]
  intro j
  induction j using Fin.induction with
  | zero => rw [Fin.val_zero, Nat.cast_zero, Int.negOnePow_zero, one_smul]
  | succ i h_ind =>
      rw [Fin.val_succ, Nat.cast_add, Nat.cast_one, Int.negOnePow_succ, Units.neg_smul,
        ← neg_eq_iff_eq_neg, ← neg_one_smul R,
        ← det_updateRow_sum (M.submatrix i.succ.succAbove id) i (fun _ ↦ -1),
        ← Fin.val_castSucc i, ← h_ind]
      congr
      ext a b
      simp_rw [neg_one_smul, updateRow_apply, Finset.sum_neg_distrib, Pi.neg_apply,
        Finset.sum_apply, submatrix_apply, id_eq]
      split_ifs with h
      · replace hv := congr_fun hv b
        rw [Fin.sum_univ_succAbove _ i.succ, Pi.add_apply, Finset.sum_apply] at hv
        rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]
      · obtain h | h := ne_iff_lt_or_gt.mp h
        · rw [Fin.succAbove_castSucc_of_lt _ _ h,
            Fin.succAbove_of_succ_le _ _ (Fin.succ_lt_succ_iff.mpr h).le]
        · rw [Fin.succAbove_succ_of_lt _ _ h, Fin.succAbove_castSucc_of_le _ _ h.le]

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

Tactic:
by
  rw [← one_smul R M.det, ← Matrix.det_updateRow_sum _ i₀ (fun _ ↦ 1), Matrix.det_succ_row _ i₀]
  simp only [updateRow_apply, if_true, one_smul, submatrix_updateRow_succAbove, Finset.sum_apply]
  rw [Fintype.sum_eq_add_sum_subtype_ne _ j₀]
  conv_lhs =>
    enter [2, 2, i]
    rw [hv _ i.prop, mul_zero, zero_mul]
  simp [Finset.sum_const_zero, add_zero]

Goal state after:
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:
induction n with

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 : ℕ
N : Fin n → Type u_5
inst✝³ : (i : Fin n) → AddCommGroup (N i)
inst✝² : (i : Fin n) → Module R (N i)
inst✝¹ : ∀ (i : Fin n), Module.Finite R (N i)
inst✝ : ∀ (i : Fin n), Module.Free R (N i)
⊢ Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ { toFun := fun x ↦ x • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
    x * { toFun := fun x ↦ x • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
    change mul _ _ = mul _ _
    rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply]
    change r • (1 * x) = r • (x * 1)
    rw [mul_one, one_mul]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)

Tactic:
rw [card k, Nat.mul_div_cancel]

Goal state after:
case H
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
⊢ 0 < Nat.card k - 1
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0

Tactic:
exact fun i => rep_nonzero (f i)

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Free R V
d1 : Module.finrank R V = 1
u✝ v : SpecialLinearGroup R V
a✝ : Nontrivial R
x✝ : V
hx : ¬x✝ = 0
u : SpecialLinearGroup R V
x : V
c : R := (LinearEquiv.smul_id_of_finrank_eq_one d1).symm ↑↑u
hc : (LinearEquiv.smul_id_of_finrank_eq_one d1) c = ↑↑u
hu : LinearEquiv.det ↑u = 1
⊢ c = 1

Tactic:
simpa [← Units.val_inj, LinearEquiv.coe_det, ← hc,
      LinearEquiv.smul_id_of_finrank_eq_one, d1] using hu

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

Goal state before:
pp: case h
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
x✝ : ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
v : ι → K
hv : v ≠ 0
⊢ r • v = ↑m • v

Tactic:
simp [← hr2]

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

Goal state before:
pp: case inr.inl
ι : 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
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i : ι
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm i) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm i)

pp: case inr.inr
ι : 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
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)

Tactic:
· simp [toBilin_apply]

Goal state after:
case inr.inr
ι : 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
bm : Basis ι R M
Q₁ Q₂ : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((Q₁ + Q₂).toBilin bm) (bm i)) (bm j) = ((Q₁.toBilin bm + Q₂.toBilin bm) (bm i)) (bm j)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: case inr.inl
ι : 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
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i : ι
⊢ (((s • Q).toBilin bm) (bm i)) (bm i) = ((s • Q.toBilin bm) (bm i)) (bm i)

pp: case inr.inr
ι : 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
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)

Tactic:
· simp [toBilin_apply]

Goal state after:
case inr.inr
ι : 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
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
bm : Basis ι R M
s : S
Q : QuadraticMap R M N
i j : ι
h : j < i
⊢ (((s • Q).toBilin bm) (bm i)) (bm j) = ((s • Q.toBilin bm) (bm i)) (bm j)
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : ¬Subsingleton V
hι : IsEmpty ι
⊢ Subsingleton V

Tactic:
by
      rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
⊢ (weightedSumSquares ℝ w).IsometryEquiv (weightedSumSquares ℝ fun i ↦ ↑(sign (w i)))

Tactic:
let u i := if h : w i = 0 then (1 : ℝˣ) else Units.mk0 (w i) h
  have hu : ∀ i : ι, 1 / √|(u i : ℝ)| ≠ 0 := fun i ↦
    have : (u i : ℝ) ≠ 0 := (u i).ne_zero
    by positivity
  have hwu : ∀ i, w i / |(u i : ℝ)| = sign (w i) := fun i ↦ by
    by_cases hi : w i = 0
    · simp [hi]
    · simp only [hi, ↓reduceDIte, Units.val_mk0, u]; field_simp; simp
  convert!
    QuadraticMap.isometryEquivBasisRepr (weightedSumSquares ℝ w)
      ((Pi.basisFun ℝ ι).unitsSMul fun i => .mk0 _ (hu i))
  ext1 v
  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: R : Type u_1
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : Module R M
Q : QuadraticForm R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
⊢ Module.finrank R ↥V ∈ Iic (Module.finrank R M) ∧
    ∃ V_1, Module.finrank R ↥V_1 = Module.finrank R ↥V ∧ (QuadraticMap.restrict Q V_1).PosDef

Tactic:
mem_Iic

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : Module R M
Q : QuadraticForm R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
⊢ Module.finrank R ↥V ≤ Module.finrank R M ∧
    ∃ V_1, Module.finrank R ↥V_1 = Module.finrank R ↥V ∧ (QuadraticMap.restrict Q V_1).PosDef
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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
aux₁ : LinearIndependent R ![P.root j, P.root i]
aux₂ : chainBotCoeff j i + chainTopCoeff j i ≤ 2
aux₃ : 1 ≤ chainTopCoeff j i
⊢ P.pairingIn ℤ i j ≤ 0

Tactic:
← P.chainBotCoeff_sub_chainTopCoeff aux₁

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : P.root i + P.root j ∈ Set.range ⇑P.root
aux₁ : LinearIndependent R ![P.root j, P.root i]
aux₂ : chainBotCoeff j i + chainTopCoeff j i ≤ 2
aux₃ : 1 ≤ chainTopCoeff j i
⊢ ↑(chainBotCoeff j i) - ↑(chainTopCoeff j i) ≤ 0