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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst✝² : CommRing R'
inst✝¹ : CommRing S'
inst✝ : Algebra R' S'
f : R →+* R'
hf : Function.Surjective ⇑f
g : S →+* S'
hg : Function.Surjective ⇑g
H : g.comp (algebraMap R S) = (algebraMap R' S').comp f
H' : RingHom.ker g ≤ Ideal.map (algebraMap R S) (RingHom.ker f)
⊢ ∀ {x y : R'}, (algebraMap R' S') x = (algebraMap R' S') y → ∃ c, ↑c * x = ↑c * y

Tactic:
intro x y e
    obtain ⟨x, rfl⟩ := hf x
    obtain ⟨y, rfl⟩ := hf y
    rw [← sub_eq_zero, ← map_sub, ← map_sub, ← RingHom.comp_apply, ← H, RingHom.comp_apply,
      ← IsLocalization.mk'_one (M := M)] at e
    obtain ⟨r, hr, hr'⟩ := (IsLocalization.mk'_mem_map_algebraMap_iff M _ _ _ _).mp (H' e)
    exact ⟨⟨_, r, hr, rfl⟩, by simpa [sub_eq_zero, mul_sub] using hr'⟩

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

Goal state before:
pp: case refine_2
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 y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * z' * x = ↑c * (z' * y)
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y

Tactic:
← mul_assoc

Goal state after:
case refine_2
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 y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * z' * x = ↑c * z' * y
⊢ ↑⟨↑c * z', ⋯⟩ * x = ↑⟨↑c * z', ⋯⟩ * y
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
J : Ideal S
inst✝ : (under R J).IsMaximal
⊢ J.IsMaximal

Tactic:
obtain ⟨m, maxm, hm⟩ := exists_le_maximal J <| by
    rintro rfl
    exact Ideal.IsMaximal.ne_top ‹_› (by simp)

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
J : Ideal S
inst✝ : (under R J).IsMaximal
m : Ideal S
maxm : m.IsMaximal
hm : J ≤ m
⊢ J.IsMaximal
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 tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x * tx * ty + y * (ty * tx) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
← mul_assoc

Goal state after:
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 tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x * tx * ty + y * ty * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Ring α
h : ∀ {a b : α}, a * b = 1 → b * a = 1
x y z : α
hxz : x * z = 1
hyz : y * z = 1
⊢ x = y

Tactic:
simpa [mul_assoc, h hyz] using congr_arg (· * y) hxz

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Monoid R
S : Submonoid R
⊢ ((∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s) →
    Nonempty (OreSet S)

Tactic:
intro ⟨H, H'⟩
    choose r' s' h using H'
    exact ⟨H, r', s', h⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
S : Submonoid R
⊢ Nonempty (OreSet S) ↔
    (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧
      ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s

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

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

Goal state before:
pp: case refine_4
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ₚ
n : ℕ
⊢ (Quotient.liftₐ (maximalIdeal Rₚ ^ n) (liftAlgHom ⋯) ⋯).comp
      (Quotient.liftₐ (p ^ n) (ofId R (Rₚ ⧸ maximalIdeal Rₚ ^ n)) ⋯) =
    AlgHom.id R (R ⧸ p ^ n)

Tactic:
· rw [← AlgHom.cancel_right (Ideal.Quotient.mkₐ_surjective _ _)]
    ext

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
H : LocalizationPreserves P
R : Type u
⊢ ∀ ⦃S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_2 : CommRing R']
    [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ P) (IsLocalization.Away.map R' S' f r)

Tactic:
S

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves P
R S : Type u
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_2 : CommRing R']
    [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ P) (IsLocalization.Away.map R' S' f r)
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 α)
⊢ ((comp m m n n α) A).IsSymm ↔ ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'

Tactic:
by
  simp [IsSymm.ext_iff]
  grind

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

Goal state before:
pp: case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ ∀ (a : ℤ) (s : Finset ℤ), a ∉ s → M (∑ n ∈ s, C (p.coeff n) * T n) → M (∑ n ∈ insert a s, C (p.coeff n) * T n)

Tactic:
intro n s ns ih

Goal state after:
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
n : ℤ
s : Finset ℤ
ns : n ∉ s
ih : M (∑ n ∈ s, C (p.coeff n) * T n)
⊢ M (∑ n ∈ insert n s, C (p.coeff n) * T n)
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (n : ℕ) (a : R), trunc (toLaurent ((monomial n) a)) = (monomial n) a

Tactic:
intro n r
    simp only [Polynomial.toLaurent_C_mul_T, trunc_C_mul_T, Int.natCast_nonneg, Int.toNat_natCast,
      if_true]

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 α
⊢ A.adjugate * A = (Aᵀ * A.adjugateᵀ)ᵀ

Tactic:
← transpose_mul,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A.adjugate * A = (A.adjugate * A)ᵀᵀ
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
M : Matrix n n R
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (t : TransvectionStruct n R), Commute t.toMatrix M

Tactic:
refine ⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩
  rw [mem_range_scalar_iff_commute_single] at h
  refine (Commute.one_left M).add_left ?_
  convert! (h _ _ t.hij).smul_left t.c using 1
  rw [smul_single, smul_eq_mul, mul_one]

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 uM
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Module.rank T P = Module.rank R M

Tactic:
simpa using lift_rank_eq_of_le_nonZeroDivisors S f hp hpT bc

Goal state after:
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✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ (⅟A)ᵀ * Aᵀ = 1

Tactic:
← transpose_mul,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ (A * ⅟A)ᵀ = 1
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✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ Aᵀ * (⅟A)ᵀ = 1

Tactic:
← transpose_mul,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ (⅟A * A)ᵀ = 1
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₂'⟩

Goal state after:
α : 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
⊢ kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) (i₁', i₂') (j₁', j₂') =
    single (i₁, i₂) (j₁, j₂) (f a b) (i₁', i₂') (j₁', 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✝⁵ : 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
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ ⅟A * A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * A + ⅟A * U * C * V -
      ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    1 + ⅟A * U * C * V - (⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V)

Tactic:
by
      rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]
      abel

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

Goal state before:
pp: case neg.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ (if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())) = if n ≤ ↑i then 0 else M (inl i) (inr ())

Tactic:
rw [if_neg, if_neg]
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
        · simpa only [not_le] using hi

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

Goal state before:
pp: case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.det • (1 * B) = A.det • C

Tactic:
← Matrix.one_mul C,

Goal state after:
case left
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
hA : IsLeftRegular A.det
B C : Matrix n n α
h : A * B = A * C
⊢ A.det • (1 * B) = A.det • (1 * C)
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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
B : List.map toMatrix L' = listTransvecRow M
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
rw [A, B]

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
B : List.map toMatrix L' = listTransvecRow M
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i j : m
n✝ : ℕ
⊢ (((scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂)) (Sum.inl i) (Sum.inl j)).coeff n✝ =
    (fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
          (Sum.inl i) (Sum.inl j)).coeff
      n✝

Tactic:
simp [diagonal]

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

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i : m
j : n
n✝ : ℕ
⊢ (((scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂)) (Sum.inl i) (Sum.inr j)).coeff n✝ =
    (fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
          (Sum.inl i) (Sum.inr j)).coeff
      n✝

Tactic:
simp [diagonal]

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

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i : n
j : m
n✝ : ℕ
⊢ (((scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂)) (Sum.inr i) (Sum.inl j)).coeff n✝ =
    (fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
          (Sum.inr i) (Sum.inl j)).coeff
      n✝

Tactic:
simp [diagonal]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M₁₁ : Matrix m m R
M₁₂ : Matrix m n R
M₂₁ : Matrix n m R
M₂₂ : Matrix n n R
i j : n
n✝ : ℕ
⊢ (((scalar (m ⊕ n)) X - C.mapMatrix (fromBlocks M₁₁ M₁₂ M₂₁ M₂₂)) (Sum.inr i) (Sum.inr j)).coeff n✝ =
    (fromBlocks ((scalar m) X - C.mapMatrix M₁₁) (-M₁₂.map ⇑C) (-M₂₁.map ⇑C) ((scalar n) X - C.mapMatrix M₂₂)
          (Sum.inr i) (Sum.inr j)).coeff
      n✝

Tactic:
simp [diagonal]

Goal state after:
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
e : n ≃ m
M : Matrix n n R
⊢ ((reindex e e) M).charmatrix.det = M.charmatrix.det

Tactic:
rw [charmatrix_reindex, Matrix.det_reindex_self]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * (↑M * N)).charpoly = N.charpoly

Tactic:
← mul_assoc

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * ↑M * N).charpoly = N.charpoly
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁸ : Fintype l
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq l
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 (fromBlocks A B C D)
this : Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D)
⊢ Invertible (A - B * ⅟D * C)

Tactic:
by
    exact (invertibleOfFromBlocksZero₁₂Invertible (A - B * ⅟D * C) 0 D).1

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ { k // eval (x + y) f = eval x f + eval x (derivative f) * y + k * y ^ 2 }

Tactic:
exists f.sum fun e a => a * (polyBinomAux1 x y e a).val

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
f : R[X]
x y : R
⊢ eval (x + y) f = eval x f + eval x (derivative f) * y + (f.sum fun e a ↦ a * ↑(polyBinomAux1 x y e a)) * y ^ 2
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
k : ℕ
hind :
  ∀ m < k, ∀ {P : R[X]}, IsUnit (P.coeff 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) → P.natDegree = m → IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : P.natDegree = 0
⊢ IsUnit (C (P.coeff 0))

Tactic:
exact hunit.map C

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

Tactic:
obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit
  constructor
  · refine .of_mul_eq_one (Q.coeff 0) ?_
    have h := (mul_coeff_zero P Q).symm
    rwa [hQ, coeff_one_zero] at h
  · intro n hn
    rw [nilpotent_iff_mem_prime]
    intro I hI
    let f := mapRingHom (Ideal.Quotient.mk I)
    have hPQ : degree (f P) = 0 ∧ degree (f Q) = 0 := by
      rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
    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
    rw [coe_mapRingHom, coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at hcoeff
    exact hcoeff

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
| span R ↑T * (↑I⁻¹ * ↑I)

Tactic:
← mul_assoc

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
| span R ↑T * ↑I⁻¹ * ↑I
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
⊢ p.spanRank = ↑p.spanFinrank ↔ p.FG

Tactic:
rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm]
  exact cast_toNat_eq_iff_lt_aleph0

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
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
let e := Matrix.reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
e : Matrix n n R ≃ₗ[R] Matrix (Fin (Fintype.card n)) (Fin (Fintype.card n)) R :=
  reindexLinearEquiv R R (Fintype.equivFin n) (Fintype.equivFin n)
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
Module: Mathlib.Data.Nat.Choose.Cast

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ¬n ! = 0
⊢ b.choose a * (a ! * (b - a)!) = b !

Tactic:
← mul_assoc

Goal state after:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ¬n ! = 0
⊢ b.choose a * a ! * (b - a)! = b !