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

Goal state before:
pp: case e_a
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).flip.obj X₂)
i : I
⊢ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 = (singleObjXSelf c 0 (𝟙_ C)).inv

Tactic:
← cancel_epi (GradedObject.Monoidal.tensorUnit₀ (I := I)).hom,

Goal state after:
case e_a
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).flip.obj X₂)
i : I
⊢ GradedObject.Monoidal.tensorUnit₀.hom ≫ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 =
    GradedObject.Monoidal.tensorUnit₀.hom ≫ (singleObjXSelf c 0 (𝟙_ C)).inv
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case e_a
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
⊢ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 = (singleObjXSelf c 0 (𝟙_ C)).inv

Tactic:
← cancel_epi (GradedObject.Monoidal.tensorUnit₀ (I := I)).hom,

Goal state after:
case e_a
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
⊢ GradedObject.Monoidal.tensorUnit₀.hom ≫ GradedObject.Monoidal.tensorUnit₀.inv ≫ (tensorUnitIso C c).hom 0 =
    GradedObject.Monoidal.tensorUnit₀.hom ≫ (singleObjXSelf c 0 (𝟙_ C)).inv
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₂ Y₁ Y₂ : GradedObject I C
f : X₁ ⟶ X₂
g : Y₁ ⟶ Y₂
inst✝¹ : X₁.HasTensor Y₁
inst✝ : X₂.HasTensor Y₂
i₁ i₂ i₁₂ : I
h : i₁ + i₂ = i₁₂
⊢ ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = f i₁ ▷ Y₁ i₂ ≫ X₂ i₁ ◁ g i₂ ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h

Tactic:
apply ι_mapBifunctorMapMap

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 k l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X.map f₁ f₂ f₃ f₁ f₂ f₃ (𝟙 (mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁ hn₂ = 𝟙 (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)

Tactic:
dsimp only [map]
  simp [shortComplexMap_id, ShortComplex.homologyMap_id]
  rfl

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

Goal state before:
pp: case refine_2
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 l : ι
f₁ : i ⟶ j
f₂ : j ⟶ k
f₃ : k ⟶ l
f₁₂ : i ⟶ k
h₁₂ : f₁ ≫ f₂ = f₁₂
f₂₃ : j ⟶ l
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hp : IsColimit (CokernelCofork.ofπ (X.cokernelSequenceOpcycles f₂ f₃ n₀ n₁ hn₁).g ⋯) := ⋯.gIsCokernel
this : hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯) = X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ hn₂
⊢ (Cone.postcompose
          (parallelPair.ext
              (Iso.refl
                ((parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).obj
                  WalkingParallelPair.zero))
              (Iso.refl
                ((parallelPair (hp.desc (CokernelCofork.ofπ (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).g ⋯)) 0).obj
                  WalkingParallelPair.one))
              ⋯ ⋯).hom).obj
      (KernelFork.ofι (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)) ⋯) ≅
    Fork.ofι (kernel.ι (X.δFromOpcycles f₁ f₂ f₃ n₁ n₂ ⋯)) ⋯

Tactic:
exact Fork.ext (Iso.refl _)

Goal state after:
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ Y✝ : Square C
φ : X✝ ⟶ Y✝
⊢ (X✝.map F).f₁₂ ≫ F.map φ.τ₂ = F.map φ.τ₁ ≫ (Y✝.map F).f₁₂

Tactic:
simpa only [Functor.map_comp] using! F.congr_map φ.comm₁₂

Goal state after:
Module: Mathlib.Order.Filter.Subsingleton

Goal state before:
pp: α : Type u_1
l : Filter α
hl : l.Subsingleton
⊢ l.IsCountablyGenerated

Tactic:
by
  rcases subsingleton_iff_bot_or_pure.1 hl with rfl | ⟨x, rfl⟩
  · exact isCountablyGenerated_bot
  · exact isCountablyGenerated_pure x

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

Goal state before:
pp: R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L₁
inst✝⁴ : LieRing L₂
inst✝³ : LieRing L₃
inst✝² : LieAlgebra R L₁
inst✝¹ : LieAlgebra R L₂
inst✝ : LieAlgebra R L₃
x✝² : L₁ ≃ₗ⁅R⁆ L₂
x✝¹ x✝ : L₁
⊢ x✝² (x✝¹ + x✝) = x✝² x✝¹ + x✝² x✝

Tactic:
by
    rw [← coe_toLinearEquiv, map_add]

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
x✝² : M ≃ₗ⁅R,L⁆ N
x✝¹ x✝ : M
⊢ x✝² (x✝¹ + x✝) = x✝² x✝¹ + x✝² x✝

Tactic:
by
    rw [← coe_toLinearEquiv, map_add]

Goal state after:
Module: Mathlib.RingTheory.Artinian.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsArtinian R M
inst✝ : IsNoetherian R M
f : Module.End R M
⊢ ∀ᶠ (n : ℕ) in atTop, IsCompl (f ^ n).ker (f ^ n).range

Tactic:
by
  filter_upwards [f.eventually_disjoint_ker_pow_range_pow.and
    f.eventually_codisjoint_ker_pow_range_pow] with n hn
  simpa only [isCompl_iff]

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 (LieSubalgebra R L)
⊢ IsGLB S (sInf S)

Tactic:
by
  have h : ∀ K K' : LieSubalgebra R L, (K : Set L) ≤ K' ↔ K ≤ K' := by
    intros
    exact Iff.rfl
  apply IsGLB.of_image @h
  simp only [coe_sInf]
  exact isGLB_biInf

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
S : Set (LieSubmodule R L M)
m : M
⊢ m ∈ ⋂ p ∈ {x | ∃ s ∈ S, ↑s = x}, ↑p ↔ m ∈ ⋂ s ∈ S, ↑s

Tactic:
simp only [mem_iInter, mem_ofPred_eq, forall_apply_eq_imp_iff₂, exists_imp,
    and_imp, SetLike.mem_coe, mem_toSubmodule]

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
ι : Sort u_1
N : ι → LieSubmodule R L M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, N i
mem : ∀ (i : ι), ∀ y ∈ N i, motive y
zero : motive 0
add : ∀ (y z : M), motive y → motive z → motive (y + z)
⊢ motive x

Tactic:
by
  rw [← LieSubmodule.mem_toSubmodule, LieSubmodule.iSup_toSubmodule] at hx
  exact Submodule.iSup_induction (motive := motive) (fun i ↦ (N i : Submodule R M)) hx mem zero add

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
⊢ N = ⊥ ↔ ∀ m ∈ N, m = 0

Tactic:
rw [eq_bot_iff]; exact Iff.rfl

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

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₁ : Surjective ⇑f
h₂ : IsLieAbelian L₁
u v : L₁
⊢ ⁅f u, f v⁆ = 0

Tactic:
rw [← LieHom.map_lie, trivial_lie_zero, map_zero]

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 N₂ : LieSubmodule R L M
⊢ ↑(comap N.incl N₂) = ↑⊤ ↔ N ≤ N₂

Tactic:
LieSubmodule.toSubmodule_comap,

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
N N₂ : LieSubmodule R L M
⊢ Submodule.comap ↑N.incl ↑N₂ = ↑⊤ ↔ N ≤ N₂
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: R : Type u
L : Type v
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
M' : Type u_2
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
inst✝ : LieRingModule L M'
e : M ≃ₗ⁅R,L⁆ M'
⊢ e.range = ⊤

Tactic:
rw [LieModuleHom.range_eq_top]
  exact e.surjective

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

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

Tactic:
zero_add,

Goal state after:
A : Type u_1
inst✝¹ : NonUnitalNonAssocCommRing A
inst✝ : IsCommJordan A
a b c : A
⊢ ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ +
        (⁅L b, L (a * a)⁆ + 0 + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ + ⁅L b, 2 • L (b * c)⁆) +
      (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + 0 + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ + ⁅L c, 2 • L (b * c)⁆) =
    ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) +
          (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) +
        (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) +
      (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆)
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 (b * c)⁆)) =
    0

Tactic:
mul_comm b c

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)⁆ + 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
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 + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆ =
    2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆)

Tactic:
aux1,

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p : (R ⧸ I)[X]
⊢ ∀ (q : (R ⧸ I)[X]),
    (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
          ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) p) =
        p →
      (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) q) =
          q →
        (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (p + q)) =
          p + q

Tactic:
q

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p q : (R ⧸ I)[X]
⊢ (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
        ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) p) =
      p →
    (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
          ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) q) =
        q →
      (Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
          ((eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X)) (p + q)) =
        p + q
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f p : R[X]
⊢ ∀ (q : R[X]),
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
          ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            (Quot.mk (⇑(Submodule.quotientRel (map C I))) p)) =
        Quot.mk (⇑(Submodule.quotientRel (map C I))) p →
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
            ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
              (Quot.mk (⇑(Submodule.quotientRel (map C I))) q)) =
          Quot.mk (⇑(Submodule.quotientRel (map C I))) q →
        (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
            ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
              (Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q))) =
          Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q)

Tactic:
q

Goal state after:
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f p q : R[X]
⊢ (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
        ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
          (Quot.mk (⇑(Submodule.quotientRel (map C I))) p)) =
      Quot.mk (⇑(Submodule.quotientRel (map C I))) p →
    (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
          ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            (Quot.mk (⇑(Submodule.quotientRel (map C I))) q)) =
        Quot.mk (⇑(Submodule.quotientRel (map C I))) q →
      (eval₂RingHom (Quotient.lift I ((Quotient.mk (map C I)).comp C) ⋯) ((Quotient.mk (map C I)) X))
          ((Quotient.lift (map C I) (eval₂RingHom (C.comp (Quotient.mk I)) X) ⋯)
            (Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q))) =
        Quot.mk (⇑(Submodule.quotientRel (map C I))) (p + q)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
⊢ ∀ (q : MvPolynomial σ (R ⧸ I)),
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (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)) p) =
        p →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            (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)) q) =
          q →
        (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
            (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)) (p + q)) =
          p + q

Tactic:
q

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ (R ⧸ I)
⊢ (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
        (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)) p) =
      p →
    (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (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)) q) =
        q →
      (Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) ⋯)
          (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)) (p + q)) =
        p + q
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    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) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
        (Ideal.Quotient.mk (Ideal.map C I)) p →
      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) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) q)) =
          (Ideal.Quotient.mk (Ideal.map C I)) q →
        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) ⋯)
              ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
          (Ideal.Quotient.mk (Ideal.map C I)) (p + q)

Tactic:
q

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ R
⊢ 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) ⋯)
          ((Ideal.Quotient.mk (Ideal.map C I)) p)) =
      (Ideal.Quotient.mk (Ideal.map C I)) p →
    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) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) q)) =
        (Ideal.Quotient.mk (Ideal.map C I)) q →
      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) ⋯)
            ((Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
        (Ideal.Quotient.mk (Ideal.map C I)) (p + q)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit y
⊢ IsUnit y

Tactic:
exact hu

Goal state after:
Module: Mathlib.FieldTheory.KummerPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this✝ : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
this : eval₂ (of g) (root g) X ^ p - (of g) a = 0
⊢ (Algebra.norm K) (root g) ^ p = a ^ g.natDegree

Tactic:
eval₂_X,

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this✝ : ¬IsUnit (X ^ p - C a)
g : K[X]
hg : Irreducible g
hg' : g ∣ X ^ p - C a
h : ¬g.natDegree = p
this : root g ^ p - (of g) a = 0
⊢ (Algebra.norm K) (root g) ^ p = a ^ g.natDegree
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: n : ℕ
⊢ Squarefree ↑n ↔ Squarefree n

Tactic:
by
  rw [← squarefree_natAbs, natAbs_natCast]

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
⊢ 0 + C e * C b = 1

Tactic:
zero_add,

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 * C b = 1
Module: Mathlib.LinearAlgebra.Determinant

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
this : ∃ s, Nonempty (Basis (↥s) A M)
⊢ LinearMap.det f = ((toMatrix b b) f).det

Tactic:
rw [LinearMap.coe_det, dif_pos this, detAux_def'' _ b]

Goal state after:
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: case h.inr.succ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f

Tactic:
have hg2 : g.natDegree ≠ 0 := by
      intro this
      rw [this, zero_mul] at hg1
      cases hg1

Goal state after:
case h.inr.succ
F : Type u
inst✝ : Field F
p : ℕ
HF : CharP F p
hp : Nat.Prime p
f : F[X]
hf : Irreducible f
h1 : ¬f.Separable
g : F[X]
hg : Irreducible g
hgf : (expand F p) g = f
N : ℕ
ih : ∀ m < N + 1, ∀ {f : F[X]}, Irreducible f → f.natDegree = m → ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f
hn : f.natDegree = N + 1
hg1 : g.natDegree * p = N.succ
hg2 : g.natDegree ≠ 0
⊢ ∃ n g, g.Separable ∧ (expand F (p ^ n)) g = f