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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized₀ P.primeCompl (f P) N = ⊤
P : Ideal R
hP : P.IsMaximal
⊢ localized₀ P.primeCompl (f P) N = localized₀ P.primeCompl (f P) ⊤

Tactic:
simpa using h P

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized' (Rₚ P) P.primeCompl (f P) N = ⊥
P : Ideal R
hP : P.IsMaximal
⊢ localized' (Rₚ P) P.primeCompl (f P) N = localized' (Rₚ P) P.primeCompl (f P) ⊥

Tactic:
simpa using h P

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized' (Rₚ P) P.primeCompl (f P) N = ⊤
P : Ideal R
hP : P.IsMaximal
⊢ localized' (Rₚ P) P.primeCompl (f P) N = localized' (Rₚ P) P.primeCompl (f P) ⊤

Tactic:
simpa using h P

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : mk' (f r) a t = (f r) m
⊢ False

Tactic:
rw [← IsLocalizedModule.mk'_one (.powers r.1), IsLocalizedModule.mk'_eq_mk'_iff] at e

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : ∃ s_1, s_1 • t • m = s_1 • 1 • a
⊢ False
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * (a₂ * (algebraMap R A) ((p₁ * p₂).coeff k)) =
    ∑ x ∈ Finset.antidiagonal k, a₁ * ((algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2)))

Tactic:
Algebra.commutes,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * (a₂ * (algebraMap R A) ((p₁ * p₂).coeff k)) =
    ∑ x ∈ Finset.antidiagonal k, a₁ * (a₂ * (algebraMap R A) (p₂.coeff x.2) * (algebraMap R A) (p₁.coeff x.1))
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.comap (algebraMap R S) N = localizationLocalizationSubmodule M N

Tactic:
dsimp [localizationLocalizationSubmodule]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
H : ∀ (x : S), IsUnit x → x ∈ N
⊢ Submonoid.comap (algebraMap R S) N = Submonoid.comap (algebraMap R S) (N ⊔ Submonoid.map (algebraMap R S) M)
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ ⇑((IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
        (Algebra.linearMap R S)) =
    ⇑(↑R (Algebra.linearMap (Rₚ p) (Sₚ p)))

Tactic:
DFunLike.coe_fn_eq

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ (IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
      (Algebra.linearMap R S) =
    ↑R (Algebra.linearMap (Rₚ p) (Sₚ p))
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ ⇑((IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
        (Algebra.linearMap R S)) =
    ⇑(↑R (Algebra.linearMap (Rₚ p) (Sₚ p)))

Tactic:
DFunLike.coe_fn_eq

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ (IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
      (Algebra.linearMap R S) =
    ↑R (Algebra.linearMap (Rₚ p) (Sₚ p))
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}
m : M
x✝¹ x✝ : N
⊢ S.mkQ (m ⊗ₜ[R] (x✝¹ + x✝)) = S.mkQ (m ⊗ₜ[R] x✝¹) + S.mkQ (m ⊗ₜ[R] x✝)

Tactic:
by simp [tmul_add]

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: 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
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
⊢ (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0

Tactic:
rwa [RingEquiv.map_ne_zero_iff]

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 : IsStableUnderBaseChange P
R S Rᵣ Sᵣ : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Rᵣ
inst✝⁴ : CommRing Sᵣ
inst✝³ : Algebra R Rᵣ
inst✝² : Algebra S Sᵣ
M : Submonoid R
inst✝¹ : IsLocalization M Rᵣ
f : R →+* S
inst✝ : IsLocalization (Submonoid.map f M) Sᵣ
hf : P f
⊢ P (IsLocalization.map Sᵣ f ⋯)

Tactic:
by
  algebraize [f, IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map,
    (IsLocalization.map (S := Rᵣ) Sᵣ f M.le_comap_map).comp (algebraMap R Rᵣ)]
  have : IsScalarTower R S Sᵣ := IsScalarTower.of_algebraMap_eq'
    (IsLocalization.map_comp M.le_comap_map)
  have : IsLocalization (Algebra.algebraMapSubmonoid S M) Sᵣ :=
    inferInstanceAs <| IsLocalization (M.map f) Sᵣ
  apply hP.of_isLocalization M hf

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ ∀ (q : R[X]), trunc (toLaurent f) = f → trunc (toLaurent q) = q → trunc (toLaurent (f + q)) = f + q

Tactic:
g

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
⊢ trunc (toLaurent f) = f → trunc (toLaurent g) = g → trunc (toLaurent (f + g)) = f + g
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝¹ : DecidableEq n
inst✝ : CommRing R
i j : n
⊢ transvection i j 0 = 1

Tactic:
by simp [transvection]

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 α
A : Matrix n n α
i j : n
⊢ ∑ j_1, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0

Tactic:
simp [mul_adjugate_apply, sum_cramer_apply, cramer_transpose_row_self, Pi.single_apply, eq_comm]

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 α
b : n → α
h : IsUnit A.det
⊢ A.det • A⁻¹ *ᵥ b = A.adjugate *ᵥ b

Tactic:
A.nonsing_inv_apply h,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • (↑h.unit⁻¹ • A.adjugate) *ᵥ b = A.adjugate *ᵥ b
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case neg
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 α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
⊢ (fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

Tactic:
have hD := hAD.not.mp hA
    have : ¬IsUnit (fromBlocks A 0 C D) :=
      isUnit_fromBlocks_zero₁₂.not.mpr (not_and'.mpr fun _ => hA)
    simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ hA, Ring.inverse_non_unit _ hD,
      Ring.inverse_non_unit _ this, Matrix.zero_mul, neg_zero, fromBlocks_zero]

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

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
u v : m → α
⊢ (1 + replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u

Tactic:
Pi.add_apply,

Goal state after:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
u v : m → α
⊢ (1 default + (replicateRow ι v * replicateCol ι u) default) default = 1 + v ⬝ᵥ u
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
u v : m → α
⊢ (1 default + (replicateRow ι v * replicateCol ι u) default) default = 1 + v ⬝ᵥ u

Tactic:
Pi.add_apply,

Goal state after:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
u v : m → α
⊢ 1 default default + (replicateRow ι v * replicateCol ι u) default default = 1 + v ⬝ᵥ u
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ IsNilpotent (x + y)

Tactic:
exact ⟨_, add_pow_add_eq_zero_of_pow_eq_zero h_comm hn hm⟩

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

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsLeft R
⊢ IsNilpotent (x * y) ↔ IsNilpotent y

Tactic:
refine ⟨?_, h_comm.isNilpotent_mul_left⟩
  rintro ⟨k, hk⟩
  rw [mul_pow h_comm] at hk
  exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hx k _ hk⟩

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ∑ i, (M.charmatrix (c i) i).natDegree ≤ #{x | c x = x}

Tactic:
card_eq_sum_ones

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ∑ i, (M.charmatrix (c i) i).natDegree ≤ ∑ x with c x = x, 1
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Cardinal.lift.{v, u} (Submodule.spanRank (map (↑f.symm) (map (↑f) I))) ≤
    Cardinal.lift.{u, v} (Submodule.spanRank (map (↑f) I))

Tactic:
exact Ideal.lift_spanRank_map_le (f.symm : T →+* R) _

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
⊢ ∑ n ∈ (p %ₘ f).support, eval₂ (algebraMap R A) x (C ((p %ₘ f).coeff n) * X ^ n) ∈
    span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))

Tactic:
refine sum_mem fun k hkq ↦ ?_

Goal state after:
case refine_2
R : Type u_6
A : Type u_7
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
f : R[X]
hf : f.Monic
hfx : (aeval x) f = 0
a✝ : Nontrivial A
hf1 : f ≠ 1
p : R[X]
hr : (aeval x) p ∈ (aeval x).range
k : ℕ
hkq : k ∈ (p %ₘ f).support
⊢ eval₂ (algebraMap R A) x (C ((p %ₘ f).coeff k) * X ^ k) ∈
    span R ↑(Finset.image (fun x_1 ↦ x ^ x_1) (Finset.range f.natDegree))
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
p✝ : R[X]
monic : p✝.Monic
deg : p✝.natDegree ≠ 0
hx : IsIntegral R ((aeval x) p✝)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R A) ((aeval x) p✝) p = 0
⊢ eval₂ (algebraMap R A) x (p.comp p✝) = 0

Tactic:
by rwa [eval₂_comp, ← aeval_def x]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Cast

Goal state before:
pp: S : Type u_1
inst✝ : Ring S
a : ℕ
⊢ ↑(a.descFactorial 2) = ↑a * (↑a - 1)

Tactic:
by
  rw [descFactorial]
  cases a
  · simp
  · simp [mul_add, add_mul]

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

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : 3 ≤ i
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i

Tactic:
Nat.succ_le_iff

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
i : ℕ
hi : 2 < i
⊢ M.charpoly.coeff i = (X ^ 2 - C M.trace * X + C M.det).coeff i
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ (X ^ k).coeff m - (C ((M ^ k) j j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) j j

Tactic:
coeff_X_pow,

Goal state after:
case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
⊢ (if m = k then 1 else 0) - (C ((M ^ k) j j)).coeff m = ((if m = k then 1 else 0) - if m = 0 then M ^ k else 0) j j
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k✝ : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (k + 1) ∈ I ^ (1 - (k + 1))

Tactic:
rw [add_comm, tsub_self_add, pow_zero, Ideal.one_eq_top]

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k✝ : ℕ
c : Equiv.Perm n
this : ∑ x, 1 = Fintype.card n
i : n
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (1 + k) ∈ ⊤
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case e_6
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
by_cases! hikl : i < k + l

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.comp (X + C 0) = f

Tactic:
C_0,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.comp (X + 0) = f
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
hcharpolyRev : M.charpolyRev = (1 + X • (-M).map ⇑C).det
⊢ ∑ s ∈ powersetCard k univ, ((-M).submatrix Subtype.val Subtype.val).det =
    (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
simp only [submatrix_neg, Pi.neg_apply, det_neg, Fintype.card_coe, mul_sum]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
hcharpolyRev : M.charpolyRev = (1 + X • (-M).map ⇑C).det
⊢ ∑ s ∈ powersetCard k univ, (-1) ^ #s * (M.submatrix Subtype.val Subtype.val).det =
    ∑ i ∈ powersetCard k univ, (-1) ^ k * (M.submatrix Subtype.val Subtype.val).det
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i + 1 ≤ p.natDegree

Tactic:
Nat.succ_le_iff

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i < p.natDegree
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i + 1 ≤ p.natDegree

Tactic:
Nat.succ_le_iff

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i < p.natDegree