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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'

Goal state after:
case h₁
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₁

case h₂
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₂

case h₃
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯).τ₃
Module: Mathlib.CategoryTheory.Square

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
sq₁ sq₂ : Square C
e₁ : sq₁.X₁ ≅ sq₂.X₁
e₂ : sq₁.X₂ ≅ sq₂.X₂
e₃ : sq₁.X₃ ≅ sq₂.X₃
e₄ : sq₁.X₄ ≅ sq₂.X₄
comm₁₂ : sq₁.f₁₂ ≫ e₂.hom = e₁.hom ≫ sq₂.f₁₂
comm₁₃ : sq₁.f₁₃ ≫ e₃.hom = e₁.hom ≫ sq₂.f₁₃
comm₂₄ : sq₁.f₂₄ ≫ e₄.hom = e₂.hom ≫ sq₂.f₂₄
comm₃₄ : sq₁.f₃₄ ≫ e₄.hom = e₃.hom ≫ sq₂.f₃₄
⊢ sq₂.f₂₄ ≫ e₄.inv = e₂.inv ≫ sq₁.f₂₄

Tactic:
simp only [← cancel_mono e₄.hom, assoc, Iso.inv_hom_id,
                      comp_id, comm₂₄, Iso.inv_hom_id_assoc]

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₁' L₂' : LieSubalgebra R L
h : L₁'.toSubmodule = L₂'.toSubmodule
⊢ L₁' = L₂'

Tactic:
by
  rw [SetLike.ext'_iff] at h
  rw [← coe_set_eq]
  exact h

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
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ comap f ⊥
⊢ I = ⊥

Tactic:
h₁

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'
I : LieIdeal R L
h₁ : comap f ⊥ = ⊥
h₂ : I ≤ ⊥
⊢ I = ⊥
Module: Mathlib.Algebra.Lie.Submodule

Goal state before:
pp: case insert
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
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih : ∀ {m : M}, ↑t ⊆ {x | ∃ p ∈ S, ↑p = x} → m ∈ ⨆ i ∈ t, i → ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
hs : ↑(insert q t) ⊆ {x | ∃ p ∈ S, ↑p = x}
m' : M
hm' : m' ∈ q
u : M
hu : u ∈ ⨆ x ∈ t, x
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
⊢ ⁅x, m'⁆ + ⁅x, u⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}

Tactic:
refine add_mem ?_ (ih (Subset.trans (by simp) hs) hu)

Goal state after:
case insert
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
S : Set (LieSubmodule R L M)
x : L
q : Submodule R M
t : Finset (Submodule R M)
hqt : q ∉ t
ih : ∀ {m : M}, ↑t ⊆ {x | ∃ p ∈ S, ↑p = x} → m ∈ ⨆ i ∈ t, i → ⁅x, m⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
hs : ↑(insert q t) ⊆ {x | ∃ p ∈ S, ↑p = x}
m' : M
hm' : m' ∈ q
u : M
hu : u ∈ ⨆ x ∈ t, x
hsm : m' + u ∈ q ⊔ ⨆ x ∈ t, x
⊢ ⁅x, m'⁆ ∈ sSup {x | ∃ p ∈ S, ↑p = x}
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
h : ↑(map f I) = ⇑f '' ↑I
⊢ ↑(comap f (map f I)) = ↑(I ⊔ f.ker)

Tactic:
comap_toSubmodule,

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'
I : LieIdeal R L
h : ↑(map f I) = ⇑f '' ↑I
⊢ Submodule.comap ↑f ↑(map f I) = ↑(I ⊔ f.ker)
Module: Mathlib.Algebra.Lie.Abelian

Goal state before:
pp: R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian ↥I ↔ I ≤ LieModule.ker R L ↥I

Tactic:
refine ⟨fun hI x hx ↦ LieHom.mem_ker.mpr ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩

Goal state after:
case refine_1
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
hI : IsLieAbelian ↥I
x : L
hx : x ∈ I
⊢ (toEnd R L ↥I) x = 0

case refine_2
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
h : I ≤ LieModule.ker R L ↥I
x✝¹ x✝ : ↥I
x : L
hx : x ∈ I
y : L
hy : y ∈ I
⊢ ⁅⟨x, hx⟩, ⟨y, hy⟩⁆ = 0
Module: Mathlib.Algebra.Lie.IdealOperations

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

Tactic:
comap_toSubmodule,

Goal state after:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
J₁ J₂ : LieIdeal R L'
h : f.IsIdealMorphism
⊢ Submodule.comap ↑f ↑⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ↑(⁅comap f J₁, comap f J₂⁆ ⊔ f.ker)
Module: Mathlib.RingTheory.Polynomial.Quotient

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
h : ¬m = 0
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m

Tactic:
· simp [h]

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

Goal state before:
pp: 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

Tactic:
hp

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p q : (R ⧸ I)[X]
hp :
  (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 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:
hp

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]
hp :
  (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 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:
hp

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ (R ⧸ I)
hp :
  (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 mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
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)) (p * X i)) =
      p * X i

Tactic:
hp

Goal state after:
case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
i : σ
hp :
  (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)) (p * X i)) =
    p * X i
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 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:
hp

Goal state after:
case add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  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.RingTheory.Polynomial.Quotient

Goal state before:
pp: case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
i : σ
⊢ 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)) (p * X i))) =
      (Ideal.Quotient.mk (Ideal.map C I)) (p * X i)

Tactic:
hp

Goal state after:
case mul_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
f p : MvPolynomial σ R
i : σ
hp :
  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)) (p * X i))) =
    (Ideal.Quotient.mk (Ideal.map C I)) (p * X i)
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : DecompositionMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ y ^ 2
⊢ x ∣ y

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul (sq y ▸ hy)

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : DecompositionMonoid R
y a b : R
ha : a ∣ y
hb : b ∣ y
hx : Squarefree (a * b)
hy : a * b ∣ y ^ 2
⊢ a * b ∣ y
Module: Mathlib.Algebra.Squarefree.Basic

Goal state before:
pp: case pos.inl
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h✝ : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
hmem : a ∈ normalizedFactors x
ha : Irreducible a
h : ↑(Multiset.count (normalize a) (normalizedFactors x)) ≤ 1
⊢ Multiset.count (normalize a) (normalizedFactors x) ≤ 1

Tactic:
assumption_mod_cast

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1
a : R
⊢ Multiset.count a (normalizedFactors x) ≤ 1

pp: case mpr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ emultiplicity a x ≤ 1 ∨ IsUnit a

Tactic:
· 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]

Goal state after:
case mpr
R : Type u_1
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
⊢ emultiplicity a x ≤ 1 ∨ IsUnit a
Module: Mathlib.FieldTheory.Separable

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) s).prod.Separable
⊢ ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t

Tactic:
rintro a t rfl

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : (Multiset.map (fun a ↦ X - C a) (a ::ₘ a ::ₘ t)).prod.Separable
⊢ False
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
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ LinearMap.det f = 1

Tactic:
by
  rw [LinearMap.det, dif_neg, MonoidHom.one_apply]
  exact fun ⟨_, ⟨b⟩⟩ ↦ h (Module.Finite.of_basis b)

Goal state after:
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
⊢ (of f) p = 0 → p = 0

Tactic:
hp

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : (of f) p = 0
⊢ p = 0
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
f : M [⋀^ι]→ₗ[R] R
⊢ f = f ⇑e • e.det

Tactic:
refine Basis.ext_alternating e fun i h => ?_

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✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
⊢ (f fun i_1 ↦ e (i i_1)) = (f ⇑e • e.det) fun i_1 ↦ e (i i_1)
Module: Mathlib.RingTheory.Nilpotent.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
⊢ exp a = ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i

Tactic:
suffices ∑ i ∈ Ico (nilpotencyClass a) k, (i.factorial : ℚ)⁻¹ • (a ^ i) = 0 by
    dsimp [exp]
    rw [h₁, this, add_zero]

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Module ℚ A
a : A
k : ℕ
h : a ^ k = 0
h₁ :
  ∑ i ∈ range k, (↑i !)⁻¹ • a ^ i =
    ∑ i ∈ range (nilpotencyClass a), (↑i !)⁻¹ • a ^ i + ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i
⊢ ∑ i ∈ Ico (nilpotencyClass a) k, (↑i !)⁻¹ • a ^ i = 0
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
R : Type u_6
S : Type u_7
T : Type u_8
U : Type u_9
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : CommRing U
inst✝ : Algebra R U
p✝ p : S[X]
q : (T ⊗[R] S)[X]
h : Polynomial.map includeRight.toRingHom p = q
⊢ T ⊗[R] AdjoinRoot p ≃ₐ[T] AdjoinRoot q

Tactic:
refine .ofAlgHom
    (Algebra.TensorProduct.lift (algHom T T _)
      (mapAlgHom includeRight p q <| by exact h.symm.dvd) fun _ _ ↦ .all ..)
    (liftAlgHom _ (Algebra.TensorProduct.map (AlgHom.id T T)
      (((Algebra.ofId S (AdjoinRoot p))).restrictScalars R)) (1 ⊗ₜ root _) ?_) ?_ ?_
  · simp only [← h, AlgHom.toRingHom_eq_coe]
    rw [Polynomial.eval₂_map]
    change Polynomial.eval₂ ((Algebra.TensorProduct.map (AlgHom.id R T) _).comp _).toRingHom _ _ = _
    simp only [map_comp_includeRight, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom,
      AlgHom.coe_restrictScalars, ← Polynomial.eval₂_map]
    change Polynomial.eval₂ _ ((RingHomClass.toRingHom includeRight) (root p)) (p.map (of _)) = _
    rw [Polynomial.eval₂_hom]
    simp [Polynomial.eval_map]
  · ext
    · simp [Algebra.ofId_apply]
    simp
  · ext : 3 <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.JordanChevalley

Goal state before:
pp: case h
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
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
q : K[X]
hq : P ^ k = minpoly K f * q
⊢ (aeval ff) P ^ k = 0

Tactic:
rw [← map_pow, Subtype.ext_iff]

Goal state after:
case h
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
ff : ↥K[f] := ⟨f, ⋯⟩
P' : K[X] := derivative P
q : K[X]
hq : P ^ k = minpoly K f * q
⊢ ↑((aeval ff) (P ^ k)) = ↑0