mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: 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 ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
f : A →ₐ[R] C
g : B →ₐ[R] C
h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)
⊢ ∀ (x y : 𝒜 ᵍ⊗[R] ℬ),
    (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) (x * y) =
      (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) x *
        (LinearMap.mul' R C ∘ₗ TensorProduct.map f.toLinearMap g.toLinearMap ∘ₗ ↑(of R 𝒜 ℬ).symm) y

Tactic:
rw [LinearMap.map_mul_iff]
      ext a₁ : 3
      refine DirectSum.decompose_lhom_ext ℬ fun j₁ => ?_
      ext b₁ : 3
      refine DirectSum.decompose_lhom_ext 𝒜 fun i₂ => ?_
      ext a₂ b₂ : 2
      dsimp
      rw [tmul_coe_mul_coe_tmul]
      rw [@Units.smul_def _ _ (_) (_), ← Int.cast_smul_eq_zsmul R, map_smul, map_smul, map_smul]
      rw [Int.cast_smul_eq_zsmul R, ← @Units.smul_def _ _ (_) (_)]
      rw [of_symm_of, map_tmul, LinearMap.mul'_apply]
      simp_rw [AlgHom.toLinearMap_apply, map_mul]
      simp_rw [mul_assoc (f a₁), ← mul_assoc _ _ (g b₂), h_anti_commutes, mul_smul_comm,
        smul_mul_assoc, smul_smul, Int.units_mul_self, one_smul]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
⊢ N.toAddSubgroup.index = Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
hNN'

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
⊢ N'.toAddSubgroup.index = Nat.card R ^ (Fintype.card ι - n) * ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
c : Fin n → R
i : ι
h : ∃ j, f j = i
⊢ (∑ x, c x • if i = f x then a x else 0) = c h.choose * if i = f h.choose then a h.choose else 0

Tactic:
by
              refine Finset.sum_eq_single h.choose ?_ (by simp)
              rintro j - hj
              have hinj := f.injective.ne hj
              rw [h.choose_spec] at hinj
              simp [hinj.symm]

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

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
⊢ (∑ x, if i = f x then ⋯.choose • a x else 0) = g i

Tactic:
by_cases! hj : ∃ j, f j = i

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∃ j, f j = i
⊢ (∑ x, if i = f x then ⋯.choose • a x else 0) = g i

case neg
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
hj : ∀ (j : Fin n), f j ≠ i
⊢ (∑ x, if i = f x then ⋯.choose • a x else 0) = g i
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
⊢ circulant v * circulant w = circulant (circulant v *ᵥ w)

Tactic:
by
  ext i j
  simp only [mul_apply, mulVec, circulant_apply, dotProduct]
  refine Fintype.sum_equiv (Equiv.subRight j) _ _ ?_
  intro x
  simp only [Equiv.subRight_apply, sub_sub_sub_cancel_right]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case succ.inl
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 : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ j,
      (-1) ^ (↑i + ↑j) * (A.fromRows B).submatrix f g i j *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove j.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
simp only [submatrix_apply, hfi, fromRows_apply_inr] at hAB

Goal state after:
case succ.inl
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 : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x, (-1) ^ (↑i + ↑x) * B j (g x) * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case neg
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
⊢ M (i.succ.succAbove a) b = M (i.castSucc.succAbove a) b

Tactic:
· 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.FreeModule.Int

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)

Tactic:
rcases snf with ⟨-, bN, -, -, -⟩

Goal state after:
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
⊢ n = Fintype.card ι ↔ Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
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 ⋯
⊢ #{i | l i ≠ ⊤} ≤ A.rank

Tactic:
have hlead : ∀ i : {i // l i ≠ ⊤}, A.IsLeadingEntry i.1 (g i) := fun i =>
    hA.isLeadingEntry (WithTop.coe_untop (l i.1) i.2).symm

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 | l i ≠ ⊤} ≤ A.rank
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 : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
⊢ (A.fromRows B).IsTotallyUnimodular

Tactic:
by
  intro k f g hf hg
  induction k with
  | zero => use 1; simp
  | succ k ih =>
    specialize hB ⟨g 0⟩
    -- Either `f` is `inr` somewhere or `inl` everywhere
    obtain ⟨i, j, hfi⟩ | ⟨f', rfl⟩ : (∃ i j, f i = .inr j) ∨ (∃ f', f = .inl ∘ f') := by
      simp_rw [← Sum.isRight_iff, or_iff_not_imp_left, not_exists, Bool.not_eq_true,
        Sum.isRight_eq_false, Sum.isLeft_iff]
      intro hfr
      choose f' hf' using hfr
      exact ⟨f', funext hf'⟩
    · have hAB := det_succ_row ((fromRows A B).submatrix f g) i
      simp only [submatrix_apply, hfi, fromRows_apply_inr] at hAB
      obtain ⟨j', s, hj'⟩ := hB j
      · simp only [hj'] at hAB
        by_cases hj'' : ∃ x, g x = j'
        · obtain ⟨x, rfl⟩ := hj''
          rw [Fintype.sum_eq_single x fun y hxy => ?_, Pi.single_eq_same] at hAB
          · rw [hAB]
            change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom
            refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
            · apply pow_mem
              exact ⟨-1, by simp⟩
            · exact ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)
          · simp [Pi.single_eq_of_ne, hg.ne_iff.mpr hxy]
        · rw [not_exists] at hj''
          use 0
          simpa [hj''] using hAB.symm
    · rw [isTotallyUnimodular_iff] at hA
      apply hA

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ (A.fromCols (replicateCol n' 0)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
by
  rw [← transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_replicateCol,
    fromRows_replicateRow0_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]

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

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
⊢ C A

Tactic:
have h_reduce : C (reduce A) := by
    rcases reduce_mem_reps hm A with ⟨H1, H2, H3, H4⟩
    exact h0 _ H1 H2 H3 H4

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ C A
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

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

Tactic:
by
    exact this.imp (fun a h ↦ by rwa [mem_closedBall_iff_norm', sub_zero] at h)

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

Goal state before:
pp: case neg
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
h1 : ¬0 < ↑A 0 0
⊢ C (reduce A) → C A

Tactic:
simp only [reduce_of_not_pos h h1, prop_red_T_pow hS hT, prop_red_S hS, imp_self]

Goal state after:
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
hA : A.IsHadamard
⊢ star A.det * A.det = ↑(Fintype.card n) ^ Fintype.card n

Tactic:
rw [mul_comm, hA.det_mul_star_det]

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
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
h_prim : A.IsPrimitive
⊢ A.IsIrreducible

Tactic:
by
  obtain ⟨h_nonneg, k, hk_pos, hk_all⟩ := h_prim
  rw [isIrreducible_iff_exists_pow_pos h_nonneg]
  aesop

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
h : P 0
⊢ a = b

Tactic:
by simpa [IsDetpBalanced] using h Fin.elim0 Fin.elim0

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
⊢ False

Tactic:
have hg : Function.Injective g := fun x y eq ↦ funext fun i ↦ by
      simpa [g] using congr($eq ⟨i, i.prop.trans hnm⟩)

Goal state after:
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
hg : Function.Injective ⇑g
⊢ False
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y z : ⨂[R] (i : ι), A i
⊢ (mul ((mul x) y)) z = (mul x) ((mul y) z)

Tactic:
by
  -- restate as an equality of morphisms so that we can use `ext`
  suffices LinearMap.llcomp R _ _ _ mul ∘ₗ mul =
      (LinearMap.llcomp R _ _ _ LinearMap.lflip.toLinearMap <|
        LinearMap.llcomp R _ _ _ mul.flip ∘ₗ mul).flip by
    exact DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this x) y) z
  ext x y z
  dsimp [← mul_def]
  simpa only [tprod_mul_tprod] using congr_arg (tprod R) (mul_assoc x y z)

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)

Tactic:
refine ⟨?_, fun h => ?_⟩
  · rintro ⟨ff, hff, hh1⟩
    contrapose hh1
    choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
    convert! hh1.units_smul a⁻¹
    ext i
    simp only [← ha, inv_smul_smul, Pi.smul_apply', Pi.inv_apply, Function.comp_apply]
  · convert! Dependent.mk _ _ h
    · simp only [mk_rep, Function.comp_apply]
    · exact fun i => rep_nonzero (f i)

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: case «0».«1»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

pp: case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
· exact Subgroup.mem_sup_left <| transvection_mem_lineStab zero_ne_one c

Goal state after:
case «1».«0»
F : Type u_2
inst✝ : Field F
c : F
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ SpecialLinearGroup.transvection hij c ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)
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 : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ ↑↑↑g = centerEquivRootsOfUnity g • LinearMap.id

Tactic:
simp only [centerEquivRootsOfUnity, Or.by_cases, MulEquiv.coe_mk, Equiv.coe_fn_mk,
    dite_smul, one_smul, Subgroup.mk_smul, Units.smul_isUnit, dite_eq_ite]
  split_ifs with hR hV
  · have : Subsingleton V := Module.subsingleton R V
    apply Subsingleton.eq_one
  · apply Subsingleton.eq_one
  · rw [not_subsingleton_iff_nontrivial] at hV
    rw [← (mem_center_iff.mp g.prop).choose_spec.2]

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

Goal state before:
pp: case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
i : ι
hi : ¬v i = 0
⊢ 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

Tactic:
have : i ∈ s := by
      contrapose hi
      exact Pi.mem_spanSubset_iff.mp hv i hi

Goal state after:
case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
i : ι
hi : ¬v i = 0
this : i ∈ s
⊢ 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case convert_8
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p : Set ι := {i | 0 < w i}
m : Set ι := {i | w i ≤ 0}
this : p.ncard + m.ncard = Nat.card ι
⊢ sigPos (weightedSumSquares 𝕜 w) = p.ncard

Tactic:
have : p.ncard ≤ sigPos (weightedSumSquares 𝕜 w) :=
    (sigPos_isGreatest _).2 ⟨Pi.spanSubset 𝕜 p, Pi.dim_spanSubset,
      posDef_spanSubset p (by grind)⟩

Goal state after:
case convert_8
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p : Set ι := {i | 0 < w i}
m : Set ι := {i | w i ≤ 0}
this✝ : p.ncard + m.ncard = Nat.card ι
this : p.ncard ≤ sigPos (weightedSumSquares 𝕜 w)
⊢ sigPos (weightedSumSquares 𝕜 w) = p.ncard
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i j k : ↥b.support
⊢ h i (Sum.inl j) (Sum.inl k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl j) (Sum.inl k)

Tactic:
simp [h, Matrix.diagonal_apply]

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

Goal state before:
pp: case inl.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i j : ↥b.support
k : ι
⊢ h i (Sum.inl j) (Sum.inr k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl j) (Sum.inr k)

Tactic:
simp [h, Matrix.diagonal_apply]

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

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
k : ↥b.support
⊢ h i (Sum.inr j) (Sum.inl k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inr j) (Sum.inl k)

Tactic:
simp [h, Matrix.diagonal_apply]

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

Goal state before:
pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i : ↥b.support
j k : ι
⊢ h i (Sum.inr j) (Sum.inr k) =
    Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inr j) (Sum.inr k)

Tactic:
simp [h, Matrix.diagonal_apply]

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

Goal state before:
pp: case inl.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : DecidableEq ι
i j k : ↥b.support
⊢ h i (Sum.inl j) (Sum.inl k) = Matrix.diagonal (0 ⊕ᵥ fun x ↦ ↑(P.pairingIn ℤ x ↑i)) (Sum.inl j) (Sum.inl k)

Tactic:
simp [h, Matrix.diagonal_apply]

Goal state after: