mathlib-initiative/mathlib-tactics huggingface dataset:
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₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
h'' : i₂ + i₃ + i₄ = i₂₃₄
⊢ X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g

Tactic:
have hj : i₁ + i₂ + i₃ + i₄ = j := by simp only [← h', ← h'', add_assoc]

Goal state after:
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₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
i₁ i₂₃₄ : I
h' : i₁ + i₂₃₄ = j
i₂ i₃ i₄ : I
h'' : i₂ + i₃ + i₄ = i₂₃₄
hj : i₁ + i₂ + i₃ + i₄ = j
⊢ X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ f =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ h'' ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j h' ≫ g
Module: Mathlib.Algebra.Homology.SpectralObject.Cycles

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, 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'
i'' j'' k'' : ι
f'' : i'' ⟶ j''
g'' : j'' ⟶ k''
α : mk₂ f g ⟶ mk₂ f' g'
n : ℤ
⊢ (mk₁ f).obj' 1 homMk₁._proof_5 ⟶ (mk₁ f').obj' 1 homMk₁._proof_5

Tactic:
exact α.app 1

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{?u.4, u_1} C
inst✝ : Abelian C
κ : Type u_2
c : ℤ → ComplexShape κ
r₀ : ℤ
E : SpectralSequence C c r₀
pq : κ
r r' : ℤ
h : r = r'
hr : r₀ ≤ r
⊢ (E.page r ⋯).X pq = (E.page r' ⋯).X pq

Tactic:
by subst h; rfl

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 : ℤ
hr : r₀ ≤ r
pq pq' : κ
hpq : (c r).Rel pq pq'
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
h₀ : i₀ = data.i₀ r pq' ⋯
h₁ : i₁ = data.i₁ pq'
h₂ : i₂ = data.i₀ r pq ⋯
h₃ : i₃ = data.i₁ pq
h₄ : i₄ = data.i₂ pq
h₅ : i₅ = data.i₃ r pq ⋯
n₀ n₁ n₂ n₃ : ℤ
hn₁' : n₁ = data.deg pq
hn₁ : autoParam (n₀ + 1 = n₁) pageD_eq._auto_1
hn₂ : autoParam (n₁ + 1 = n₂) pageD_eq._auto_3
hn₃ : autoParam (n₂ + 1 = n₃) pageD_eq._auto_5
⊢ i₂ = data.i₂ pq'

Tactic:
rw [h₂, data.hc₀₂ r pq pq' hpq]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
α : mk₁ f ⟶ mk₁ f'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
hβ : β = homMk₃ (α.app 0) (α.app 0) (α.app 1) (α.app 1) ⋯ ⋯ ⋯
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.map (𝟙 i) f (𝟙 j) (𝟙 i') f' (𝟙 j') β n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.H n₁).map α

Tactic:
obtain rfl : α = homMk₁ (β.app 1) (β.app 2) (naturality' β 1 2) := by
    subst hβ
    exact hom_ext₁ rfl rfl

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j : ι
f : i ⟶ j
i' j' : ι
f' : i' ⟶ j'
β : mk₃ (𝟙 i) f (𝟙 j) ⟶ mk₃ (𝟙 i') f' (𝟙 j')
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hβ :
  β =
    homMk₃ ((homMk₁ (β.app 1) (β.app 2) ⋯).app 0) ((homMk₁ (β.app 1) (β.app 2) ⋯).app 0)
      ((homMk₁ (β.app 1) (β.app 2) ⋯).app 1) ((homMk₁ (β.app 1) (β.app 2) ⋯).app 1) ⋯ ⋯ ⋯
⊢ X.map (𝟙 i) f (𝟙 j) (𝟙 i') f' (𝟙 j') β n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f' n₀ n₁ n₂ hn₁ hn₂).hom =
    (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom ≫ (X.H n₁).map (homMk₁ (β.app 1) (β.app 2) ⋯)
Module: Mathlib.Algebra.Homology.SpectralObject.Page

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ (X.opcyclesIsoH f n₀ n₁ hn₁).hom = X.fromOpcycles f (𝟙 i₁) f ⋯ n₁

Tactic:
rw [← cancel_epi (X.pOpcycles f (𝟙 _) n₁), p_fromOpcycles]

Goal state after:
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i₀ i₁ : ι
f : i₀ ⟶ i₁
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
⊢ X.pOpcycles f (𝟙 i₁) n₁ ≫ (X.opcyclesIsoH f n₀ n₁ hn₁).hom = (X.H n₁).map (twoδ₂Toδ₁ f (𝟙 i₁) f ⋯)
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).next pq' = pq''
i₀' i₀ i₁ i₂ i₃ : ι
hi₀' : i₀' = data.i₀ r' pq' ⋯
hi₀ : i₀ = data.i₀ r pq' ⋯
hi₁ : i₁ = data.i₁ pq'
hi₂ : i₂ = data.i₂ 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₂ pq''

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

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

Goal state before:
pp: L : Type v
inst✝ : LieRing L
x y : L
⊢ ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0

Tactic:
← lie_add

Goal state after:
L : Type v
inst✝ : LieRing L
x y : L
⊢ ⁅x + y, x + y⁆ = 0
Module: Mathlib.Algebra.Lie.Basic

Goal state before:
pp: L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m⁆ + ⁅x, m⁆ = 0

Tactic:
← lie_add

Goal state after:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m : M
⊢ ⁅x, -m + m⁆ = 0
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
f : Module.End R M
⊢ ∀ᶠ (n : ℕ) in atTop, ⨅ m, (f ^ m).range = (f ^ n).range

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.range (f ^ n) = LinearMap.range (f ^ m)⟩ :=
    IsArtinian.monotone_stabilizes f.iterateRange
  refine eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
  rcases le_or_gt l m with h | h
  · rw [← hn _ (hl.trans h), hn _ hl]
  · exact f.iterateRange.monotone h.le

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
⊢ ∀ {x : L} {m : N}, ((↑f).inverse g h₁ h₂).toFun ⁅x, m⁆ = ⁅x, ((↑f).inverse g h₁ h₂).toFun m⁆

Tactic:
intro x n

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : LieRingModule L M
inst✝¹ : LieRingModule L N
inst✝ : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x : L
n : N
⊢ ((↑f).inverse g h₁ h₂).toFun ⁅x, n⁆ = ⁅x, ((↑f).inverse g h₁ h₂).toFun n⁆
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsArtinianRing R
Jac : Ideal R := Ring.jacobson R
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } n = { toFun := fun x ↦ Jac ^ x, monotone' := ⋯ } m
⊢ Jac ^ (n + 1) = Jac ^ n

Tactic:
exact (hn _ n.le_succ).symm

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : ↑J₁ ⊆ ↑J₂
⊢ ↑(comap f J₁) ⊆ ↑(comap f J₂)

Tactic:
dsimp only [SetLike.coe]

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : ↑J₁ ⊆ ↑J₂
⊢ (↑(comap f J₁)).carrier ⊆ (↑(comap f J₂)).carrier
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2.add
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y : L
hy : y ∈ lieSpan R L s
u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⁅⟨u, hx✝⟩, ⟨y, hy⟩⁆ = 0
hv : ⁅⟨v, hy✝⟩, ⟨y, hy⟩⁆ = 0
⊢ ⁅⟨u + v, ⋯⟩, ⟨y, hy⟩⁆ = 0

Tactic:
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] at hu hv ⊢

Goal state after:
case refine_2.add
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
h : ∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0
x✝¹ x✝ : ↥(lieSpan R L s)
x y : L
hy : y ∈ lieSpan R L s
u v : L
hx✝ : u ∈ lieSpan R L s
hy✝ : v ∈ lieSpan R L s
hu : ⁅u, y⁆ = 0
hv : ⁅v, y⁆ = 0
⊢ ⁅u, y⁆ + ⁅v, y⁆ = 0
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
s : Set M
⊢ lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = 0

Tactic:
by
  rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]

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

Goal state before:
pp: R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst✝⁹ : CommRing R
inst✝⁸ : LieRing L
inst✝⁷ : LieRing L'
inst✝⁶ : LieAlgebra R L'
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N✝ N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
e : M ≃ₗ⁅R,L⁆ M'
N : LieSubmodule R L M'
m✝ : M'
⊢ m✝ ∈ map e.toLieModuleHom (comap e.toLieModuleHom N) ↔ m✝ ∈ N

Tactic:
simp [← e.eq_symm_apply]

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
hx : (minpoly A x).degree = 1
h : ¬IsIntegral A x
⊢ False

Tactic:
rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : ⊥ = ↑1
h : ¬IsIntegral A x
⊢ False
Module: Mathlib.FieldTheory.Minpoly.Basic

Goal state before:
pp: case inr
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Algebra A B
x : B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : (Polynomial.aeval x) g = 0
⊢ minpoly A x = g * f

Tactic:
rw [mul_comm, he]

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

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ ↑f = ↑g

Tactic:
funext_iff

Goal state after:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : ∀ (x : ↑(range ⇑(Module.finBasis F E))), rootsOfMinPolyPiType F E K f x = rootsOfMinPolyPiType F E K g x
⊢ ↑f = ↑g
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (a * c)⁆ + ⁅L c, L (c * a)⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (c * b)⁆)) =
    0
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (c * b)⁆)) =
    0
Module: Mathlib.Algebra.Jordan.Basic

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

Tactic:
rw [two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add]

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + (⁅L (a * a), L b⁆ + ⁅L (b * b), L a⁆) +
        (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + (⁅L (a * a), L c⁆ + ⁅L (c * c), L a⁆)) +
      (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + (⁅L (b * b), L c⁆ + ⁅L (c * c), L b⁆)) =
    0
Module: Mathlib.RingTheory.Norm.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
h : ¬∃ s, Nonempty (Basis (↥s) R S)
x : S
⊢ (if H : ∃ s, Nonempty (Basis (↥s) R S) then detAux (Trunc.mk ⋯.some) else 1) ((lmul R S) x) = 1

Tactic:
split_ifs <;> trivial

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
⊢ root (X ^ n - C a) = 0 ↔ a = 0

Tactic:
have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩
  rintro rfl
  have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl
  rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]

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

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
f : ι → R
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (IsRelPrime on f) → (∀ i ∈ s, Squarefree (f i)) → Squarefree (∏ i ∈ s, f i)
hs : (↑s).Pairwise (IsRelPrime on f) ∧ ∀ b ∈ ↑s, a ≠ b → (IsRelPrime on f) a b ∧ (IsRelPrime on f) b a
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree (∏ x ∈ s, f x)

Tactic:
· exact ih hs.left fun i hi ↦ hs' i <| Finset.mem_cons_of_mem hi

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : IsCancelMulZero R
inst✝ : DecompositionMonoid R
ι : Type u_2
s : Finset ι
f : ι → R
hs : (↑s).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ s, Squarefree (f i)
⊢ Squarefree (∏ i ∈ s, f i)

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    rw [Finset.prod_cons, squarefree_mul_iff]
    rw [Finset.coe_cons, Set.pairwise_insert] at hs
    refine ⟨.prod_right fun i hi ↦ ?_, hs' a (by simp), ?_⟩
    · exact (hs.right i (by simp [hi]) fun h ↦ ha (h ▸ hi)).left
    · exact ih hs.left fun i hi ↦ hs' i <| Finset.mem_cons_of_mem hi

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ x ∈ s, x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ (∏ x ∈ insert a s, f x).Separable

Tactic:
rw [prod_insert has]

Goal state after:
R : Type u
inst✝ : CommRing R
ι : Type u_1
f : ι → R[X]
s✝ : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ x ∈ s, x ≠ a → IsCoprime (f x) (f a)) ∧ ∀ x ∈ s, ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ (f a * ∏ x ∈ s, f x).Separable
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 * b) = 1

Tactic:
hb,

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 1 = 1
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ Multiset.count x p.roots ≤ 1

Tactic:
rw [count_roots p]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: 𝕜 : Type u_7
inst✝² : Field 𝕜
M : Type u_8
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
⊢ LinearMap.det f = 1

Tactic:
by
  classical
    refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl
    intro s b
    have : IsEmpty s := by
      rw [← Fintype.card_eq_zero_iff]
      exact (Module.finrank_eq_card_basis b).symm.trans h
    exact Matrix.det_isEmpty

Goal state after:
Module: Mathlib.FieldTheory.Perfect

Goal state before:
pp: M : Type u_1
p q : ℕ
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : PerfectRing M q
⊢ Bijective fun x ↦ x ^ (p * q)

Tactic:
simp_rw [pow_mul]

Goal state after:
M : Type u_1
p q : ℕ
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
inst✝ : PerfectRing M q
⊢ Bijective fun x ↦ (x ^ p) ^ q
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✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ ((Pi.basis fun x ↦ b).repr
        ((pi fun i ↦ f i ∘ₗ proj i)
          ((Pi.basis fun x ↦ b)
            ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).symm
              ((Equiv.prodComm (Free.ChooseBasisIndex R M) ι) (j₁, j₂))))))
      ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).symm
        ((Equiv.prodComm (Free.ChooseBasisIndex R M) ι) (i₁, i₂))) =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0

Tactic:
Equiv.prodComm_apply,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : Fintype ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Free.ChooseBasisIndex R M × ι) R (ι → M) :=
  (Pi.basis fun x ↦ b).reindex
    ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).trans (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
i₁ : Free.ChooseBasisIndex R M
i₂ : ι
j₁ : Free.ChooseBasisIndex R M
j₂ : ι
⊢ ((Pi.basis fun x ↦ b).repr
        ((pi fun i ↦ f i ∘ₗ proj i)
          ((Pi.basis fun x ↦ b) ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).symm (j₁, j₂).swap))))
      ((Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)).symm (i₁, i₂).swap) =
    if i₂ = j₂ then (toMatrix b b) (f i₂) i₁ j₁ else 0
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
x : R
⊢ (lift i a h) ((of f) x) = i x

Tactic:
rw [← mk_C x, lift_mk, eval₂_C]

Goal state after:
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
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ p ∣ Polynomial.map (↑↑f.symm) q

Tactic:
have : (RingHomClass.toRingHom f.toRingEquiv.symm).comp (RingHomClass.toRingHom f) =
        .id S := by ext; exact f.symm_apply_apply _

Goal state after:
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
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
this : (↑f.toRingEquiv.symm).comp ↑f = RingHom.id S
⊢ p ∣ Polynomial.map (↑↑f.symm) q
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
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
⊢ Associated (Polynomial.map (↑f.symm) q) p

Tactic:
have : (RingHomClass.toRingHom f.toRingEquiv.symm).comp (RingHomClass.toRingHom f) =
        .id S := by ext; exact f.symm_apply_apply _

Goal state after:
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
a : S
h✝ : eval₂ i a f✝ = 0
inst✝⁴ : CommRing T
inst✝³ : CommRing U
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R U
f : S ≃ₐ[R] T
p : S[X]
q : T[X]
h : Associated (Polynomial.map (↑f) p) q
this : (↑f.toRingEquiv.symm).comp ↑f = RingHom.id S
⊢ Associated (Polynomial.map (↑f.symm) q) p