mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.GrpWithZero

Goal state before:
pp: α β : GrpWithZero
e : α.carrier ≃* β.carrier
⊢ ofHom (MonoidWithZeroHom.ofClass e.symm) ≫ ofHom (MonoidWithZeroHom.ofClass e) = 𝟙 β

Tactic:
by
    ext
    exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
hS : S.Exact
⊢ S.δ₀.Exact

Tactic:
rw [exact_iff_δ₀] at hS
  exact hS.2

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ) →
    ∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ

Tactic:
· intro h A y₂ hy₂
    obtain ⟨A₁, π₁, hπ₁, γ, hγ⟩ := h (S₂.liftCycles y₂ hy₂ ≫ S₂.homologyπ)
    obtain ⟨A₂, π₂, hπ₂, x₂, hx₂, fac⟩ := S₁.eq_liftCycles_homologyπ_up_to_refinements γ
    replace hγ := π₂ ≫= hγ
    simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_liftCycles_assoc, liftCycles_comp_homologyπ_eq_iff_up_to_refinements] at hγ
    obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ := hγ
    exact ⟨A₃, π₃ ≫ π₂ ≫ π₁, inferInstance, π₃ ≫ x₂, by simp only [assoc, hx₂, comp_zero],
      x₁, by simpa only [assoc] using hx₁⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ (∀ ⦃A : C⦄ (y₂ : A ⟶ S₂.X₂),
      y₂ ≫ S₂.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f) →
    ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
Module: Mathlib.Algebra.Homology.ShortComplex.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
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.g))

Tactic:
by
  rw [← Preadditive.epi_iff_surjective]
  exact hS.epi_g

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ ({ f := s.ι.f ≫ T.ε.app X.A, h := ⋯ } ≫ (beckCoalgebraFork X).ι).f = s.ι.f

Tactic:
simpa [← T.ε.naturality_assoc, T.left_counit_assoc] using! h₁ =≫ T.ε.app ((T : C ⥤ C).obj X.A)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π (J.snd a)

Tactic:
by
  rw [← K.w (WalkingMultispan.Hom.snd a)]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: ⊢ ∀ {X Y : WalkingReflexivePair} (f : X.Hom Y), (Hom.id X).comp f = f

Tactic:
intro _ _ f

Goal state after:
X✝ Y✝ : WalkingReflexivePair
f : X✝.Hom Y✝
⊢ (Hom.id X✝).comp f = f
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: ⊢ ∀ {X Y : WalkingReflexivePair} (f : X.Hom Y), f.comp (Hom.id Y) = f

Tactic:
intro _ _ f

Goal state after:
X✝ Y✝ : WalkingReflexivePair
f : X✝.Hom Y✝
⊢ f.comp (Hom.id Y✝) = f
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
obtain _ | k := k

Goal state after:
case succ.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
hk : 0 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨0, hk⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨0, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨0, hk⟩ hjk

case succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
k : ℕ
hk : k + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k + 1, hk⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k + 1, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨k + 1, hk⟩ hjk
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✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ G.map (F.map (adj.unit.app Y)) ≫ G.map (adj.counit.app (F.1 ((𝟭 C).obj Y))) =
    𝟙 (G.obj ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))

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✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 ((𝟭 C).obj Y))) =
    𝟙 (G.obj ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))

Tactic:
· rw [← G.map_comp, ← G.map_id]
          exact congr_arg G.map (adj.left_triangle_components Y)

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✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 ((𝟭 C).obj Y))) =
    𝟙 (G.obj ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))
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
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ s • IsLocalizedModule.mk' f m s ∈ N'

Tactic:
Submonoid.smul_def,

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
N' : Submodule S N
m : M
s : ↥p
hn : Function.uncurry (IsLocalizedModule.mk' f) (m, s) ∈ N'
⊢ ↑s • IsLocalizedModule.mk' f m s ∈ N'
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
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ 1 ∈ I

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_comap] at hM

Goal state after:
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
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : (algebraMap R S) m ∈ I
⊢ 1 ∈ I
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ mk' S 1 1 = 0

Tactic:
mk'_eq_zero_iff

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ∃ m, ↑m * 1 = 0
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
n : Submodule R N
x : M
hx : x ∈ m
y : N
⊢ ((n.liftQ ((mk R M N).flip.compr₂ ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ)
              ⋯).flip
          x ∘ₗ
        n.mkQ)
      y =
    (0 ∘ₗ n.mkQ) y

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, LinearMap.flip_apply,
        Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, LinearMap.zero_comp,
        LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero]

Goal state after:
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
n : Submodule R N
x : M
hx : x ∈ m
y : N
⊢ x ⊗ₜ[R] y ∈ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
p : R[X]
⊢ (eval₂ f x) (toLaurent p) = Polynomial.eval₂ f (↑x) p

Tactic:
unfold eval₂
  rw [← algebraMap_eq_toLaurent, IsLocalization.lift_eq, coe_eval₂RingHom]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ 1 = (↑x * ↑x⁻¹) ^ n

Tactic:
Units.mul_inv,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ 1 = 1 ^ n
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
k : ℕ
hk : k ≤ r
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
by
  induction hk using Nat.decreasingInduction with
  | of_succ n hn IH =>
    have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
    rw [List.drop_eq_getElem_cons hn']
    simpa [listTransvecCol, Matrix.mul_assoc]
  | self =>
    simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
      Matrix.one_mul]

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

Goal state before:
pp: α : Type u_3
m : Type u_10
n : Type u_11
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
a b : ℕ
⊢ (diagonal fun mn ↦ ↑a * ↑b) = ↑(a * b)

Tactic:
by simp_rw [← Nat.cast_mul]; rfl

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✝⁴ : 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 + C * V * ⅟A * U * C)
⊢ 1 - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A * A +
      (⅟A * (U * C * V) - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A * (U * C * V)) =
    1

Tactic:
sub_add,

Goal state after:
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 + C * V * ⅟A * U * C)
⊢ 1 -
      (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A * A -
        (⅟A * (U * C * V) - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A * (U * C * V))) =
    1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
⊢ IsUnit (diagonal v) ↔ IsUnit v

Tactic:
by
  simp only [← nonempty_invertible_iff_isUnit,
    (diagonalInvertibleEquivInvertible v).nonempty_congr]

Goal state after:
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 | H s ih =>
  subst hs
  cases isEmpty_or_nonempty m
  · simp
  let k := (univ.image b).max' (univ_nonempty.image _)
  rw [twoBlockTriangular_det' M fun i => b i = k]
  · have : univ.image b = insert k ((univ.image b).erase k) := by
      rw [insert_erase]
      apply max'_mem
    rw [this, prod_insert (notMem_erase _ _)]
    refine congr_arg _ ?_
    let b' := fun i : { a // b a ≠ k } => b ↑i
    have h' : BlockTriangular (M.toSquareBlockProp fun i => b i ≠ k) b' := hM.submatrix
    have hb' : image b' univ = (image b univ).erase k := by
      convert! image_subtype_ne_univ_eq_image_erase k b
    rw [ih _ (max'_mem _ _) h' hb']
    refine Finset.prod_congr rfl fun l hl => ?_
    let he : { a // b' a = l } ≃ { a // b a = l } :=
      haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl)
      Equiv.subtypeSubtypeEquivSubtype @hc
    rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm]
    rfl
  · intro i hi j hj
    apply hM
    rw [hi]
    apply lt_of_le_of_ne _ hj
    exact Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))

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

Goal state before:
pp: case succ
𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
e : n ≃ Fin r ⊕ Unit
⊢ ∃ L L' D, (List.map toMatrix L).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L').prod = diagonal D

Tactic:
apply
      exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction fun N =>
        IH (Fin r) N (by simp)

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 A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A + 0) (⅟A * B + -(⅟A * B * ⅟D) * D) (0 * A + 0) (0 * B + ⅟D * D) = 1

Tactic:
Matrix.zero_mul,

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 A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A + 0) (⅟A * B + -(⅟A * B * ⅟D) * D) (0 + 0) (0 + ⅟D * 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 α
C : Matrix n m α
D : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A + 0 * C) (0 + 0 * D) (-(⅟D * C * ⅟A) * A + ⅟D * C) (0 + ⅟D * D) = 1

Tactic:
Matrix.zero_mul,

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 A
inst✝ : Invertible D
⊢ fromBlocks (⅟A * A + 0) (0 + 0) (-(⅟D * C * ⅟A) * A + ⅟D * C) (0 + ⅟D * D) = 1
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelAddMonoid α
p : a = b
H : a' + b < b' + a
⊢ a' < b'

Tactic:
by
  rwa [p, add_lt_add_iff_right] at H

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 α
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)).toBlocks₂₂ =
    toBlocks₂₂ 1
⊢ (⅟(fromBlocks A 0 C D)).toBlocks₂₂ * D = 1

Tactic:
simpa only [Matrix.toBlocks_fromBlocks₂₂, Matrix.mul_zero, zero_add, ← fromBlocks_one] using
        this

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 α
i : Invertible A × Invertible D
⊢ Invertible (fromBlocks A B 0 D)

Tactic:
by
    letI := i.1
    letI := i.2
    exact fromBlocksZero₂₁Invertible A B D

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

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A B 0 D)
⊢ 0 = fromBlocks 0 (-(0 * B * 0)) 0 0

Tactic:
Matrix.zero_mul,

Goal state after:
case neg
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A B 0 D)
⊢ 0 = fromBlocks 0 (-0) 0 0
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A 0 C D)
⊢ 0 = fromBlocks 0 0 (-(0 * C * 0)) 0

Tactic:
Matrix.zero_mul,

Goal state after:
case neg
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A 0 C D)
⊢ 0 = fromBlocks 0 0 (-0) 0
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r + 1)

Tactic:
by
  rw [← IsUnit.neg_iff, neg_add']
  exact isUnit_sub_one hnil.neg

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

Goal state before:
pp: case insert
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (∑ i ∈ insert j s, f i)

Tactic:
Finset.sum_insert hj

Goal state after:
case insert
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (f j + ∑ x ∈ s, f x)
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x : B
n : ℕ
hn : 0 < n
hx : IsIntegral R (x ^ n)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R B) (x ^ n) p = 0
⊢ eval₂ (algebraMap R B) x ((expand R n) p) = 0

Tactic:
rwa [← aeval_def, expand_aeval]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ (aeval x) (p₁ * p₂) = 0

Tactic:
aeval_prod_apply,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A × B
p₁ : R[X]
hp₁Monic : p₁.Monic
hp₁Eval : (aeval x.1) p₁ = 0
p₂ : R[X]
hp₂Monic : p₂.Monic
hp₂Eval : (aeval x.2) p₂ = 0
⊢ ((aeval x.1) (p₁ * p₂), (aeval x.2) (p₁ * p₂)) = 0
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
⊢ ((diagonal fun i ↦ 1) - t_inv • M.map ⇑LaurentPolynomial.C).det = invert q

Tactic:
diagonal_one,

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
⊢ (1 - t_inv • M.map ⇑LaurentPolynomial.C).det = invert q