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

Goal state before:
pp: case mpr
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ coeSubmodule S (Ideal.span {x}) = R ∙ (algebraMap R S) x

Tactic:
coeSubmodule_span_singleton

Goal state after:
case mpr
R : Type u_3
inst✝³ : CommRing R
M : Submonoid R
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ R ∙ (algebraMap R S) x = R ∙ (algebraMap R S) x
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_2
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ₚ
⊢ Function.Surjective ⇑(algebraMap R (Rₚ ⧸ maximalIdeal Rₚ))

Tactic:
intro x

Goal state after:
case refine_2
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ₚ ⧸ maximalIdeal Rₚ
⊢ ∃ a, (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) a = x
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Set a✝
hs : Ideal.span s = ⊤
⊢ (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝

Tactic:
hs'

Goal state after:
case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Set a✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)
⊢ P e✝
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
⊢ (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
hs'

Goal state after:
case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)
⊢ P e✝
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h
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 T
hσ : ∀ (s : T), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∀ (s : T), ∃ t ∈ adjoin S ↑σ, IsUnit t ∧ s * t ∈ adjoin S ↑σ

Tactic:
intro x

Goal state after:
case h
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 T
hσ : ∀ (s : T), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x : T
⊢ ∃ t ∈ adjoin S ↑σ, IsUnit t ∧ x * t ∈ adjoin S ↑σ
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
⊢ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS) ≤ pS

Tactic:
intro x

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
⊢ x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS) → x ∈ pS
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 : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hT✝ : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)
r : ↑s
T : Type u
w✝² : CommRing T
w✝¹ : Algebra S T
w✝ : IsLocalization.Away (↑r) T
hT : P ((algebraMap S T).comp f)
⊢ (algebraMap S (Localization.Away ↑r)).comp f =
    ((↑(Localization.algEquiv (Submonoid.powers ↑r) T).symm.toRingEquiv).comp (algebraMap S T)).comp f

Tactic:
AlgEquiv.toRingEquiv_toRingHom,

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
hT✝ : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)
r : ↑s
T : Type u
w✝² : CommRing T
w✝¹ : Algebra S T
w✝ : IsLocalization.Away (↑r) T
hT : P ((algebraMap S T).comp f)
⊢ (algebraMap S (Localization.Away ↑r)).comp f =
    ((↑(Localization.algEquiv (Submonoid.powers ↑r) T).symm).comp (algebraMap S T)).comp f
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p)) ≤ I

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ x ∈ ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p)) → x ∈ I
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_2
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ₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro x

Goal state after:
case refine_2
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ₚ
Sₚ : Type u_9
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : CommRing Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra R Sₚ
inst✝³ : Algebra Rₚ Sₚ
inst✝² : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝¹ : IsScalarTower R S Sₚ
inst✝ : IsScalarTower R Rₚ Sₚ
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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)ᵀ = A.map f

Tactic:
← transpose_map,

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
⊢ Aᵀ.map f = A.map f
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ (A.map f)ᵀ = A.map f ↔ Aᵀ = A

Tactic:
← transpose_map,

Goal state after:
α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
f : α → β
hf : Function.Injective f
⊢ Aᵀ.map f = A.map f ↔ Aᵀ = A
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
R : Type u_5
inst✝² : Monoid R
inst✝¹ : MulAction R α
A : Matrix n n α
k : R
inst✝ : Invertible k
⊢ (k • A).IsSymm ↔ A.IsSymm

Tactic:
refine ⟨fun h ↦ ?_, (·.smul k)⟩
  rw [← invOf_smul_smul k A]
  exact h.smul ⅟k

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 α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Cᵀ = B

Tactic:
rw [← hBC]

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
⊢ Bᵀᵀ = B
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = 1

Tactic:
by
  cases subsingleton_or_nontrivial α
  · simp [eq_iff_true_of_subsingleton]
  rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]
  simp only [Matrix.map_one, C_eq_zero, map_one]
  rcases (natDegree_det_X_add_C_le 1 A).eq_or_lt with h | h
  · simp only [map_one, Matrix.map_one, C_eq_zero] at h
    rw [h]
  · -- contradiction. we have a hypothesis that the degree is less than |n|
    -- but we know that coeff _ n = 1
    have H := coeff_eq_zero_of_natDegree_lt h
    rw [coeff_det_X_add_C_card] at H
    simp at H

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
m n : ℤ
⊢ f * T m * T n = f * T (m + n)

Tactic:
by
  simp [← T_add, mul_assoc]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : 0 ≤ n
⊢ (comapDomainAddMonoidHom Nat.cast trunc._proof_1) (AddMonoidAlgebra.single n r) = ((monomial n.toNat) r).toFinsupp

pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : ¬0 ≤ n
⊢ (comapDomainAddMonoidHom Nat.cast trunc._proof_1) (AddMonoidAlgebra.single n r) = toFinsupp 0

Tactic:
· lift n to ℕ using hn
    simp [toFinsupp_monomial, -single_eq_C_mul_T]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
hn : ¬0 ≤ n
⊢ (comapDomainAddMonoidHom Nat.cast trunc._proof_1) (AddMonoidAlgebra.single n r) = toFinsupp 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f✝ : R →+* S
x : Sˣ
f : R[T;T⁻¹]
⊢ ∃ x, f * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1

Tactic:
by
      induction f using LaurentPolynomial.induction_on_mul_T with | _ f n
      have : X ^ n ∈ Submonoid.powers (X : R[X]) := ⟨n, rfl⟩
      refine ⟨(f, ⟨_, this⟩), ?_⟩
      simp only [algebraMap_eq_toLaurent, toLaurent_X_pow, mul_T_assoc, neg_add_cancel, T_zero,
        mul_one]

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

Goal state before:
pp: case mk.inr.inr
n : Type u_1
p : Type u_2
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i✝ j✝ : n
hij✝ : i✝ ≠ j✝
c✝ : R
a b : p
⊢ (sumInl p { i := i✝, j := j✝, hij := hij✝, c := c✝ }).toMatrix (inr a) (inr b) =
    fromBlocks { i := i✝, j := j✝, hij := hij✝, c := c✝ }.toMatrix 0 0 1 (inr a) (inr b)

Tactic:
by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h]

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

Goal state before:
pp: case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n > 0
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
replace h_card := tsub_add_cancel_of_le h_card.nat_succ_le

Goal state after:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

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

Tactic:
adjugate_fin_succ_eq_det_submatrix

Goal state after:
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det = !![A 1 1, -A 0 1; -A 1 0, A 0 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✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ A * (⅟A * B) = B

Tactic:
rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul]

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 : β
⊢ kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) = single (i₁, i₂) (j₁, j₂) (f a b)

Tactic:
ext ⟨i₁', i₂'⟩ ⟨j₁', j₂'⟩
  dsimp [single]
  grind

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⁻¹ = ↑h.unit⁻¹ • A.adjugate

Tactic:
by
  rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]

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
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ ⅟A = A⁻¹

Tactic:
rw [inv_def, Ring.inverse_invertible, invOf_eq]

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'
⊢ (M.toSquareBlockProp fun i ↦ ¬b i = k).det = ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det

Tactic:
have hb' : image b' univ = (image b univ).erase k := by
      convert! image_subtype_ne_univ_eq_image_erase k b

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' ⋯
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
⊢ (M.toSquareBlockProp fun i ↦ ¬b i = k).det = ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det
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
i : n
⊢ M.charmatrix i i = X - C (M i i)

Tactic:
by
  simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, map_apply,
    diagonal_apply_eq]

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ (if i' = i ∧ j' = j then x.coeff k else 0) = (if i' = i ∧ j' = j then x else 0).coeff k

Tactic:
split_ifs <;> rename_i h

Goal state after:
case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : i' = i ∧ j' = j
⊢ x.coeff k = x.coeff k

case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : ¬(i' = i ∧ j' = j)
⊢ 0 = coeff 0 k
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
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
⊢ ((A * B).map ⇑C - (scalar m) X).det * (-(scalar n) X).det =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)

Tactic:
← neg_sub,

Goal state after:
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
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
⊢ (-((scalar m) X - (A * B).map ⇑C)).det * (-(scalar n) X).det =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
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
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
hdet_MN :
  (M * N).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
⊢ (-(scalar m) X).det * ((B * A).map ⇑C - (scalar n) X).det =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card m * ((scalar n) X - (B * A).map ⇑C).det)

Tactic:
← neg_sub,

Goal state after:
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
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
hdet_MN :
  (M * N).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
⊢ (-(scalar m) X).det * (-((scalar n) X - (B * A).map ⇑C)).det =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card m * ((scalar n) X - (B * A).map ⇑C).det)
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
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C)

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (invertibleEquivFromBlocks₂₂Invertible A B C D).nonempty_congr]

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 A
⊢ (fromBlocks A B C D).det = A.det * (D - C * ⅟A * B).det

Tactic:
rw [fromBlocks_eq_of_invertible₁₁ (A := A), det_mul, det_mul, det_fromBlocks_zero₂₁,
    det_fromBlocks_zero₂₁, det_fromBlocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one]

Goal state after: