mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case h
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ (Ideal.Quotient.mk p) x * ((Ideal.Quotient.mk p) ↑s * ((Ideal.Quotient.mk p) ↑s)⁻¹) - (Ideal.Quotient.mk p) x = 0

Tactic:
mul_inv_cancel₀,

Goal state after:
case h
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ (Ideal.Quotient.mk p) x * 1 - (Ideal.Quotient.mk p) x = 0

case h
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ (Ideal.Quotient.mk p) ↑s ≠ 0
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
refine ⟨y, hy, z, ?_⟩

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ x = mk' S y z
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R S A
M : Submonoid S
inst✝² : IsLocalization M A
inst✝¹ : FaithfulSMul S A
s : Finset A
hs : LinearIndepOn R id ↑s
inst✝ : DecidableEq S
⊢ LinearIndepOn R id ↑(finsetIntegerMultiple M s)

Tactic:
rw [← LinearIndepOn.id_image_algebraMap_iff (A := A),
    finsetIntegerMultiple_image, ← s.coe_smul_finset]
  rw [linearIndepOn_finset_iff] at hs ⊢
  intro f h
  rw [s.smul_finset_def, s.forall_mem_image]
  apply hs
  have inj := (IsLocalization.smul_bijective A (commonDenomOfFinset M s)).injective
  rw [← inj.eq_iff, smul_zero, s.smul_sum, ← h, s.smul_finset_def, s.sum_image inj.injOn]
  exact s.sum_congr rfl fun x hx ↦ smul_comm ..

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

Goal state before:
pp: case pos
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : i = σ j
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
congr
    ext j'
    subst h
    have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff
    rw [updateRow_apply, updateCol_apply]
    simp_rw [this]
    rw [← dite_eq_ite, ← dite_eq_ite]
    congr 1 with rfl
    rw [Pi.single_eq_same, Pi.single_eq_same]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (T n).degree = ↑n

Tactic:
← one_mul (T n),

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (1 * T n).degree = ↑n
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
⊢ (List.map toMatrix (t :: L)).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod = 1

Tactic:
suffices
      t.toMatrix *
            ((L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod) *
          t.inv.toMatrix = 1
      by simpa [Matrix.mul_assoc]
    simp_rw [IH, Matrix.mul_one, t.mul_inv]

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

Goal state before:
pp: α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A.adjugate i j =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j

Tactic:
adjugate_fin_succ_eq_det_submatrix,

Goal state after:
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ Aᵀ * (⅟A)ᵀ = 1

Tactic:
by rw [← transpose_mul, invOf_mul_self, transpose_one]

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

Goal state before:
pp: case «0».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

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

Goal state before:
pp: case «0».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Goal state after:
case «0».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 0 2 * A 2 1 - A 0 1 * A 2 2 = -(A 0 1 * A 2 2) + A 0 2 * A 2 1
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case «0».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨2, ⋯⟩) + ↑((fun i ↦ i) ⟨0, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨0, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

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

Goal state before:
pp: case «1».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Goal state after:
case «1».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A 1 2 * A 2 0 - A 1 0 * A 2 2 = -(A 1 0 * A 2 2) + A 1 2 * A 2 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case «1».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

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

Goal state before:
pp: case «1».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨2, ⋯⟩) + ↑((fun i ↦ i) ⟨1, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨1, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Goal state after:
case «1».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 3 * (A 0 0 * A 1 2 - A 0 2 * A 1 0) = -(A 0 0 * A 1 2) + A 0 2 * A 1 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case «2».«0»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨0, ⋯⟩) + ↑((fun i ↦ i) ⟨2, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨0, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

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

Goal state before:
pp: case «2».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨1, ⋯⟩) + ↑((fun i ↦ i) ⟨2, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨1, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Goal state after:
case «2».«1»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 3 * (A 0 0 * A 2 1 - A 0 1 * A 2 0) = -(A 0 0 * A 2 1) + A 0 1 * A 2 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case «2».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ (↑((fun i ↦ i) ⟨2, ⋯⟩) + ↑((fun i ↦ i) ⟨2, ⋯⟩)) *
      (A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 0 *
          A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 1 -
        A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 0 1 *
          A.submatrix ((fun i ↦ i) ⟨2, ⋯⟩).succAbove ((fun i ↦ i) ⟨2, ⋯⟩).succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [Fin.succAbove, Fin.lt_def]

Goal state after:
case «2».«2»
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ (-1) ^ 4 * (A 0 0 * A 1 1 - A 0 1 * A 1 0) = A 0 0 * A 1 1 - A 0 1 * A 1 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ A.det • (B * 1) = A.det • (C * 1)

Tactic:
← Matrix.mul_smul,

Goal state after:
case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ B * A.det • 1 = A.det • (C * 1)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ B * A.det • 1 = A.det • (C * 1)

Tactic:
← Matrix.mul_smul,

Goal state after:
case right
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : B * A = C * A
⊢ B * A.det • 1 = C * A.det • 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : LT α
S : Type u_9
F : Type u_10
inst✝³ : FunLike F R S
inst✝² : Zero R
inst✝¹ : Zero S
inst✝ : ZeroHomClass F R S
f : F
h : M.BlockTriangular b
i j : m
lt : b j < b i
⊢ M.map (⇑f) i j = 0

Tactic:
simp [h lt]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
b : m → α
inst✝¹ : LT α
inst✝ : Zero R
M : Matrix m m (Matrix n n R)
h : M.BlockTriangular b
i j : m × n
lt : (fun i ↦ b i.1) j < (fun i ↦ b i.1) i
⊢ (Matrix.comp m m n n R) M i j = 0

Tactic:
simp [h lt]

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A.adjugate⁻¹ = h.unit⁻¹ • A

Tactic:
refine inv_eq_left_inv ?_
  rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]

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

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
a : α
x✝ : a ∈ univ
ha : a ∉ image b univ
⊢ (M.toSquareBlock b a).det = 1

Tactic:
have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
a : α
x✝ : a ∈ univ
ha : a ∉ image b univ
this : IsEmpty { i // b i = a }
⊢ (M.toSquareBlock b a).det = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
⊢ M⁻¹ i j = 0

Tactic:
obtain hbi | hi : b i = k ∨ _ := (le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt

Goal state after:
case H.inl
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hbi : b i = k
⊢ M⁻¹ i j = 0

case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hi : b i < (image b univ).max' ⋯
⊢ M⁻¹ i j = 0
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R), (matPolyEquiv (single i j ((monomial n_1) a))).coeff k = single i j (((monomial n_1) a).coeff k)

Tactic:
intro k x
    simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]
    split_ifs <;>
      · funext
        simp

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this : fromBlocks A 0 C D * ⅟(fromBlocks A 0 C D) = 1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1

Tactic:
← fromBlocks_toBlocks (⅟(fromBlocks A 0 C D)),

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks A 0 C D *
      fromBlocks (⅟(fromBlocks A 0 C D)).toBlocks₁₁ (⅟(fromBlocks A 0 C D)).toBlocks₁₂
        (⅟(fromBlocks A 0 C D)).toBlocks₂₁ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ =
    1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1