mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
hm : (fun x ↦ x • p) m' = n • y
this : NeZero n
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p

Tactic:
← (Int.divModEquiv n).symm_apply_apply m',

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
hm : (fun x ↦ x • p) ((Int.divModEquiv n).symm ((Int.divModEquiv n) m')) = n • y
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : S.X₁.isFinite
h₃ : S.X₃.isFinite
⊢ S.X₂.isFinite

Tactic:
by
    simp only [prop_isFinite_iff] at h₁ h₃ ⊢
    have hg := hS.epi_g
    rw [AddCommGrpCat.epi_iff_surjective] at hg
    obtain ⟨s, hs⟩ := hg.hasRightInverse
    have hφ : Function.Surjective (fun (x₁, x₃) ↦ S.f x₁ + s x₃) := fun x₂ ↦ by
      obtain ⟨x₁, hx₁⟩ := (ShortComplex.ab_exact_iff S).1 hS.exact (x₂ - s (S.g x₂))
        (by simp [hs (S.g x₂)])
      exact ⟨⟨x₁, S.g x₂⟩, by simp [hx₁]⟩
    exact Finite.of_surjective _ hφ

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : FloorRing 𝕜
x : 𝕜
⊢ ↑(Int.fract x) = ↑x

Tactic:
simp [← Int.self_sub_floor, mem_zmultiples_iff]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬∃ n_1, n_1 • p = ↑m * (p / ↑n)

Tactic:
rintro ⟨k, hk⟩

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : k • p = ↑m * (p / ↑n)
⊢ False
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ((a / ↑n * ↑n) • p + (a % ↑n) • p) / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑k

Tactic:
add_div,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : (a / ↑n * ↑n) • p / ↑n + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑k
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ y ≫ Cofork.π c = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
refine ⟨fun hy ↦ ?_, ?_⟩

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
⊢ (∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f) → y ≫ Cofork.π c = 0
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr.refine_2.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.δlast.Exact
h' : (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact
i : ℕ
hi✝¹ : i + 2 ≤ n + 2
hi✝ : i ≤ n
hi : i < n
⊢ (S.sc ⋯ i hi✝¹).Exact

Tactic:
exact h.exact i

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

Tactic:
· ext
    dsimp
    rw [← Functor.map_comp, X.counit, Functor.map_id]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case inl
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i k : Fin 2
hij : i ≤ i
hjk : i ≤ k
⊢ map f i k ⋯ = 𝟙 (obj X₀ X₁ i) ≫ map f i k hjk

Tactic:
id_comp

Goal state after:
case inl
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i k : Fin 2
hij : i ≤ i
hjk : i ≤ k
⊢ map f i k ⋯ = map f i k hjk
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.zero
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
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f 0 ⟨k, hk⟩ ⋯ = 𝟙 X ≫ map F f 0 ⟨k, hk⟩ hjk

Tactic:
id_comp

Goal state after:
case zero.zero
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
hi hj : 0 < n + 1 + 1
hjk : ⟨0, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨0, hj⟩
⊢ map F f 0 ⟨k, hk⟩ ⋯ = map F f 0 ⟨k, hk⟩ hjk
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
      · simp [Fin.ext_iff] at hjk
      · dsimp
        rw [← F.map_comp, homOfLE_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))

Tactic:
have : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
c : Cone (F ⋙ R)
h : IsLimit c
this : HasLimit (F ⋙ R)
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ c.ι.app j ≫ t.desc (newCocone D c) ≫ T.δ.app c.pt =
    c.ι.app j ≫ t.desc (newCocone D c) ≫ T.map (t.desc (newCocone D c))

Tactic:
simp only [Functor.comp_obj, forget_obj, IsColimit.fac_assoc,
      newCocone_ι_app, assoc, NatTrans.naturality, Functor.comp_map]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
j : J
⊢ (D.obj j).a ≫ T.δ.app (D.obj j).A ≫ T.map (T.map (c.ι.app j)) =
    (D.obj j).a ≫ T.map (c.ι.app j) ≫ T.map (t.desc (newCocone D c))
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
f g : A ⟶ B
s : B ⟶ A
sl : s ≫ f = 𝟙 B
sr : s ≫ g = 𝟙 B
F : C ⥤ D
⊢ F.map s ≫ F.map f = 𝟙 (F.obj B)

Tactic:
by simp only [← Functor.map_comp, sl, Functor.map_id]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ G.ι.app one = F.map right ≫ G.π

Tactic:
Cocone.w G right

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ G.ι.app one = G.ι.app one
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case insert
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ ((insert a s).inf f).IsPrimary

Tactic:
| insert a s ha IH =>

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
z : S
⊢ map_ideal M S I = Ideal.map (algebraMap R S) I

Tactic:
rw [map_ideal, Ideal.map, Ideal.span, Submodule.localized'_eq_span, Algebra.coe_linearMap]

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ a ⊗ₜ[R] ∑ a ∈ p.support, p.coeff a • X ^ a = a ⊗ₜ[R] p

Tactic:
conv_rhs => rw [← sum_C_mul_X_pow_eq p]

Goal state after:
case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ a ⊗ₜ[R] ∑ a ∈ p.support, p.coeff a • X ^ a = a ⊗ₜ[R] p.sum fun n a ↦ C a * X ^ n
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z) →
    ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x

Tactic:
rintro ⟨y, z, e⟩
    exact ⟨y, y.prop, _, ⟨z, z.prop, rfl⟩, e.symm⟩

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

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
⊢ (A ^ k)ᵀ = A ^ k

Tactic:
transpose_pow,

Goal state after:
α : Type u_1
n : Type u_3
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsSymm
k : ℕ
⊢ Aᵀ ^ k = A ^ k
Module: Mathlib.LinearAlgebra.Matrix.Polynomial

Goal state before:
pp: case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = 1

Tactic:
← @det_one n,

Goal state after:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = det 1
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:
rw [← T_add, sub_eq_add_neg]

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 α
i : n
⊢ Aᵀ.cramer (A i) = Pi.single i A.det

Tactic:
by
  ext j
  rw [cramer_apply, Pi.single_apply]
  split_ifs with h
  · -- i = j: this entry should be `A.det`
    subst h
    simp only [updateCol_transpose, det_transpose, updateRow_eq_self]
  · -- i ≠ j: this entry should be 0
    rw [updateCol_transpose, det_transpose]
    apply det_zero_of_row_eq h
    rw [updateRow_self, updateRow_ne (Ne.symm h)]

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

Goal state before:
pp: n : Type u_2
α : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring α
A : Matrix n n α
⊢ IsUnit Aᵀ ↔ IsUnit A

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
    (transposeInvertibleEquivInvertible A).nonempty_congr]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : IsEmpty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ Module.rank R R
⊢ False

Tactic:
rank_self

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
h : IsEmpty (OreLocalization.OreSet R⁰)
this : ℵ₀ ≤ 1
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
M✝ : Matrix n n α
⊢ f' (g M✝).adjugate = M✝.adjugate

Tactic:
RingHom.map_adjugate,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
M✝ : Matrix n n α
⊢ ((evalRingHom 0).mapMatrix (g M✝)).adjugate = M✝.adjugate
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
⊢ f' (g (A * B)).adjugate = f' (g A * g B).adjugate

Tactic:
RingHom.map_adjugate,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
⊢ ((evalRingHom 0).mapMatrix (g (A * B))).adjugate = f' (g A * g B).adjugate
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
⊢ ((evalRingHom 0).mapMatrix (g (A * B))).adjugate = f' (g A * g B).adjugate

Tactic:
RingHom.map_adjugate,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := (evalRingHom 0).mapMatrix
f'_inv : ∀ (M : Matrix n n α), f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), f' (g M).adjugate = M.adjugate
f'_g_mul : ∀ (M N : Matrix n n α), f' (g M * g N) = M * N
hu : ∀ (M : Matrix n n α), IsRegular (g M).det
⊢ ((evalRingHom 0).mapMatrix (g (A * B))).adjugate = ((evalRingHom 0).mapMatrix (g A * g B)).adjugate
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 2 + 1) • A'

Tactic:
h_card',

Goal state after:
case succ.succ
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h : Fintype.card n ≠ 1
n✝ : ℕ
h_card : Fintype.card n = n✝ + 1 + 1
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1
is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) A'.det
⊢ A'.det • A'.adjugate.adjugate = A'.det ^ (Fintype.card n - 1) • A'
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
have hnr : n < r := hk
    let n' : Fin r := ⟨n, hnr⟩
    have A :
      (listTransvecRow M)[n]? =
        ↑(transvection (inr unit) (inl n')
        (-M (inr unit) (inl n') / M (inr unit) (inr unit))) := by
      simp only [n', listTransvecRow, hnr, dif_pos, List.getElem?_ofFn]
    simp only [List.take_add_one, A, ← Matrix.mul_assoc, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
      have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]
      simp only [h, mul_transvection_apply_same, if_false,
        mul_listTransvecRow_last_col_take _ _ hnr.le, hni.le, this, if_true, IH hnr.le]
      field
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
      simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp [hi, n.le_succ.trans hi]
      · rw [if_neg, if_neg]
        · simpa only [not_le] using! hi
        · simpa only [hni.symm, not_le, or_false] using! Nat.lt_succ_iff_lt_or_eq.1 hi

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

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i ↦ b ↑i
h' : (M.toSquareBlockProp fun i ↦ b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
⊢ (M.toSquareBlockProp fun i ↦ ¬b i = k).det = ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det

Tactic:
ih _ (max'_mem _ _) h' hb'

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i ↦ b ↑i
h' : (M.toSquareBlockProp fun i ↦ b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
⊢ ∏ a ∈ (image b univ).erase ((image b univ).max' ⋯), ((M.toSquareBlockProp fun i ↦ b i ≠ k).toSquareBlock b' a).det =
    ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_3
inst✝ : CommRing R
M : Matrix n n R[X]
r : R
⊢ ((eval₂RingHom (RingHom.id R) r).mapMatrix M).det = (eval ((scalar n) r) (matPolyEquiv M)).det

Tactic:
exact congr_arg det <| ext fun _ _ ↦ matPolyEquiv_eval _ _ _ _ |>.symm

Goal state after:
Module: Mathlib.Tactic.LinearCombination.Lemmas

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : NoZeroDivisors α
n : ℕ
p : a = b
H : (a' - b') ^ n - (a - b) = 0
⊢ a' = b'

Tactic:
by
  rw [← sub_eq_zero] at p ⊢; apply eq_zero_of_pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent P → IsNilpotent (X * P)

Tactic:
rintro ⟨k, hk⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ IsNilpotent (X * P)
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsRight R
⊢ IsNilpotent (x * y) → IsNilpotent x

Tactic:
rintro ⟨k, hk⟩

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsRight R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent x
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsLeft R
⊢ IsNilpotent (x * y) → IsNilpotent y

Tactic:
rintro ⟨k, hk⟩

Goal state after:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsLeft R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent y
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), f x ∈ (Ideal.finsuppTotal ι M I b).range

Tactic:
Ideal.range_finsuppTotal,

Goal state after:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), f x ∈ I • Submodule.span R (Set.range b)
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')
⊢ ↑(1 * I) ≤ span R ↑T

Tactic:
← mul_one (span R (T : Set A))

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 * 1
Module: Mathlib.Data.Nat.Factorial.Cast

Goal state before:
pp: S : Type u_1
inst✝ : Ring S
a : ℕ
⊢ ↑(a.descFactorial 2) = ↑a * (↑a - 1)

Tactic:
descFactorial

Goal state after:
S : Type u_1
inst✝ : Ring S
a : ℕ
⊢ ↑((a - 1) * a.descFactorial 1) = ↑a * (↑a - 1)