mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} D₁
inst✝³ : Category.{v_5, u_5} D₂
inst✝² : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
T₁₂ : C₁ ⥤ C₃
B₁₂ : D₁ ⥤ D₃
eT : T₁ ⋙ T₂ ≅ T₁₂
eB : B₁ ⋙ B₂ ≅ B₁₂
inst✝¹ : B₁.EssSurj
inst✝ : w.GuitartExact
h : (w.hComp' w' eT eB).GuitartExact
⊢ w'.GuitartExact

Tactic:
by
  dsimp [TwoSquare.hComp'] at h
  rw [whiskerHorizontal_iff] at h
  exact of_hComp w w'

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex.Plus (InjectiveObject C)
f : K ⟶ L
⊢ IsIso ((quotient (InjectiveObject C)).map f) ↔
    CochainComplex.Plus.quasiIso C ((InjectiveObject.ι C).mapCochainComplexPlus.map f)

Tactic:
rw [← isIso_iff_of_reflects_iso _ (HomotopyCategory.Plus.ι (InjectiveObject C)),
    ← isIso_iff_of_reflects_iso _ (Functor.mapHomotopyCategory (InjectiveObject.ι C) (.up ℤ))]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex.Plus (InjectiveObject C)
f : K ⟶ L
⊢ IsIso
      (((InjectiveObject.ι C).mapHomotopyCategory (ComplexShape.up ℤ)).map
        ((ι (InjectiveObject C)).map ((quotient (InjectiveObject C)).map f))) ↔
    CochainComplex.Plus.quasiIso C ((InjectiveObject.ι C).mapCochainComplexPlus.map f)
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : Int.ofNat n + 1 ≠ Int.ofNat m
⊢ ¬(ComplexShape.up ℕ).Rel n m

Tactic:
simp at hnm ⊢; lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n✝ m✝ : ℤ
n m : ℕ
hnm : Int.negSucc n + 1 ≠ Int.negSucc m
⊢ ¬(ComplexShape.down ℕ).Rel n m

Tactic:
simp at hnm ⊢; lia

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
inst✝ : Projective Z
n✝ : ℕ
⊢ Projective (((single₀ C).obj Z).X (n✝ + 1))

Tactic:
apply IsZero.projective
      apply HomologicalComplex.isZero_single_obj_X
      simp

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: case pos
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
j : J
s : Cofan ((((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).mapObjFun p j)
i : I
j' : J
h : (i, j') ∈ p ⁻¹' {j}
hi : i = 0
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(i, j'), h⟩ ≫
      e.inv.app (Y j) ≫ (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫ s.inj ⟨(0, j), ⋯⟩ =
    s.inj ⟨(i, j'), h⟩

Tactic:
subst hi
        simp only [Set.mem_preimage, hp, Set.mem_singleton_iff] at h
        subst h
        simp

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

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • φ₁.τ₂ = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂

Tactic:
h.comm₂

Goal state after:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) = S₁.g ≫ (a • h.h₂) + (a • h.h₁) ≫ S₂.f + a • φ₂.τ₂
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
X Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ (mapMap
      (((mapBifunctor (curriedTensor C) I I).map (𝟙 X)).app Y ≫ ((mapBifunctor (curriedTensor C) I I).obj X).map (𝟙 Y))
      fun x ↦ x.1 + x.2) =
    𝟙 (tensorObj X Y)

Tactic:
simp only [Functor.map_id, NatTrans.id_app, comp_id, mapMap_id]

Goal state after:
I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
X Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ 𝟙 ((((mapBifunctor (curriedTensor C) I I).obj X).obj Y).mapObj fun x ↦ x.1 + x.2) = 𝟙 (tensorObj X Y)
Module: Mathlib.Algebra.Homology.SpectralObject.Basic

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.H n₀).map (homMk₂ (α.app 0) (α.app 1) (β.app 1) ⋯ ⋯) ≫
      (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.H n₁).map (homMk₂ (α.app 0) (α.app 1) (β.app 1) ⋯ ⋯)
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α

Tactic:
dsimp at h

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_3, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
i' j' k' : ι
f' : i' ⟶ j'
g' : j' ⟶ k'
α : mk₁ f ⟶ mk₁ f'
β : mk₁ g ⟶ mk₁ g'
n₀ n₁ : ℤ
hαβ : α.app 1 = β.app 0
hn₁ : n₀ + 1 = n₁
h :
  (X.H n₀).map (homMk₁ (α.app 1) (β.app 1) ⋯) ≫ (X.δ' n₀ n₁ hn₁).app (mk₂ f' g') =
    (X.δ' n₀ n₁ hn₁).app (mk₂ f g) ≫ (X.H n₁).map (homMk₁ (α.app 0) (α.app 1) ⋯)
⊢ (X.H n₀).map β ≫ X.δ f' g' n₀ n₁ hn₁ = X.δ f g n₀ n₁ hn₁ ≫ (X.H n₁).map α
Module: Mathlib.CategoryTheory.GradedObject.Monoidal

Goal state before:
pp: I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝² : X₃.HasTensor X₄
inst✝¹ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + i₂₃₄ = j

Tactic:
rw [← hi, ← add_assoc, ← add_assoc, h]

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₂ = data.i₀ r pq ⋯

Tactic:
by rw [hi₂, data.hc₀₂ r _ _ h]

Goal state after:
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n : M
t : R
x m : L
⊢ -⁅m, t • x⁆ = t • ⁅x, m⁆

Tactic:
← lie_skew x m,

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
t✝ : R
x✝ y z : L
m✝ n : M
t : R
x m : L
⊢ -⁅m, t • x⁆ = t • -⁅m, x⁆
Module: Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
κ : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Preorder ι
X : SpectralObject C ι
c : ℤ → ComplexShape κ
r₀ : ℤ
data : SpectralSequenceDataCore ι c r₀
r r' : ℤ
hrr' : r + 1 = r'
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).prev pq' = pq
i₀ i₁ i₂ i₃ i₃' : ι
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ pq'
hi₃ : i₃ = data.i₃ r pq' ⋯
hi₃' : i₃' = data.i₃ r' pq' ⋯
n₀ n₁ n₂ : ℤ
hn₁' : n₁ = data.deg pq'
inst✝ : X.HasSpectralSequence data
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h : (c r).Rel pq pq'
⊢ i₂ = data.i₀ r pq ⋯

Tactic:
by rw [hi₂, data.hc₀₂ r _ _ h]

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
this : ∀ (s : Set L), lieSpan R L (-s) ≤ lieSpan R L s
⊢ lieSpan R L s ≤ lieSpan R L (-s)

Tactic:
simpa using (this (-s))

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s✝ s : Set L
x : L
⊢ 0 ∈ lieSpan R L s

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ ⟨0, ⋯⟩ ∈ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.Algebra.Lie.Subalgebra

Goal state before:
pp: case a.zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
ι : Type u_1
f : ι → ↥K
x : L
⊢ 0 ∈ map K.incl (lieSpan R (↥K) (range f))

Tactic:
exact zero_mem _

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
m : M
hm : m ∈ ↑N
N' : Submodule R M
hN' : ∀ p ∈ {x | ∃ s, (∃ x ∈ N, lieSpan R L {x} = s) ∧ ↑s = x}, p ≤ N'
⊢ ∀ m ∈ N, ↑(lieSpan R L {m}) ≤ N'

Tactic:
simpa using hN'

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
p : A[X]
pmonic : p.Monic
hp : (Polynomial.aeval x) p = 0
⊢ (minpoly A x).degree ≤ p.degree

Tactic:
delta minpoly; split_ifs with hx
  · refine le_of_not_gt <| degree_lt_wf.not_lt_min _ ?_
    exact ⟨pmonic, hp⟩
  · simp only [degree_zero, bot_le]

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: F : Type u_3
E : Type u_4
A : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : CommRing A
inst✝³ : Algebra F E
inst✝² : Algebra E A
inst✝¹ : Algebra F A
inst✝ : IsScalarTower F E A
a : A
ha : IsIntegral F a
h : minpoly E a ∈ lifts (algebraMap F E)
⊢ map (algebraMap F E) (minpoly F a) = minpoly E a

Tactic:
by
  refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic ha.tower_top)
    ((algebraMap F E).injective.monic_map_iff.mp <| minpoly.monic ha)
    (minpoly.dvd E a (by simp)) ?_
  obtain ⟨g, hg, hgdeg, hgmon⟩ := lifts_and_natDegree_eq_and_monic h (minpoly.monic ha.tower_top)
  rw [natDegree_map, ← hgdeg]
  refine natDegree_le_of_dvd (minpoly.dvd F a ?_) hgmon.ne_zero
  rw [← aeval_map_algebraMap A, IsScalarTower.algebraMap_eq F E A, ← coe_mapRingHom,
    ← mapRingHom_comp, RingHom.comp_apply, coe_mapRingHom, coe_mapRingHom, hg,
    aeval_map_algebraMap, minpoly.aeval]

Goal state after:
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case f
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| I.incl

pp: case J
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
next => skip

Goal state after:
case J
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
| ⁅I ⊓ I₁, I ⊓ I₂⁆
Module: Mathlib.Algebra.Jordan.Basic

Goal state before:
pp: A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ 2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆) = 0

Tactic:
symm
  calc
    0 = ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ := by
      rw [(commute_lmul_lmul_sq (a + b + c)).lie_eq]
    _ = _ := by rw [aux0, aux1, aux2, aux3, nsmul_add, nsmul_add]

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (X - C a) = 0
⊢ (mk (X - C a)) X = 0

Tactic:
mk_X,

Goal state after:
K : Type u
inst✝ : Field K
a : K
ha : a ≠ 0
hn : 0 < Nat.succ 0
e : root (X - C a) = 0
⊢ root (X - C a) = 0
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
⊢ Function.LeftInverse
    (eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map C I)).comp C) ⋯) fun i ↦
      (Ideal.Quotient.mk (Ideal.map C I)) (X i))
    ⇑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)

Tactic:
intro f
  obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
  apply induction_on f
  · intro r
    rw [Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply, eval₂_C, Ideal.Quotient.lift_mk,
      RingHom.comp_apply]
  · intro p q hp hq
    rw [Ideal.Quotient.lift_mk] at hp hq ⊢
    simp only [eval₂_add, map_add, coe_eval₂Hom] at hp hq ⊢
    rw [hp, hq]
  · intro p i hp
    simp only [coe_eval₂Hom, Ideal.Quotient.lift_mk,
      eval₂_mul, map_mul, eval₂_X] at hp ⊢
    simp only [hp]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
hderiv : derivative f = C b
⊢ C e * C b = 1

Tactic:
← map_mul,

Goal state after:
R : Type u
inst✝ : CommRing R
n : ℕ
a b c : R
hn : ↑n = 0
hb✝ : IsUnit b
f : R[X] := C a * X ^ n + C b * X + C c
e : R
hb : e * b = 1
hderiv : derivative f = C b
⊢ C (e * b) = 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case pos.hMM'
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix b (b.map e)) ↑e * (toMatrix (b.map e) b) ↑e.symm = 1

pp: case pos.hM'M
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix (b.map e) b) ↑e.symm * (toMatrix b (b.map e)) ↑e = 1

Tactic:
· rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]

Goal state after:
case pos.hM'M
M : Type u_2
inst✝⁴ : AddCommGroup M
A : Type u_5
inst✝³ : CommRing A
inst✝² : Module A M
N : Type u_7
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
⊢ (toMatrix (b.map e) b) ↑e.symm * (toMatrix b (b.map e)) ↑e = 1
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p 1) x = x ^ p

Tactic:
rw [iterateFrobeniusEquiv_def, pow_one]

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: case prime.inr
K : Type u_1
p : ℕ
inst✝² : Field K
inst✝¹ : ExpChar K p
inst✝ : PerfectRing K p
hp : Nat.Prime p
hchar✝ : CharP K p
g : K[X]
hf : Irreducible ((expand K p) g)
⊢ ((expand K p) g).Separable

Tactic:
exfalso; revert hf; have := Fact.mk hp; simp

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ (map (algebraMap F K) f).Separable ↔ f.Separable

Tactic:
separable_map

Goal state after:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
f : F[X]
hf : f ≠ 0
h : (map (algebraMap F K) f).Splits
⊢ f.Separable ↔ f.Separable
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst✝¹ : CommRing R
f g✝ : R[X]
inst✝ : CommRing S
i : R →+* S
x : S
h : eval₂ i x f = 0
g : R[X]
H : g ∈ span {f}
y : R[X]
hy : g = f * y
⊢ (eval₂RingHom i x) g = 0

Tactic:
rw [hy, map_mul, coe_eval₂RingHom, h, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ f ((algebraMap R (AdjoinRoot (C r * X - 1))) r) * f (root (C r * X - 1)) = 1

Tactic:
← map_mul,

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ f ((algebraMap R (AdjoinRoot (C r * X - 1))) r * root (C r * X - 1)) = 1
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ g ((algebraMap R (AdjoinRoot (C r * X - 1))) r) * g (root (C r * X - 1)) = 1

Tactic:
← map_mul,

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ g ((algebraMap R (AdjoinRoot (C r * X - 1))) r * root (C r * X - 1)) = 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : Nontrivial R
h : e.det = 0
⊢ False

Tactic:
simpa [h] using e.det_self

Goal state after:
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: case inr.inl
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j : n
k : m
⊢ W.mkQ (e ↑(bW k)) = 0

Tactic:
← LinearMap.mem_ker,

Goal state after:
case inr.inl
R : Type u_6
V : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
W : Submodule R V
inst✝² : Free R ↥W
inst✝¹ : Module.Finite R ↥W
inst✝ : Free R (V ⧸ W)
e : V →ₗ[R] V
he : W ≤ comap e W
m : Type u_7 := Free.ChooseBasisIndex R ↥W
bW : Basis m R ↥W := Free.chooseBasis R ↥W
n : Type u_7 := Free.ChooseBasisIndex R (V ⧸ W)
bQ : Basis n R (V ⧸ W) := Free.chooseBasis R (V ⧸ W)
b : Basis (m ⊕ n) R V := bW.sumQuot bQ
A : Matrix m m R := (toMatrix bW bW) (e.restrict he)
B : Matrix m n R := of fun i l ↦ ((bW.sumQuot bQ).repr (e ((bW.sumQuot bQ) (Sum.inr l)))) (Sum.inl i)
D : Matrix n n R := (toMatrix bQ bQ) (W.mapQ W e he)
j : n
k : m
⊢ e ↑(bW k) ∈ W.mkQ.ker
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := max n₁ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
⊢ ?m.193

Tactic:
by
    calc ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • (a + b) ^ i
        = ∑ i ∈ R2N, (i ! : ℚ)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * i.choose j := ?_
      _ = ∑ i ∈ R2N, (∑ j ∈ range (i + 1),
            ((j ! : ℚ)⁻¹ * ((i - j) ! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_
      _ = ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N,
            ((ij.1 ! : ℚ)⁻¹ * (ij.2 ! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
    · refine sum_congr rfl fun i _ ↦ ?_
      rw [Commute.add_pow h₁ i]
    · simp_rw [smul_sum]
      refine sum_congr rfl fun i hi ↦ sum_congr rfl fun j hj ↦ ?_
      simp only [mem_range] at hi hj
      replace hj := Nat.le_of_lt_succ hj
      suffices (i ! : ℚ)⁻¹ * (i.choose j) = ((j ! : ℚ)⁻¹ * ((i - j)! : ℚ)⁻¹) by
        rw [← Nat.cast_commute (i.choose j), ← this, ← mul_smul_comm, ← nsmul_eq_mul,
          mul_smul, ← smul_assoc, smul_comm, smul_assoc]
        norm_cast
      rw [Nat.choose_eq_factorial_div_factorial hj,
        Nat.cast_div (Nat.factorial_mul_factorial_dvd_factorial hj) (by positivity)]
      simp [field]
    · rw [hR2N, sum_sigma']
      apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))
      · simp only [mem_sigma, mem_range, mem_filter, mem_product, and_imp]
        lia
      · simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]
        rintro ⟨x₁, y₁⟩ - h₁ ⟨x₂, y₂⟩ - h₂ h₃ h₄
        simp_all
        lia
      · simp only [mem_filter, mem_product, mem_range, mem_sigma, exists_prop, Sigma.exists,
          and_imp, Prod.forall, Prod.mk.injEq]
        exact fun x y _ _ _ ↦ ⟨x + y, x, by lia⟩
      · simp only [mem_sigma, mem_range, implies_true]

Goal state after:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: case refine_1
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
hss : (aeval ⟨s, mem⟩) P = 0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ f - s ∈ K[f]

pp: case refine_2
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
hss : (aeval ⟨s, mem⟩) P = 0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ (f - s) ^ k = 0

pp: case refine_3
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
hss : (aeval ⟨s, mem⟩) P = 0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ s.IsSemisimple

Tactic:
· exact sub_mem (self_mem_adjoin_singleton K f) mem

Goal state after:
case refine_2
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
hss : (aeval ⟨s, mem⟩) P = 0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ (f - s) ^ k = 0

case refine_3
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
P : K[X]
k✝ : ℕ
sep : P.Separable
nil : minpoly K f ∣ P ^ k✝
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
nil' : IsNilpotent ((aeval ff) P)
sep' : IsUnit ((aeval ff) P')
s : End K V
mem : s ∈ K[f]
hss : (aeval ⟨s, mem⟩) P = 0
k : ℕ
hk : (ff - ⟨s, mem⟩) ^ k = 0
⊢ s.IsSemisimple