mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ IsLocalization (Submonoid.comap (algebraMap R S) N) T

Tactic:
convert! localization_localization_isLocalization M N T using 1
  dsimp [localizationLocalizationSubmodule]
  congr
  symm
  rw [sup_eq_left]
  rintro _ ⟨x, hx, rfl⟩
  exact H _ (IsLocalization.map_units _ ⟨x, hx⟩)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
⊢ Submodule.map (↑(LinearEquiv.refl R (M ⊗[R] N)))
      ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id ⊥.subtype).range) =
    (map m.subtype LinearMap.id).range

Tactic:
by
    simp [Submodule.map_span, range_map_eq_span_tmul]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Ideal S
inst✝² : P.IsPrime
s : Subalgebra R S
H : s.saturation (P.primeCompl ⊓ s.toSubmonoid) ⋯ = ⊤
p : Ideal ↥s
inst✝¹ : p.IsPrime
inst✝ : P.LiesOver p
this : ∀ (y z : S), z ∉ P → ∃ y' ∈ s, ∃ z' ∉ P, z' ∈ s ∧ ∃ t ∉ P, t * (z * y') = t * (z' * y)
⊢ Function.Surjective ⇑(localRingHom p P (algebraMap (↥s) S) ⋯)

Tactic:
by
      simpa [(IsLocalization.mk'_surjective p.primeCompl).exists,
        (IsLocalization.mk'_surjective P.primeCompl).forall, P.over_def p,
        Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq, -map_mul,
        IsLocalization.eq_iff_exists P.primeCompl, Function.Surjective] using this

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
R' : Type u_5
S' : Type u_6
M : Submonoid R
T : Submonoid S
inst✝¹¹ : CommSemiring R'
inst✝¹⁰ : CommSemiring S'
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra S S'
inst✝⁷ : Algebra R' S'
inst✝⁶ : Algebra R S'
inst✝⁵ : IsScalarTower R S S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsLocalization M R'
inst✝² : IsLocalization T S'
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
disj : Disjoint ↑T ↑P
h : Ideal.map (algebraMap R R') (under R (under R' (Ideal.map (algebraMap S S') P))) = Ideal.map (algebraMap R R') p
⊢ Ideal.map (algebraMap R R') p = under R' (Ideal.map (algebraMap S S') P)

Tactic:
rw [← h, IsLocalization.map_under (M := M)]

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

Goal state before:
pp: case h
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
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ (Ideal.Quotient.mk p) ↑s ≠ 0

Tactic:
rw [Ne, Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
case h
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
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ ↑s ∉ p
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 S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ ∀ (r : R) (R' S' : Type u) [inst : CommRing R'] [inst_1 : CommRing S'] [inst_2 : Algebra R R'] [inst_3 : Algebra S S']
    [inst_4 : IsLocalization.Away r R'] [inst_5 : 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:
r

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✝ : CommRing S
f : R →+* S
r : R
⊢ ∀ (R' S' : Type u) [inst : CommRing R'] [inst_1 : CommRing S'] [inst_2 : Algebra R R'] [inst_3 : Algebra S S']
    [inst_4 : IsLocalization.Away r R'] [inst_5 : 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.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ₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑c * ↑(y, s).1 ∈ pS

Tactic:
exact Ideal.mul_mem_left _ _ y.prop

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
⊢ LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by
  introv R hf
  exact hP.isLocalization_map _ _ hf

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

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
r : R
⊢ trunc (toLaurent ((monomial n) r)) = (monomial n) r
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.refine_2
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul 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✝
this✝¹ : NoZeroDivisors R
h✝ : Nontrivial R
this✝ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝¹ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
x✝ : Field (FR ⊗[R] FT) := ⋯.toField
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Tactic:
have := bc.comp_iff.2 ((isLocalizedModule_iff_isBaseChange T⁰ FT g).1 inferInstance)

Goal state after:
case inr.refine_2
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul 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✝
this✝² : NoZeroDivisors R
h✝ : Nontrivial R
this✝¹ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this✝ : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝¹ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
x✝ : Field (FR ⊗[R] FT) := ⋯.toField
this : IsBaseChange FT (↑R g ∘ₗ g✝)
⊢ Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : k ≤ r → (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
hkr : k < r
k' : Fin r := ⟨k, hkr⟩
this : (listTransvecRow M)[k]? = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ (M * (List.take k (listTransvecRow M)).prod *
        transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
      i (inr ()) =
    M i (inr ())

Tactic:
rw [mul_transvection_apply_of_ne, IH hkr.le]

Goal state after:
case succ.hb
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : k ≤ r → (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
hkr : k < r
k' : Fin r := ⟨k, hkr⟩
this : (listTransvecRow M)[k]? = some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ inr () ≠ inl k'
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case refine_1
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
h : Function.Injective fun v ↦ v ᵥ* A
⊢ Function.Surjective fun v ↦ v ᵥ* A

Tactic:
exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ A = B

Tactic:
refine left_inv_eq_left_inv (mul_nonsing_inv _ h') ?_

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * A⁻¹ = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case inr.inr
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
ht : Nontrivial α
hc : 0 < Fintype.card n
⊢ 0⁻¹ = 0

Tactic:
· have hn : Nonempty n := Fintype.card_pos_iff.mp hc
    refine nonsing_inv_apply_not_isUnit _ ?_
    simp [det]

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

Goal state before:
pp: case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
hM : M (inr ()) (inr ()) = 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
simp only [not_and_or, IsTwoBlockDiagonal, toBlocks₁₂, toBlocks₂₁, ← Matrix.ext_iff] at H

Goal state after:
case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
⊢ M.det = ∏ k, (M.toSquareBlock b k).det

Tactic:
refine h.det.trans (prod_subset (subset_univ _) fun a _ ha => ?_)

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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
a : α
x✝ : a ∈ univ
ha : a ∉ image b univ
⊢ (M.toSquareBlock b a).det = 1
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : k = k✝
⊢ single i j x = single i j x

Tactic:
· funext
        simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : ¬k = k✝
⊢ 0 = single i j 0

Tactic:
· funext
        simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case refine_2
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 : n
⊢ ∀ (p q : Matrix n n R[X]),
    (matPolyEquiv p).coeff k i j = (p i j).coeff k →
      (matPolyEquiv q).coeff k i j = (q i j).coeff k → (matPolyEquiv (p + q)).coeff k i j = ((p + q) i j).coeff k

Tactic:
intro p q hp hq
    simp [hp, hq]

Goal state after:
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 α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks (⅟(fromBlocks A B 0 D)).toBlocks₁₁ (⅟(fromBlocks A B 0 D)).toBlocks₁₂ (⅟(fromBlocks A B 0 D)).toBlocks₂₁
        (⅟(fromBlocks A B 0 D)).toBlocks₂₂ *
      fromBlocks A B 0 D =
    1
⊢ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A = 1

Tactic:
fromBlocks_multiply

Goal state after:
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 α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks ((⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A + (⅟(fromBlocks A B 0 D)).toBlocks₁₂ * 0)
      ((⅟(fromBlocks A B 0 D)).toBlocks₁₁ * B + (⅟(fromBlocks A B 0 D)).toBlocks₁₂ * D)
      ((⅟(fromBlocks A B 0 D)).toBlocks₂₁ * A + (⅟(fromBlocks A B 0 D)).toBlocks₂₂ * 0)
      ((⅟(fromBlocks A B 0 D)).toBlocks₂₁ * B + (⅟(fromBlocks A B 0 D)).toBlocks₂₂ * D) =
    1
⊢ (⅟(fromBlocks A B 0 D)).toBlocks₁₁ * A = 1
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 α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks A B 0 D *
      fromBlocks (⅟(fromBlocks A B 0 D)).toBlocks₁₁ (⅟(fromBlocks A B 0 D)).toBlocks₁₂
        (⅟(fromBlocks A B 0 D)).toBlocks₂₁ (⅟(fromBlocks A B 0 D)).toBlocks₂₂ =
    1
⊢ D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂ = 1

Tactic:
fromBlocks_multiply

Goal state after:
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 α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A B 0 D)
this :
  fromBlocks (A * (⅟(fromBlocks A B 0 D)).toBlocks₁₁ + B * (⅟(fromBlocks A B 0 D)).toBlocks₂₁)
      (A * (⅟(fromBlocks A B 0 D)).toBlocks₁₂ + B * (⅟(fromBlocks A B 0 D)).toBlocks₂₂)
      (0 * (⅟(fromBlocks A B 0 D)).toBlocks₁₁ + D * (⅟(fromBlocks A B 0 D)).toBlocks₂₁)
      (0 * (⅟(fromBlocks A B 0 D)).toBlocks₁₂ + D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂) =
    1
⊢ D * (⅟(fromBlocks A B 0 D)).toBlocks₂₂ = 1
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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks A 0 C D *
      fromBlocks (⅟(fromBlocks A 0 C D)).toBlocks₁₁ (⅟(fromBlocks A 0 C D)).toBlocks₁₂
        (⅟(fromBlocks A 0 C D)).toBlocks₂₁ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ =
    1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1

Tactic:
fromBlocks_multiply

Goal state after:
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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
      (A * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + 0 * (⅟(fromBlocks A 0 C D)).toBlocks₂₂)
      (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₁)
      (C * (⅟(fromBlocks A 0 C D)).toBlocks₁₂ + D * (⅟(fromBlocks A 0 C D)).toBlocks₂₂) =
    1
⊢ A * (⅟(fromBlocks A 0 C D)).toBlocks₁₁ = 1
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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks (⅟(fromBlocks A 0 C D)).toBlocks₁₁ (⅟(fromBlocks A 0 C D)).toBlocks₁₂ (⅟(fromBlocks A 0 C D)).toBlocks₂₁
        (⅟(fromBlocks A 0 C D)).toBlocks₂₂ *
      fromBlocks A 0 C D =
    1
⊢ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D = 1

Tactic:
fromBlocks_multiply

Goal state after:
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 α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible (fromBlocks A 0 C D)
this :
  fromBlocks ((⅟(fromBlocks A 0 C D)).toBlocks₁₁ * A + (⅟(fromBlocks A 0 C D)).toBlocks₁₂ * C)
      ((⅟(fromBlocks A 0 C D)).toBlocks₁₁ * 0 + (⅟(fromBlocks A 0 C D)).toBlocks₁₂ * D)
      ((⅟(fromBlocks A 0 C D)).toBlocks₂₁ * A + (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * C)
      ((⅟(fromBlocks A 0 C D)).toBlocks₂₁ * 0 + (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D) =
    1
⊢ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D = 1
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)
⊢ Invertible (A - B * ⅟D * C)

Tactic:
by
  suffices Invertible (fromBlocks (A - B * ⅟D * C) 0 0 D) by
    exact (invertibleOfFromBlocksZero₁₂Invertible (A - B * ⅟D * C) 0 D).1
  letI : Invertible (1 : Matrix n n α) := invertibleOne
  letI : Invertible (1 : Matrix m m α) := invertibleOne
  letI iDC : Invertible (fromBlocks 1 0 (⅟D * C) 1 : Matrix (m ⊕ n) (m ⊕ n) α) :=
    fromBlocksZero₁₂Invertible _ _ _
  letI iBD : Invertible (fromBlocks 1 (B * ⅟D) 0 1 : Matrix (m ⊕ n) (m ⊕ n) α) :=
    fromBlocksZero₂₁Invertible _ _ _
  letI iBDC := Invertible.copy ‹_› _ (fromBlocks_eq_of_invertible₂₂ A B C D).symm
  refine (iBD.mulLeft _).symm ?_
  exact (iDC.mulRight _).symm iBDC

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

Goal state before:
pp: R : Type u_1
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ IsReduced R

Tactic:
simp_rw [isReduced_iff, IsNilpotent, exists_imp, ← zero_dvd_iff]

Goal state after:
R : Type u_1
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x
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')
⊢ ↑I ≤ span R ↑T

Tactic:
← one_mul I,

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')
⊢ ↑(1 * I) ≤ span R ↑T
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s // span R s = span R (Set.range v) }
this : #↑↑x = #↑(Subtype.val ⁻¹' ↑x)
⊢ span R (Subtype.val ⁻¹' ↑x) = ⊤

Tactic:
· apply map_injective_of_injective (f := (span R _).subtype) (injective_subtype _)
    simp [map_span, Set.image_preimage_eq_inter_range, Set.inter_eq_self_of_subset_left, ← x.2]

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
a : Cardinal.{max u v}
⊢ lift.{v, u} p.spanRank ≤ a ↔ ∃ s, lift.{v, u} #↑s ≤ a ∧ span R s = p

Tactic:
constructor
  · intro h
    obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p
    exact ⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩
  · exact fun ⟨s, ⟨h₁, h₂⟩⟩ ↦ h₂.symm ▸ (Cardinal.lift_le.mpr (spanRank_span_le_card s)).trans h₁

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_5
B : Type u_6
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A ≃ₐ[R] B
x : A
h : IsIntegral R (f x)
⊢ IsIntegral R x

Tactic:
simpa using h.map f.symm

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
⊢ ∑ x ∈ p.support, (monomial x) (f (g x)) = p

Tactic:
hg,

Goal state after:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := ∑ k ∈ p.support, (monomial k) (g k)
⊢ ∑ x ∈ p.support, (monomial x) (p.coeff x) = p
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: 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
⊢ (↑(expand K k) ((M ^ k).charmatrix i j)).coeff m = ((X ^ k).coeff m - if m = 0 then M ^ k else 0) i j

Tactic:
AlgHom.coe_toRingHom,

Goal state after:
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
⊢ ((expand K k) ((M ^ k).charmatrix i j)).coeff m = ((X ^ k).coeff m - if m = 0 then M ^ k else 0) i j