mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_2
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) ≤ CochainComplex.Plus.quasiIso C

Tactic:
intro K

Goal state after:
case refine_2
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
K : CochainComplex.Plus C
⊢ ∀ ⦃Y : CochainComplex.Plus C⦄ (f : K ⟶ Y),
    (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) f →
      CochainComplex.Plus.quasiIso C f
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : ¬n + 1 = m
⊢ h.d n m ≫ h.d m p = 0

Tactic:
rw [h.shape n m hnm, zero_comp]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

Tactic:
obtain _ | _ := c.exists_distinct_prev_or j

Goal state after:
case neg.inl
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
h✝ : ∃ k, c.Rel j k ∧ j ≠ k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1

case neg.inr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_2
c : ComplexShape ι
inst✝ : c.HasNoLoop
X : C
j : ι
h : ¬∃ k, c.Rel j k
h✝ : ∀ (k : ι), ¬c.Rel j k
⊢ ∀ (j_1 : ι), ¬c.Rel j j_1
Module: Mathlib.CategoryTheory.Generator.HomologicalComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : (ObjectProperty.ofObj X).IsSeparating
⊢ (ObjectProperty.ofObj (separatingFamily c X)).IsSeparating

Tactic:
intro K

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst✝² : c.HasNoLoop
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
α : Type t
X : α → C
hX : (ObjectProperty.ofObj X).IsSeparating
K : HomologicalComplex C c
⊢ ∀ ⦃Y : HomologicalComplex C c⦄ (f g : K ⟶ Y),
    (∀ (G : HomologicalComplex C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g) →
      f = g
Module: Mathlib.Algebra.Homology.ExactSequenceFour

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)

Tactic:
have : Mono (hS.cokerToKer' k hk cc kf hcc hkf) :=
      hS.toIsComplex.mono_cokerToKer' k hk cc kf hcc hkf
    (hS.exact k)

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : Balanced C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.Exact
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
this : Mono (hS.cokerToKer' k hk cc kf hcc hkf)
⊢ IsIso (hS.cokerToKer' k hk cc kf hcc hkf)
Module: Mathlib.CategoryTheory.GradedObject.Single

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : HasInitial C
inst✝ : DecidableEq J
j : J
X : C
i : J
h : i ≠ j
⊢ IsInitial (⊥_ C)

Tactic:
exact initialIsInitial

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

Goal state before:
pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i₁ i₂ j : I
h₁ : ¬c.Rel i₂ (c.next i₂)
⊢ mapBifunctor.d₂ K (tensorUnit C c) (curriedTensor C) c i₁ i₂ j = 0

Tactic:
· rw [mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₁]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteColimits F
X : C
⊢ IsIso (F.fromLeftDerivedZero.app X)

Tactic:
dsimp [Functor.fromLeftDerivedZero]
  infer_instance

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

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₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₁₂ : i₀ ⟶ i₂
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
f₄₅ : i₃ ⟶ i₅
h₄₅ : f₄ ≫ f₅ = f₄₅
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ (X.H n₁).map (twoδ₂Toδ₁ f₃ f₄ (f₃ ≫ f₄) ⋯) ≫
      X.δ (f₁ ≫ f₂) (f₃ ≫ f₄) n₁ n₂ hn₂ ≫ X.toCycles f₁ f₂ (f₁ ≫ f₂) ⋯ n₂ ≫ X.πE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃ =
    0

Tactic:
rw [X.δ_naturality_assoc (f₁ ≫ f₂) f₃ (f₁ ≫ f₂) (f₃ ≫ f₄)
        (𝟙 _) (twoδ₂Toδ₁ f₃ f₄ _ rfl) n₁ n₂ rfl hn₂, Functor.map_id, id_comp,
        δ_toCycles_assoc .., δToCycles_πE ..]

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₀ : ℤ
X✝ Y✝ Z✝ : SpectralSequence C c r₀
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
r r' : ℤ
hrr' : κ
pq : r + 1 = r'
hr : r₀ ≤ r
⊢ HomologicalComplex.homologyMap (f.hom r ⋯ ≫ g.hom r ⋯) hrr' ≫ (Z✝.iso r r' hrr' ⋯ ⋯).hom =
    (X✝.iso r r' hrr' ⋯ ⋯).hom ≫ (f.hom r' ⋯ ≫ g.hom r' ⋯).f hrr'

Tactic:
simp [HomologicalComplex.homologyMap_comp, assoc, g.comm r r', f.comm_assoc r r']

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✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
⊢ Injective DFunLike.coe

Tactic:
rintro ⟨⟨⟨f, _⟩⟩⟩ ⟨⟨⟨g, _⟩⟩⟩ h

Goal state after:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
f : M → N
map_add'✝¹ : ∀ (x y : M), f (x + y) = f x + f y
map_smul'✝¹ :
  ∀ (m : R) (x : M),
    { toFun := f, map_add' := map_add'✝¹ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := f, map_add' := map_add'✝¹ }.toFun x
map_lie'✝¹ :
  ∀ {x : L} {m : M},
    { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹ }.toFun m⁆
g : M → N
map_add'✝ : ∀ (x y : M), g (x + y) = g x + g y
map_smul'✝ :
  ∀ (m : R) (x : M),
    { toFun := g, map_add' := map_add'✝ }.toFun (m • x) =
      (RingHom.id R) m • { toFun := g, map_add' := map_add'✝ }.toFun x
map_lie'✝ :
  ∀ {x : L} {m : M},
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝ }.toFun m⁆
h :
  ⇑{ toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    ⇑{ toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }
⊢ { toFun := f, map_add' := map_add'✝¹, map_smul' := map_smul'✝¹, map_lie' := map_lie'✝¹ } =
    { toFun := g, map_add' := map_add'✝, map_smul' := map_smul'✝, map_lie' := map_lie'✝ }
Module: Mathlib.Algebra.Lie.OfAssociative

Goal state before:
pp: R : Type u
L : Type v
M : 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
t : R
x : L
⊢ { toFun := fun m ↦ ⁅t • x, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) t • { toFun := fun m ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext m; apply smul_lie

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
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x y : L
hx : ∀ a ∈ S, x ∈ ↑a.toSubmodule
hy : ∀ a ∈ S, y ∈ ↑a.toSubmodule
⊢ ∀ a ∈ S, ⁅x, y⁆ ∈ ↑a.toSubmodule

Tactic:
intro K

Goal state after:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K✝ K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x y : L
hx : ∀ a ∈ S, x ∈ ↑a.toSubmodule
hy : ∀ a ∈ S, y ∈ ↑a.toSubmodule
K : LieSubalgebra R L
⊢ K ∈ S → ⁅x, y⁆ ∈ ↑K.toSubmodule
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
x : L
⊢ x ∈ lieSpan R L s ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K

Tactic:
rw [← SetLike.mem_coe, lieSpan, coe_sInf]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
x : L
⊢ x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
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
m : L
hm : m ∈ s
⊢ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K

Tactic:
intro K

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
m : L
hm : m ∈ s
K : LieSubalgebra R L
⊢ s ⊆ ↑K → m ∈ K
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
⊢ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s) = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ ⊤ ≤ lieSpan R (↥(lieSpan R L s)) (Subtype.val ⁻¹' s)
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
p : Submodule R M
h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier
⊢ ↑{ toSubmodule := p, lie_mem := h } = p

Tactic:
cases p; rfl

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'
I : LieIdeal R L
J : LieIdeal R L'
h : ⇑f '' ↑I = ↑J
⊢ map f I = J

Tactic:
apply le_antisymm
  · rw [map, LieSubmodule.lieSpan_le, Submodule.map_coe]
    /- I'm uncertain how to best resolve this `erw`.
    ```
    have : (↑(toLieSubalgebra R L I).toSubmodule : Set L) = I := rfl
    rw [this]
    simp [h]
    ```
    works, but still feels awkward. There are missing `simp` lemmas here.`
    -/
    erw [h]
  · rw [← SetLike.coe_subset_coe, ← h]; exact LieSubmodule.subset_lieSpan

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

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₂
h : Function.Injective ⇑f
⊢ Function.Injective ⇑↑f

Tactic:
LieHom.coe_toLinearMap

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₂
h : Function.Injective ⇑f
⊢ Function.Injective ⇑f
Module: Mathlib.Algebra.Lie.Subalgebra

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₂
L₁' L₁'' : LieSubalgebra R L₁
L₂' : LieSubalgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
h : LieSubalgebra.map e.toLieHom L₁' = L₂'
⊢ Submodule.map (↑e.toLinearEquiv) L₁'.toSubmodule = L₂'.toSubmodule

Tactic:
by
      rw [← h]
      rfl

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

Goal state before:
pp: case h
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'
I : LieIdeal R L
h₁ : Function.Surjective ⇑f
x : L
hx : x ∈ ↑I
⊢ f ↑⟨x, hx⟩ = ↑f x

Tactic:
LieHom.coe_toLinearMap

Goal state after:
case h
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'
I : LieIdeal R L
h₁ : Function.Surjective ⇑f
x : L
hx : x ∈ ↑I
⊢ f ↑⟨x, hx⟩ = f x
Module: Mathlib.Algebra.Lie.IdealOperations

Goal state before:
pp: case refine_4
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
⊢ ∀ (a : R), ∀ x ∈ Submodule.span R s, ⁅y, x⁆ ∈ Submodule.span R s → ⁅y, a • x⁆ ∈ Submodule.span R s

Tactic:
intro t m'' _ hm''

Goal state after:
case refine_4
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
inst✝¹ : LieAlgebra R L
I : LieIdeal R L
inst✝ : LieModule R L M
s : Set M := {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x}
y : L
m' : M
hm' : m' ∈ Submodule.span R s
t : R
m'' : M
hx✝ : m'' ∈ Submodule.span R s
hm'' : ⁅y, m''⁆ ∈ Submodule.span R s
⊢ ⁅y, t • m''⁆ ∈ Submodule.span R s
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case mp
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
⊢ Nontrivial ↥N → N ≠ ⊥

pp: case mpr
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
⊢ N ≠ ⊥ → Nontrivial ↥N

Tactic:
· rintro ⟨⟨m₁, h₁⟩, ⟨m₂, h₂⟩, h₁₂⟩ rfl
    simp [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂] at h₁₂

Goal state after:
case mpr
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
⊢ N ≠ ⊥ → Nontrivial ↥N
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
x : M
⊢ x ∈ lieSpan R L s ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

Tactic:
rw [← SetLike.mem_coe, lieSpan, coe_sInf]

Goal state after:
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
x : M
⊢ x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: case refine_2.mem
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
w : L
hw : w ∈ s
⊢ ⁅⟨w, ⋯⟩, ⟨y, hy⟩⁆ = 0

Tactic:
induction hy using lieSpan_induction with
      | mem u hu => simpa [Subtype.ext_iff] using h w hw u hu
      | zero => simp [Subtype.ext_iff]
      | add u v _ _ hu hv =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, lie_add] at hu hv ⊢
        simp [hu, hv]
      | smul t u _ hu =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
        simp [Subtype.ext_iff, hu]
      | lie u v _ _ hu hv =>
        simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
        rw [leibniz_lie]
        simp [hu, hv]

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

Goal state before:
pp: R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ ↑(map f ⁅I, N⁆) = ↑⁅I, map f N⁆

Tactic:
toSubmodule_map,

Goal state after:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N : LieSubmodule R L M
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
⊢ Submodule.map ↑f ↑⁅I, N⁆ = ↑⁅I, map f N⁆
Module: Mathlib.FieldTheory.Minpoly.Field

Goal state before:
pp: case pos
A : Type u_1
inst✝² : Field A
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
a : A
hx : IsIntegral A x
⊢ minpoly A (x + (algebraMap A B) a) = (minpoly A x).comp (X - C a)

Tactic:
refine (minpoly.unique _ _ ((minpoly.monic hx).comp_X_sub_C _) ?_ fun q qmo hq => ?_).symm
    · simp [aeval_comp]
    · have : (Polynomial.aeval x) (q.comp (X + C a)) = 0 := by simpa [aeval_comp] using hq
      have H := minpoly.min A x (qmo.comp_X_add_C _) this
      rw [degree_eq_natDegree qmo.ne_zero,
        degree_eq_natDegree ((minpoly.monic hx).comp_X_sub_C _).ne_zero, natDegree_comp,
        natDegree_X_sub_C, mul_one]
      rwa [degree_eq_natDegree (minpoly.ne_zero hx),
        degree_eq_natDegree (qmo.comp_X_add_C _).ne_zero, natDegree_comp,
        natDegree_X_add_C, mul_one] at H

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C (X - C a) * C p + (X - C b) * q = P

Tactic:
eq_add_of_sub_eq' hq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C (X - C a) * C p + (X - C b) * q = C (eval b P) + (X - C b) * q
Module: Mathlib.RingTheory.PowerBasis

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : Ring S
inst✝⁷ : Algebra R S
A : Type u_4
B : Type u_5
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
K : Type u_6
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
f : S →ₐ[A] S'
⊢ (aeval (f pb.gen)) (minpoly A pb.gen) = 0

Tactic:
by rw [aeval_algHom_apply, minpoly.aeval, map_zero]

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

Goal state before:
pp: case cons
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 : (↑(cons a s ha)).Pairwise (IsRelPrime on f)
hs' : ∀ i ∈ cons a s ha, Squarefree (f i)
⊢ Squarefree (∏ i ∈ cons a s ha, f i)

Tactic:
| cons a s ha ih =>

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
⊢ Squarefree x ↔ (normalizedFactors x).Nodup

Tactic:
classical
  rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
  have := nontrivial_of_ne x 0 x0
  constructor <;> intro h a
  · by_cases hmem : a ∈ normalizedFactors x
    · have ha := irreducible_of_normalized_factor _ hmem
      rcases h a with (h | h)
      · rw [← normalize_normalized_factor _ hmem]
        rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
        assumption_mod_cast
      · have := ha.1
        contradiction
    · simp [Multiset.count_eq_zero_of_notMem hmem]
  · rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
⊢ (map f p).Separable ↔ p.Separable

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩

Goal state after:
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
⊢ p.Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable

Tactic:
have := Separable.map H (f := Ideal.Quotient.mk m)

Goal state after:
F : Type u
inst✝² : Field F
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case inl
F✝ : Type u
inst✝¹ : Field F✝
p✝ : ℕ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ k : ℕ
r : F
hr : IsUnit r
hg₂ : (C r).Separable
hg₁ : ((expand F (p ^ k)) (C r)).Separable
hf : Irreducible (C r)
⊢ n₁ = n₁ + k ∧ (expand F (p ^ k)) (C r) = C r

Tactic:
exact absurd (isUnit_C.2 hr) hf.1

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬derivative f = 0

Tactic:
← degree_eq_bot,

Goal state after:
F : Type u
inst✝¹ : Field F
inst✝ : CharZero F
f : F[X]
hf : Irreducible f
⊢ ¬(derivative f).degree = ⊥
Module: Mathlib.RingTheory.AdjoinRoot

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : f = 0
⊢ 0 ∣ C p

Tactic:
rwa [h] at hp

Goal state after:
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
v : ι → M
hli : LinearIndependent R v
hspan : span R (Set.range v) = ⊤
v' : Basis ι R M := Basis.mk hli ⋯
i j : ι
⊢ e.toMatrix v i j = (LinearMap.toMatrix v' e) (↑(LinearEquiv.refl R M)) i j

Tactic:
simp [v']

Goal state after: