mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType (X₁ ⨯ X₂)
⊢ ((prodEquiv X₁ X₂) x).1 = (hom prod.fst) x

Tactic:
simpa using! congr_hom (prodComparison_fst (forget C) X₁ X₂) x

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: case mpr
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Epi ((forget₂ C Ab).map f) → Epi f

Tactic:
apply Functor.epi_of_epi_map

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Fan f
r : R
x : ↑s.1
⊢ (fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) (r • x)) =
    (RingHom.id R) r • fun j ↦ (ConcreteCategory.hom (s.π.app { as := j })) x

Tactic:
simp only [Functor.const_obj_obj, map_smul]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ R.map (L.map (R.map f) ≫ h.counit.app Y✝) = R.map (h.counit.app X✝) ≫ R.map f

Tactic:
Adjunction.counit_naturality,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ R.map (h.counit.app X✝ ≫ f) = R.map (h.counit.app X✝) ≫ R.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasReflexiveCoequalizers C
A B : C
f g : A ⟶ B
r : B ⟶ A
rf : r ≫ f = 𝟙 B
rg : r ≫ g = 𝟙 B
⊢ HasCoequalizer f g

Tactic:
by
  let := IsReflexivePair.mk' r rf rg
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : CreatesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ HasLimit (parallelPair f g ⋙ F)

Tactic:
rw [hasLimit_iff_of_iso (diagramIsoParallelPair _)]

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : CreatesLimitOfIsCosplitPair F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ HasLimit
    (parallelPair ((parallelPair f g ⋙ F).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ F).map WalkingParallelPairHom.right))
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
⊢ a • S = comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S

Tactic:
ext
  simp [pointwise_smul_def]
  rfl

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid 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
M' M'' : Submodule R M
r : R
x : N
⊢ x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x} →
    r • x ∈ {x | ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = x}

Tactic:
by
    rintro ⟨m, hm, s, hx⟩
    exact ⟨r • m, smul_mem M' _ hm, s, by rw [IsLocalizedModule.mk'_smul, hx]⟩

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ localized₀ p f ⊥ = ⊥

Tactic:
rw [← le_bot_iff]

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ localized₀ p f ⊥ ≤ ⊥
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ IsRadical y ↔ (Ideal.span {y}).IsRadical

Tactic:
simp_rw [IsRadical, ← Ideal.mem_span_singleton]

Goal state after:
R : Type u_1
y : R
inst✝ : CommSemiring R
⊢ (∀ (n : ℕ) (x : R), x ^ n ∈ Ideal.span {y} → x ∈ Ideal.span {y}) ↔ (Ideal.span {y}).IsRadical
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrimary
⊢ I.minimalPrimes = {I.radical}

Tactic:
ext J
  constructor
  · intro H
    have le := H.out.isPrime.radical_le_iff.mpr H.le
    exact (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ le).antisymm le
  · rintro (rfl : J = I.radical)
    exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid 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
M' M'' : Submodule R M
x : ↥p
⊢ IsUnit ((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)

Tactic:
simp_rw [Module.End.isUnit_iff]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid 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
M' M'' : Submodule R M
x : ↥p
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
I p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
hI : p ∈ I.minimalPrimes
J : Ideal S
hJP : J ≤ P
hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes
q : Ideal S
x✝ : (fun q ↦ q.IsPrime ∧ map (algebraMap R S) I ⊔ J ≤ q) q
hqle : q ≤ P
left✝ : q.IsPrime
hleq : map (algebraMap R S) I ⊔ J ≤ q
⊢ P ≤ q

Tactic:
simp only [sup_le_iff] at hleq
    have h1 : p.map (algebraMap R S) ≤ q := by
      rw [Ideal.map_le_iff_le_comap]
      refine hI.2 ⟨inferInstance, le_trans Ideal.le_comap_map (Ideal.comap_mono hleq.1)⟩ ?_
      convert! Ideal.comap_mono hqle
      exact Ideal.LiesOver.over
    have h2 : P.map (Ideal.Quotient.mk (p.map (algebraMap R S))) ≤
        q.map (Ideal.Quotient.mk (p.map (algebraMap R S))) :=
      hJ.2 ⟨Ideal.isPrime_map_quotientMk_of_isPrime h1, Ideal.map_mono hleq.2⟩
        (Ideal.map_mono hqle)
    simpa [h1] using Ideal.comap_mono (f := Ideal.Quotient.mk (p.map (algebraMap R S))) h2

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

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
inst✝ : IsLocalization M S
I : Ideal R
x : R
⊢ (algebraMap R S) x ∈ Ideal.map (algebraMap R S) I ↔ ∃ m ∈ M, m * x ∈ I

Tactic:
by
  rw [← IsLocalization.mk'_one (M := M), mk'_mem_map_algebraMap_iff]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case h
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ map (mk (I ^ n)) I ^ n = 0

Tactic:
simp [← Ideal.map_pow]

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

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
inst✝ : IsLocalization M S
⊢ ∀ {a b : Ideal S},
    { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } a ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } b ↔ a ≤ b

Tactic:
by
    rintro J₁ J₂
    constructor
    · exact fun hJ => (map_under M S) J₁ ▸ (map_under M S) J₂ ▸ Ideal.map_mono hJ
    · exact fun hJ => Ideal.comap_mono hJ

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e :
  (algebraMap R (Localization.Away s)) x * (algebraMap R (Localization.Away s)) (s ^ n) =
    (algebraMap R (Localization.Away s)) ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
rw [← map_mul, IsLocalization.eq_iff_exists (.powers s)] at e

Goal state after:
case a
R : Type u_1
inst✝ : CommSemiring R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e : ∃ c, ↑c * (x * s ^ n) = ↑c * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
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.AtPrime P (f P)
Nₚ : (P : Ideal R) → [P.IsMaximal] → Type u_7
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Nₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Nₚ P)
g : (P : Ideal R) → [inst : P.IsMaximal] → N →ₗ[R] Nₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (g P)
Lₚ : (P : Ideal R) → [P.IsMaximal] → Type u_8
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Lₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Lₚ P)
h : (P : Ideal R) → [inst : P.IsMaximal] → L →ₗ[R] Lₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (h P)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (J : Ideal R) [inst : J.IsMaximal],
    Function.Exact ⇑((IsLocalizedModule.map J.primeCompl (f J) (g J)) F)
      ⇑((IsLocalizedModule.map J.primeCompl (g J) (h J)) G)
⊢ Function.Exact ⇑F ⇑G

Tactic:
by
  simp only [LinearMap.exact_iff] at H ⊢
  apply eq_of_localization₀_maximal Nₚ g
  intro J hJ
  rw [← LinearMap.range_localizedMap_eq_localized₀_range _ (f J) (g J) F,
    ← LinearMap.ker_localizedMap_eq_localized₀_ker J.primeCompl (g J) (h J) G]
  have := SetLike.ext_iff.mp <| H J
  ext x
  simp only [mem_range, mem_ker] at this ⊢
  exact this x

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case surj
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
s t : S
ht : t ∈ adjoin R ↑σ
ht' : IsUnit t
h : s * t ∈ adjoin R ↑σ
⊢ ∃ x, s * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

Tactic:
exact ⟨⟨⟨_, h⟩, ⟨t, ht⟩, ht'⟩, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ coeSubmodule S ⊤ = 1

Tactic:
by
  rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Type u_3
A : Matrix n n α
h : A.IsSymm
f : α → β
⊢ (A.map f).IsSymm

Tactic:
by
  rw [IsSymm, ← transpose_map, h.eq]

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

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D).IsSymm

Tactic:
unfold Matrix.IsSymm

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m - n) = T m * T (-n)

Tactic:
by rw [← T_add, sub_eq_add_neg]

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

Goal state before:
pp: case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
have : (∏ j' : n, updateCol A j (Pi.single i 1) (σ j') j') = 0 := by
      apply prod_eq_zero (mem_univ j)
      rw [updateCol_self, Pi.single_eq_of_ne' h]

Goal state after:
case neg
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
h : ¬i = σ j
this : ∏ j', A.updateCol j (Pi.single i 1) (σ j') j' = 0
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ (T n).degree = (C 1 * T n).degree

Tactic:
by rw [map_one, one_mul]

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

Goal state before:
pp: 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
⊢ finrank T P = finrank R M

Tactic:
simpa using! congr_arg toNat bc.lift_rank_eq

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Tactic:
simpa using mul_listTransvecRow_last_col_take M i le_rfl

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

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

Tactic:
cases h.nonempty_invertible

Goal state after:
case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A.det
⊢ A⁻¹.det = A.det⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝ : Invertible (diagonal v)
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ

Tactic:
cases h.nonempty_invertible

Goal state after:
case pos.intro.intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝¹ : Invertible (diagonal v)
val✝ : Invertible v
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case pos
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
⊢ (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁

Tactic:
cases h.nonempty_invertible

Goal state after:
case pos.intro
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
⊢ (A.submatrix ⇑e₁ ⇑e₂)⁻¹ = A⁻¹.submatrix ⇑e₂ ⇑e₁
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✝ : LinearOrder α
hM : M.BlockTriangular b
s : Finset α
hs : image b univ = s
⊢ M.det = ∏ a ∈ s, (M.toSquareBlock b a).det

Tactic:
induction s using Finset.eraseInduction generalizing m with

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

Goal state before:
pp: m : Type u_3
R : Type v
M : Matrix m m R
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
h : M.IsUpperTriangular
this : DecidableEq R
⊢ M.det = ∏ i, M i i

Tactic:
simp_rw [h.det, image_id, det_toSquareBlock_id]

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

Goal state before:
pp: case neg.inr
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : ¬IsUnit A.det
h✝ : Nonempty n
hAB : ¬IsUnit (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

Tactic:
rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]

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
α : Type u_5
inst✝ : Preorder α
M : Matrix n n R
b : n → α
⊢ M.charmatrix.BlockTriangular b ↔ M.BlockTriangular b

Tactic:
rw [charmatrix, scalar_apply, RingHom.mapMatrix_apply, (blockTriangular_diagonal _).sub_iff_right]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
n : Type u_4
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α : Type u_5
inst✝ : Preorder α
M : Matrix n n R
b : n → α
⊢ (M.map ⇑C).BlockTriangular b ↔ M.BlockTriangular b
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
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)

Tactic:
let := fromBlocks₂₂Invertible A B C D

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
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
this : Invertible (fromBlocks A B C D) := A.fromBlocks₂₂Invertible B C D
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)
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) = ↑b ! / (↑a ! * ↑(b - a)!)

Tactic:
rw [eq_div_iff_mul_eq (mul_ne_zero this this)]

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 !
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ (m + n).choose k = ((X + 1) ^ (m + n)).coeff k

Tactic:
coeff_X_add_one_pow,

Goal state after:
m n k : ℕ
⊢ (m + n).choose k = ↑((m + n).choose k)
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
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ p * invert (T (↑(Fintype.card n) * 1)) = invert q

Tactic:
← T_pow,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
t : R[T;T⁻¹] := T 1
t_inv : R[T;T⁻¹] := T (-1)
p : R[T;T⁻¹] := ((scalar n) t - M.map ⇑LaurentPolynomial.C).det
q : R[T;T⁻¹] := (1 - (scalar n) t * M.map ⇑LaurentPolynomial.C).det
ht : t_inv * t = 1
hp : toLaurentAlg M.charpoly = p
hq : toLaurentAlg M.charpolyRev = q
this : t_inv ^ Fintype.card n * p = invert q
⊢ p * invert (T 1 ^ Fintype.card n) = invert q
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: G : Type u_1
R : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing K
inst✝³ : Algebra R K
inst✝² : Group G
inst✝¹ : MulSemiringAction G K
inst✝ : SMulCommClass G R K
g : G
x y : ↥(integralClosure R K)
⊢ ↑(g • (x + y)) = ↑(g • x + g • y)

Tactic:
exact smul_add g (x : K) (y : K)

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
hM : IsNilpotent M
⊢ IsNilpotent (M.charpoly - X ^ Fintype.card n)

Tactic:
nontriviality R
  let p : R[X] := M.charpolyRev
  have hp : p - 1 = X * (p /ₘ X) := by
    conv_lhs => rw [← modByMonic_add_div p X]
    simp [p, modByMonic_X]
  have : IsNilpotent (p /ₘ X) :=
    (Polynomial.isUnit_iff'.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
  have aux : (M.charpoly - X ^ (Fintype.card n)).natDegree ≤ M.charpoly.natDegree :=
    le_trans (natDegree_sub_le _ _) (by simp)
  rw [← isNilpotent_reflect_iff aux, reflect_sub, ← reverse, M.reverse_charpoly]
  simpa [p, hp]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
r : R
hk : 0 < k
⊢ (hasseDeriv k) (C r) = 0

Tactic:
by
  rw [← monomial_zero_left, hasseDeriv_monomial, Nat.choose_eq_zero_of_lt hk, Nat.cast_zero,
    zero_mul, monomial_zero_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
i : ℕ
⊢ (p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)

Tactic:
by
  simp +contextual [scaleRoots, coeff_monomial]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
h : n ≤ (p * q).natDegree
⊢ r ^ (p.natDegree + q.natDegree - (p * q).natDegree) * ((p * q).coeff n * r ^ ((p * q).natDegree - n)) =
    (p * q).coeff n * r ^ (p.natDegree + q.natDegree - n)

Tactic:
| inr h =>

Goal state after: