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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
x✝¹ : A
x✝ : M
⊢ { toFun := fun n ↦ Submodule.Quotient.mk ((x✝¹ • x✝) ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } =
    x✝¹ • { toFun := fun n ↦ Submodule.Quotient.mk (x✝ ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ Submodule.map (Algebra.linearMap R S) ⊥ = ⊥

Tactic:
Submodule.map_bot

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ ⊥ = ⊥
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set R
⊢ Submodule.span R (⇑(Algebra.linearMap R S) '' s) = Submodule.span R (⇑(algebraMap R S) '' s)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ Submodule.span R (⇑(algebraMap R S) '' {x}) = R ∙ (algebraMap R S) x

Tactic:
Set.image_singleton

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ R ∙ (algebraMap R S) x = R ∙ (algebraMap R S) x
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
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ₚ
inst✝ : p.IsMaximal
n : ℕ
x✝ : R
⊢ x✝ ∈ under R (maximalIdeal Rₚ ^ n) ↔ x✝ ∈ p ^ n

Tactic:
rw [mem_comap, ← map_eq_maximalIdeal p Rₚ, ← Ideal.map_pow,
    algebraMap_mem_map_algebraMap_iff p.primeCompl Rₚ]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
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ₚ
inst✝ : p.IsMaximal
n : ℕ
x✝ : R
⊢ (∃ m ∈ p.primeCompl, m * x✝ ∈ p ^ n) ↔ x✝ ∈ p ^ n
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
c u : B
⊢ ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
              (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
            Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
      (c • (Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) u) =
    c •
      ↑(tensorQuotEquivQuotSMul B I ≪≫ₗ
                (I • ⊤).quotEquivOfEq (Submodule.restrictScalars A (Ideal.map (algebraMap A B) I)) ⋯ ≪≫ₗ
              Submodule.Quotient.restrictScalarsEquiv A (Ideal.map (algebraMap A B) I)).symm
        ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) u)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
a₁ a₂ : A
b₁ b₂ : T
⊢ (((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
        (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯)
      (Submodule.Quotient.mk (a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂)) =
    (((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
          (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯)
        (Submodule.Quotient.mk (a₁ ⊗ₜ[R] b₁)) *
      (((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
          (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯)
        (Submodule.Quotient.mk (a₂ ⊗ₜ[R] b₂))

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.add
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : T ⊗[R] S
hx :
  ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ x * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy :
  ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ y * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ (x + y) * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
obtain ⟨tx, hx₁, hx₂, hx₃⟩ := hx
    obtain ⟨ty, hy₁, hy₂, hy₃⟩ := hy
    refine ⟨_, mul_mem hx₁ hy₁, hx₂.mul hy₂, ?_⟩
    rw [add_mul, ← mul_assoc, mul_comm tx ty, ← mul_assoc]
    exact add_mem (mul_mem hx₃ hy₁) (mul_mem hy₃ hx₁)

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ Nonempty (OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

Tactic:
by
  constructor
  · exact fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩
  · intro H
    choose r' s' h using H
    exact ⟨oreSetOfNoZeroDivisors r' s' h⟩

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := e.toRingHom.toAlgebra
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ e.toRingHom.comp f = (algebraMap S T).comp f

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this✝¹ : Algebra S T := ⋯
this✝ : IsLocalization.Away 1 R
this : IsLocalization.Away (f 1) T
⊢ (IsLocalization.Away.map R T f 1).comp (algebraMap R R) = IsLocalization.Away.map R T f 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Field

Goal state before:
pp: x✝ : IsField ℤ
exists_pair_ne✝ : ∃ x y, x ≠ y
mul_comm✝ : ∀ (x y : ℤ), x * y = y * x
h : ∀ {a : ℤ}, a ≠ 0 → ∃ b, a * b = 1
this : 2 ≠ 0 → ∃ b, 2 * b = 1
⊢ False

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
⊢ (A.map f).IsSymm

Tactic:
rw [IsSymm, ← transpose_map, h.eq]

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

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m (Matrix n n α)
⊢ (∀ (a : m) (b : n) (a_1 : m) (b_1 : n), A a_1 a b_1 b = A a a_1 b b_1) ↔
    ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ toLaurent (Polynomial.C r * X ^ n) = C r * T ↑n

Tactic:
simp only [map_mul, Polynomial.toLaurent_C, Polynomial.toLaurent_X_pow]

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

Goal state before:
pp: case C_mul_T
R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
s : R
⊢ AddMonoidAlgebra.single 0 (r * s) = C (r * s)

Tactic:
rfl

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

Goal state before:
pp: m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
⊢ (A.updateCol (e i) fun i ↦ b (e.symm i)).det = (A.updateCol (e i) (b ∘ ⇑e.symm)).det

Tactic:
Function.comp_def

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 α
r : α
A : Matrix n n α
⊢ (of fun i ↦ (r ^ (Fintype.card n - 1) • Aᵀ.cramer) (Pi.single i 1)) =
    r ^ (Fintype.card n - 1) • of fun i ↦ Aᵀ.cramer (Pi.single i 1)

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
⊢ f.smeval x = f.smeval x

Tactic:
rfl

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

Goal state before:
pp: R : Type u_6
inst✝ : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
i₁' : l
i₂' : n
j₁' : m
j₂' : p
⊢ f (if i₁ = i₁' ∧ j₁ = j₁' then a else 0) (if i₂ = i₂' ∧ j₂ = j₂' then b else 0) =
    if (i₁, i₂) = (i₁', i₂') ∧ (j₁, j₂) = (j₁', j₂') then f a b else 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
i₁ : l
i₂ : m
j₁ : l
j₂ : n
⊢ kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i ↦ B.map fun b ↦ f (a i) b) (i₁, i₂)
      (j₁, j₂)

Tactic:
simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf]

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

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
i : l'
i' : n'
j : m'
j' : p'
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) (i, i') (j, j') =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N) (i, i') (j, j')

Tactic:
rfl

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

Goal state before:
pp: α : Type u_3
m : Type u_10
n : Type u_11
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
a b : ℕ
⊢ (diagonal fun mn ↦ ↑(a * b)) = ↑(a * b)

Tactic:
rfl

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

Goal state before:
pp: case e_a.e_a.e_a
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ ⅟(C + C * V * ⅟A * U * C) * (C * (V * (⅟A * A))) + ⅟(C + C * V * ⅟A * U * C) * (C * (V * (⅟A * (U * (C * V))))) = V

Tactic:
← Matrix.mul_add

Goal state after:
case e_a.e_a.e_a
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ ⅟(C + C * V * ⅟A * U * C) * (C * (V * (⅟A * A)) + C * (V * (⅟A * (U * (C * V))))) = V
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix n m α
h : B = A * C
⊢ A⁻¹ * (A * C) = C

Tactic:
inv_mul_cancel_left_of_invertible

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix n m α
h : B = A * C
⊢ C = C
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Finite n
A : Matrix m n R
val✝ : Fintype n
h : Function.Surjective fun v ↦ v ᵥ* A
rows : n → m → R
hrows : ∀ (x : n), (fun v ↦ v ᵥ* A) (rows x) = Pi.single x 1
i j : n
⊢ (of rows i ᵥ* A) j = (fun v ↦ v ᵥ* A) (rows i) j

Tactic:
rfl

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

Goal state before:
pp: case intro
m : Type u
n : Type u'
R : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq m
inst✝¹ : Finite m
inst✝ : Fintype n
A : Matrix m n R
val✝ : Fintype m
h : Function.Surjective A.mulVec
cols : m → n → R
hcols : ∀ (x : m), A *ᵥ cols x = Pi.single x 1
i j : m
⊢ (A * (of cols)ᵀ) i j = (A *ᵥ cols j) i

Tactic:
rfl

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 α
inst✝ : Invertible A.det
i✝ j✝ : n
⊢ ↑A.unitOfDetInvertible i✝ j✝ = ↑(A.nonsingInvUnit ⋯) i✝ j✝

Tactic:
rfl

Goal state after:
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:
rfl

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

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
hA : IsUnit A
h : IsUnit (C + C * V * A⁻¹ * U * C)
val✝ : Invertible A
ih : Invertible (C + C * V * ⅟A * U * C)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul' U C V
⊢ ⅟(A + U * C * V) = ⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A

Tactic:
apply invOf_add_mul_mul'

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 α
⊢ (A * B)⁻¹ = B⁻¹ * A⁻¹

Tactic:
by
  simp only [inv_def]
  rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
    Ring.mul_inverse_rev]

Goal state after:
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
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i ↦ b ↑i
h' : (M.toSquareBlockProp fun i ↦ b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype ⋯
⊢ (of fun i j ↦ M.toSquareBlockProp (fun i ↦ b i ≠ k) ↑i ↑j).det = ((reindex he.symm he.symm) (M.toSquareBlock b l)).det

Tactic:
rfl

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

Goal state before:
pp: 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
inst✝¹ : Invertible A
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁

Tactic:
rfl

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

Goal state before:
pp: m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (↑h.unit * N * ↑h.unit⁻¹).det = N.det

Tactic:
det_units_conj

Goal state after:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ N.det = N.det
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
IH :
  ∀ (M : Matrix (Fin r) (Fin r) 𝕜),
    ∃ L₀ L₀' D₀, (List.map toMatrix L₀).prod * M * (List.map toMatrix L₀').prod = diagonal D₀
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
L₁ L₁' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hM : ((List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod).IsTwoBlockDiagonal
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := (List.map toMatrix L₁).prod * M * (List.map toMatrix L₁').prod
M'' : Matrix (Fin r) (Fin r) 𝕜 := M'.toBlocks₁₁
L₀ L₀' : List (TransvectionStruct (Fin r) 𝕜)
D₀ : Fin r → 𝕜
h₀ : (List.map toMatrix L₀).prod * M'' * (List.map toMatrix L₀').prod = diagonal D₀
c : 𝕜 := M' (inr ()) (inr ())
⊢ fromBlocks M'.toBlocks₁₁ 0 0 M'.toBlocks₂₂ = fromBlocks M'' 0 0 (diagonal fun x ↦ c)

Tactic:
rfl

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

Goal state before:
pp: case zero
𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩

Goal state after:
case zero
𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
⊢ (List.map toMatrix []).prod * M * (List.map toMatrix []).prod = diagonal fun x ↦ 1
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case hdiag
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := ⋯
⊢ ∀ (D : n → 𝕜), (diagonal D).det = M.det → Q (diagonal D)

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ (toFunAlgHom n R A) (invFun n R A M) = M

Tactic:
simp only [invFun, map_sum, toFunAlgHom_apply]
  convert! Finset.sum_product (β := Matrix n n A) ..
  conv_lhs => rw [matrix_eq_sum_single M]
  simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible D
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)

Tactic:
by
  let := fromBlocks₂₂Invertible A B C D
  convert! (rfl : ⅟(fromBlocks A B C D) = _)

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

Goal state before:
pp: case inl.inl
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
rfl

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

Goal state before:
pp: case inl.inr
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
rfl

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

Goal state before:
pp: case inr.inl
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
rfl

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

Goal state before:
pp: case inr.inr
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ val✝ : n
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after: