mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono (↾⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))) ↔ Mono (↾⇑(ConcreteCategory.hom f))

Tactic:
apply (MorphismProperty.monomorphisms (Type w)).arrow_mk_iso_iff

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Arrow.mk (↾⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))) ≅ Arrow.mk (↾⇑(ConcreteCategory.hom f))
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
S : ShortComplex (ModuleCat R')
h : S.Exact
⊢ (S.map (restrictScalars f)).Exact

Tactic:
rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact] at h ⊢
  exact h

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : ComposableArrows C 0
φ φ' : F ⟶ G
h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1
⊢ φ = φ'

Tactic:
ext i
  fin_cases i
  exact h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
⊢ IsConnected (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)

Tactic:
refine IsConnected.of_induct (j₀ := StructuredArrow.mk (Y := one) (𝟙 _)) ?_

Goal state after:
case zero
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (p : Set (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)),
    StructuredArrow.mk (𝟙 WalkingReflexivePair.zero) ∈ p →
      (∀ {j₁ j₂ : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair} (x : j₁ ⟶ j₂),
          j₁ ∈ p ↔ j₂ ∈ p) →
        ∀ (j : StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair), j ∈ p
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ ∀ (X : Fin (n + 1 + 1)), (isoMkSucc (eqToIso h₀) (eqToIso h) ⋯).hom.app X = eqToHom ⋯

Tactic:
rintro ⟨_ | _, hi⟩ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ (limit.cone F).pt ≅ ((monadicLeftAdjoint R).mapCone c).pt

Tactic:
apply (asIso ((monadicAdjunction R).counit.app _)).symm.trans

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := ⋯
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ (R ⋙ monadicLeftAdjoint R).obj (limit.cone F).1 ≅ ((monadicLeftAdjoint R).mapCone c).pt
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : CommSemiring Rp
inst✝⁵ : Algebra R Rp
inst✝⁴ : AddCommMonoid Mp
inst✝³ : Module R Mp
inst✝² : Module Rp Mp
inst✝¹ : IsScalarTower R Rp Mp
inst✝ : Flat R M
S : Submonoid R
⊢ IsLocalizedModule S (LocalizedModule.mkLinearMap S M)

Tactic:
exact localizedModuleIsLocalizedModule S

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun x ↦ (a + b) • x) x ∈ a • s + b • s

Tactic:
simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x)) ↔ IsUnit ((mk I) x)

Tactic:
← isUnit_map_iff (DoubleQuot.quotQuotEquivQuotOfLE (Ideal.pow_le_self hn))

Goal state after:
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((DoubleQuot.quotQuotEquivQuotOfLE ⋯) ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x))) ↔ IsUnit ((mk I) x)
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ 1 = (Ideal.Quotient.mk I) (mk' S m ⟨m, hm⟩)

Tactic:
mk'_self,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : IsField (R ⧸ Ideal.under R I)
r m : R
hm : m ∈ M
hM : ¬(Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
rn : R
hn :
  (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m) *
      (Ideal.quotientMap I (algebraMap R S) ⋯) ((Ideal.Quotient.mk (Ideal.under R I)) rn) =
    1
⊢ 1 = (Ideal.Quotient.mk I) 1
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommRing R
S : Type u_2
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDomain R
inst✝¹² : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹¹ : CommRing Rₚ
inst✝¹⁰ : IsDomain Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R Rₚ
inst✝⁷ : Algebra R Sₚ
inst✝⁶ : Algebra S Sₚ
inst✝⁵ : Algebra Rₚ Sₚ
inst✝⁴ : IsScalarTower R S Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst✝² : IsLocalization M Rₚ
inst✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst✝ : Module.IsTorsionFree R S
e : Algebra.algebraMapSubmonoid S M ≤ S⁰
this✝ : IsDomain Sₚ
this : algebraMap Rₚ Sₚ = map Sₚ (algebraMap R S) ⋯
x : R
s : ↥M
a : R
ha : a ∈ ↑M
H : a * x = 0
⊢ ∃ a ∈ M, a * x = 0

Tactic:
exact ⟨a, ha, H⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ (algebraMap R S) ↑s * ↑⟨x, ⋯⟩ ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Tactic:
rw [mul_comm, Subtype.coe_mk, e]

Goal state after:
case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ (algebraMap R S) (y, s).1 ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr.exists_of_eq
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : ↥(adjoin R ↑σ)
e : (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
exact ⟨1, by simpa using Subtype.ext e⟩

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
use ∅

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : S), ∃ t ∈ adjoin R ↑∅, IsUnit t ∧ s * t ∈ adjoin R ↑∅
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: 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✝
I : Ideal R
hI : I.IsPrime
A : Type u_4
B : Type u_5
C : Type u_6
inst✝²¹ : CommSemiring A
inst✝²⁰ : CommSemiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : IsScalarTower R A B
inst✝¹⁵ : CommSemiring C
inst✝¹⁴ : Algebra A C
inst✝¹³ : Algebra B C
inst✝¹² : IsScalarTower A B C
p : Ideal A
inst✝¹¹ : p.IsPrime
P : Ideal B
inst✝¹⁰ : P.IsPrime
inst✝⁹ : P.LiesOver p
Q : Ideal C
inst✝⁸ : Q.IsPrime
inst✝⁷ : Q.LiesOver P
inst✝⁶ : Q.LiesOver p
inst✝⁵ : Algebra (Localization.AtPrime p) (Localization.AtPrime P)
inst✝⁴ : IsLiesOverAlgebra p P
inst✝³ : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)
inst✝² : IsLiesOverAlgebra P Q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime Q)
inst✝ : IsLiesOverAlgebra p Q
⊢ algebraMap (Localization.AtPrime p) (Localization.AtPrime Q) =
    (algebraMap (Localization.AtPrime P) (Localization.AtPrime Q)).comp
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime P))

Tactic:
simp [IsLiesOverAlgebra.algebraMap_eq, ← localRingHom_comp, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
i j✝ j : n
⊢ Pi.single i 1 j = 1 j i

Tactic:
rw [Matrix.one_eq_pi_single, Pi.single_comm]

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

Goal state before:
pp: n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ (cramer 0 ∘ₗ LinearMap.single α (fun i ↦ α) i) 1 j = (0 ∘ₗ LinearMap.single α (fun i ↦ α) i) 1 j

Tactic:
apply det_eq_zero_of_column_eq_zero j'

Goal state after:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), updateCol 0 j ((LinearMap.single α (fun i ↦ α) i) 1) i_1 j' = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ (Aᵀ.det • 1)ᵀ = A.det • 1

Tactic:
det_transpose,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ (A.det • 1)ᵀ = A.det • 1
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ adjugate 0 i j = 0 i j

Tactic:
apply det_eq_zero_of_column_eq_zero j'

Goal state after:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), 0ᵀ.updateCol j (Pi.single i 1) i_1 j' = 0
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
R : Type u_6
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * N * ↑M⁻¹).trace = N.trace

Tactic:
by
  rw [trace_mul_cycle, Units.inv_mul, one_mul]

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

Goal state before:
pp: case mk
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
⊢ ∑ j, (-1) ^ (↑(e i) + ↑j) * A' (e i) j * (A'.submatrix (e i).succAbove j.succAbove).det =
    ∑ j, A' (e i) j * A'.adjugate j (e i)

Tactic:
simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]

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

Goal state before:
pp: case succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n' : ℕ
h_card : Fintype.card n = n' + 1
⊢ A.adjugate.adjugate = A.det ^ (n' + 1 - 2) • A

Tactic:
cases n'

Goal state after:
case succ.zero
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
h_card : Fintype.card n = 0 + 1
⊢ A.adjugate.adjugate = A.det ^ (0 + 1 - 2) • A

case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
⊢ A.adjugate.adjugate = A.det ^ (n✝ + 1 + 1 - 2) • A
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 α)ˣ
⊢ ↑A⁻¹ = (↑A)⁻¹

Tactic:
let := A.invertible
  rw [← invOf_eq_nonsing_inv, invOf_units]

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 α
⊢ A.det⁻¹ʳ • A.adjugateᵀ = Aᵀ.det⁻¹ʳ • Aᵀ.adjugate

Tactic:
det_transpose,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A.det⁻¹ʳ • A.adjugateᵀ = A.det⁻¹ʳ • Aᵀ.adjugate
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
⊢ (single i j c).BlockTriangular b

Tactic:
intro r s hrs

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
r s : m
hrs : b s < b r
⊢ single i j c r s = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: m : Type u_3
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
M : Matrix m m R
p q : m → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : ∀ (x : m), q x ↔ p x
⊢ (M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det

Tactic:
convert!
    Matrix.det_reindex_self (Equiv.subtypeEquivRight e)
      (toSquareBlockProp M q)

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 α
⊢ IsUnit A⁻¹.det ↔ IsUnit A.det

Tactic:
isUnit_nonsing_inv_det_iff

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 B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ IsUnit A⁻¹.det

Tactic:
isUnit_nonsing_inv_det_iff

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ IsUnit A.det
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
⊢ ⅟(diagonal v) = diagonal ⅟v

Tactic:
@Invertible.congr _ _ _ _ _ (diagonalInvertible v) rfl

Goal state after:
n : Type u'
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
⊢ ⅟(diagonal v) = diagonal ⅟v
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
let k := (univ.image b).max' (univ_nonempty.image _)

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
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 α
Xs : List (Matrix n n α)
⊢ (A :: Xs).prod⁻¹ = (List.map Inv.inv (Xs.reverse.concat A)).prod

Tactic:
List.map_concat,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
Xs : List (Matrix n n α)
⊢ (A :: Xs).prod⁻¹ = ((List.map Inv.inv Xs.reverse).concat A⁻¹).prod
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (A.submatrix ⇑e₁ ⇑e₂)
⊢ (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁

Tactic:
simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this,
      submatrix_zero, Pi.zero_apply]

Goal state after:
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
⊢ M⁻¹ i j = 0

Tactic:
let k := (univ.image b).max' (univ_nonempty.image _)

Goal state after:
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' ⋯
⊢ M⁻¹ i j = 0
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ matPolyEquiv.symm (C M) = M.map ⇑C

Tactic:
by
  simp [matPolyEquiv]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

Tactic:
by_cases h : i = j

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j

case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (M.charmatrix i j).coeff k = (X.coeff k - (C M).coeff k) i j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ (-C (M i j)).coeff k = ((if 1 = k then 1 else 0) - (C M).coeff k) i j

Tactic:
coeff_neg,

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
i j : n
h : ¬i = j
⊢ -(C (M i j)).coeff k = ((if 1 = k then 1 else 0) - (C M).coeff k) i j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

Tactic:
by_cases h : i = j

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : i = j
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

case neg
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : ¬i = j
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n✝ : ℕ
⊢ ((M.map ⇑f).charmatrix i j).coeff n✝ = (M.charmatrix.map (Polynomial.map f) i j).coeff n✝

Tactic:
by_cases h : i = j

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n✝ : ℕ
h : i = j
⊢ ((M.map ⇑f).charmatrix i j).coeff n✝ = (M.charmatrix.map (Polynomial.map f) i j).coeff n✝

case neg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n✝ : ℕ
h : ¬i = j
⊢ ((M.map ⇑f).charmatrix i j).coeff n✝ = (M.charmatrix.map (Polynomial.map f) i j).coeff n✝