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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
H : ∀ (P : Ideal S) [inst : P.IsMaximal], Flat R (Mₚ P)
⊢ Flat R M

Tactic:
simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor M N.subtype)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
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
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ ↑s * (algebraMap R S) (↑t' * ↑t) = ↑s * (algebraMap R S) ↑(t' * t)

Tactic:
Submonoid.coe_mul

Goal state after:
case refine_1
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
x : T
y : S
s : ↥N
eq₁ : x * (algebraMap S T) ↑s = (algebraMap S T) y
z : R
t : ↥M
eq₂ : y * (algebraMap R S) ↑t = (algebraMap R S) z
z' : R
t' : ↥M
eq₃ : ↑s * (algebraMap R S) ↑t' = (algebraMap R S) z'
⊢ ↑s * (algebraMap R S) (↑t' * ↑t) = ↑s * (algebraMap R S) (↑t' * ↑t)
Module: Mathlib.RingTheory.Flat.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
s : Set S
spn : Ideal.span s = ⊤
Mₛ : ↑s → Type u_5
inst✝⁴ : (r : ↑s) → AddCommMonoid (Mₛ r)
inst✝³ : (r : ↑s) → Module R (Mₛ r)
inst✝² : (r : ↑s) → Module S (Mₛ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Mₛ r)
g : (r : ↑s) → M →ₗ[S] Mₛ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
H : ∀ (r : ↑s), Flat R (Mₛ r)
⊢ Flat R M

Tactic:
simp_rw [Flat.iff_lTensor_injectiveₛ] at H ⊢

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
s : Set S
spn : Ideal.span s = ⊤
Mₛ : ↑s → Type u_5
inst✝⁴ : (r : ↑s) → AddCommMonoid (Mₛ r)
inst✝³ : (r : ↑s) → Module R (Mₛ r)
inst✝² : (r : ↑s) → Module S (Mₛ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Mₛ r)
g : (r : ↑s) → M →ₗ[S] Mₛ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
H :
  ∀ (r : ↑s) ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor (Mₛ r) N.subtype)
⊢ ∀ ⦃P : Type u_1⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(lTensor M N.subtype)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case mp
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✝
⊢ (∀ (s : Set a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝) →
    ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝

Tactic:
intro h s

Goal state after:
case mp
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 : Set a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Finset a✝
⊢ Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case mp
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✝
⊢ (∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) →
    ∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
intro h s

Goal state after:
case mp
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 : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Finset b✝
⊢ Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
Module: Mathlib.RingTheory.OreLocalization.OreSet

Goal state before:
pp: case mp
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

pp: case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ (∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) → Nonempty (OreSet S)

Tactic:
· exact fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
S : Submonoid R
⊢ (∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) → Nonempty (OreSet S)
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 B : Matrix n n α
⊢ (X • A.map ⇑C + B.map ⇑C).det.coeff 0 = B.det

Tactic:
by
  rw [det_apply, finsetSum_coeff, det_apply]
  refine Finset.sum_congr rfl ?_
  rintro g -
  convert! coeff_smul (R := α) (sign g) _ 0
  rw [coeff_zero_prod]
  refine Finset.prod_congr rfl ?_
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case mpr
R : Type uR
S : Type uS
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra S A
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R S A
inst✝ : IsFractionRing S A
a✝ : Nontrivial R
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x) →
    ∃ s, s.card = n ∧ LinearIndependent R fun (x : ↑↑s) ↦ id ↑x

Tactic:
rintro ⟨s, rfl, hs⟩
    exact ⟨finsetIntegerMultiple S⁰ s, card_finsetIntegerMultiple S⁰ s,
      linearIndepOn_finsetIntegerMultiple S⁰ hs⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
| Cardinal.lift.{max uM (max uP uS) uT, uN} (Module.rank S N)

Tactic:
← lift_lift.{max uS uT, max uM uP},

Goal state after:
R : Type uR
S : Type uS
M : Type uM
N : Type uN
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : AddCommGroup M
inst✝¹⁶ : AddCommGroup N
inst✝¹⁵ : Module R M
inst✝¹⁴ : Module R N
inst✝¹³ : Algebra R S
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
p : Submonoid R
inst✝¹⁰ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁹ : IsLocalizedModule p f
hp : p ≤ R⁰
inst✝⁸ : Free S N
inst✝⁷ : StrongRankCondition S
T : Type uT
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R T
hpT : Algebra.algebraMapSubmonoid T p ≤ T⁰
inst✝⁴ : StrongRankCondition (S ⊗[R] T)
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
ST : Type (max uS uT) := S ⊗[R] T
| Cardinal.lift.{max uM uP, max (max uS uT) uN} (Cardinal.lift.{max uS uT, uN} (Module.rank S N))
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f (M.adjugate i k) = ((M.map ⇑f).updateRow k (Pi.single i 1)).det

Tactic:
this,

Goal state after:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f (M.adjugate i k) = ((M.map ⇑f).updateRow k (⇑f ∘ Pi.single i 1)).det
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : Module R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (C r * p).smeval x = r • p.smeval x
hq : (C r * q).smeval x = r • q.smeval x
⊢ (C r * (p + q)).smeval x = r • (p + q).smeval x

Tactic:
| add p q hp hq =>

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg : ∑ i ∈ Finset.range (n + 1), g i • (r * ↑s ^ (i + x)) = 0
i : ℕ
hin : i < n + 1
⊢ g i = 0

Tactic:
Finset.sum_range_succ'

Goal state after:
case succ
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x : ℕ
hg : ∑ k ∈ Finset.range n, g (k + 1) • (r * ↑s ^ (k + 1 + x)) + g 0 • (r * ↑s ^ (0 + x)) = 0
i : ℕ
hin : i < n + 1
⊢ g i = 0
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (vecMulVec a b).trace = a ⬝ᵥ b

Tactic:
rw [vecMulVec_eq Unit, trace_replicateCol_mul_replicateRow]

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

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : Nonempty n
r : R
⊢ ∃ a, a.trace = r

Tactic:
by
  classical
  inhabit n
  exact ⟨single default default r, trace_single_eq_same default r⟩

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 α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ).adjugate.adjugate =
    ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).det ^ (Fintype.card n - 2) •
      (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)

Tactic:
this,

Goal state after:
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' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2) • A'
⊢ (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (A'.det ^ (Fintype.card n - 2) • A') =
    ((MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)).det ^ (Fintype.card n - 2) •
      (MvPolynomial.aeval fun p ↦ A p.1 p.2).mapMatrix (mvPolynomialX n n ℤ)
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h_det : ¬IsUnit A.det
⊢ A⁻¹ = A⁻¹ʳ

Tactic:
have h := mt A.isUnit_iff_isUnit_det.mp h_det
    rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]

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
u v : n → α
hM : u = A *ᵥ v
⊢ (A⁻¹ * A) *ᵥ v = v

Tactic:
Matrix.inv_mul_of_invertible,

Goal state after:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
u v : n → α
hM : u = A *ᵥ v
⊢ 1 *ᵥ v = v
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0

Tactic:
this,

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ((listTransvecCol (M * (listTransvecRow M).prod)).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
α : Type v
inst✝³ : CommRing α
inst✝² : Subsingleton m
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
i : m
⊢ A.det = A i i

Tactic:
exact det_eq_elem_of_subsingleton _ _

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

Tactic:
this,

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)
⊢ (M.toSquareBlockProp fun i ↦ b i = k).det * (M.toSquareBlockProp fun i ↦ ¬b i = k).det =
    ∏ a ∈ insert k ((image b univ).erase k), (M.toSquareBlock b a).det
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this✝ : Invertible (M.toBlock p p)
this : (fun i ↦ k ≤ b i) = q
⊢ (M⁻¹.toBlock (fun i ↦ k ≤ b i) fun i ↦ b i < k) = 0

Tactic:
this,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this✝ : Invertible (M.toBlock p p)
this : (fun i ↦ k ≤ b i) = q
⊢ (M⁻¹.toBlock q fun i ↦ b i < k) = 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 (M.map ⇑C) = C M

Tactic:
by
  rw [← matPolyEquiv_symm_C, AlgEquiv.apply_symm_apply]

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
d : n → R
⊢ (diagonal fun x ↦ X) - (diagonal d).map ⇑C = diagonal fun i ↦ X - C (d i)

Tactic:
diagonal_map (map_zero _),

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
d : n → R
⊢ ((diagonal fun x ↦ X) - diagonal fun m ↦ C (d m)) = diagonal fun i ↦ X - C (d i)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
H : ∃ L L' D, (List.map toMatrix L).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L').prod = diagonal D
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
rcases H with ⟨L₀, L₀', D₀, h₀⟩
  refine ⟨L₀.map (reindexEquiv e.symm), L₀'.map (reindexEquiv e.symm), D₀ ∘ e, ?_⟩
  have : M = reindexAlgEquiv 𝕜 _ e.symm (reindexAlgEquiv 𝕜 _ e M) := by simp
  rw [this]
  simp_rw [List.map_map, toMatrix_reindexEquiv_prod, ← map_mul, h₀]
  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
this : fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)
⊢ (fromBlocks A B C D).det = D.det * (A - B * ⅟D * C).det

Tactic:
this,

Goal state after:
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
this : fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)
⊢ ((fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)).det = D.det * (A - B * ⅟D * 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 α
⊢ (fromBlocks A B C 1).det = (A - B * C).det

Tactic:
have : Invertible (1 : Matrix n n α) := invertibleOne

Goal state after:
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 α
this : Invertible 1
⊢ (fromBlocks A B C 1).det = (A - B * 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 α
⊢ (fromBlocks A B C 1).det = (A - B * C).det

Tactic:
have : Invertible (1 : Matrix n n α) := invertibleOne
  rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : (f P).degree = 0 ∧ (f Q).degree = 0
⊢ P.coeff n ∈ I

Tactic:
have hcoeff : (f P).coeff n = 0 := by
      refine coeff_eq_zero_of_degree_lt ?_
      rw [hPQ.1]
      exact WithBot.coe_pos.2 hn.bot_lt

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : (f P).degree = 0 ∧ (f Q).degree = 0
hcoeff : (f P).coeff n = 0
⊢ P.coeff n ∈ I
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
this : P = C (eval 0 P) + X * (P /ₘ X)
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)

Tactic:
by
    conv_lhs => rw [this]; simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).spanRank ≤ #↑s

Tactic:
by
  rw [spanRank]
  let s' : {s1 : Set M // span R s1 = span R s} := ⟨s, rfl⟩
  exact ciInf_le' _ s'

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.spanFinrank = 1
fg : p.FG
⊢ ∃ a, p.generators = {a}

Tactic:
simpa [← fg.generators_ncard] using h

Goal state after: